From 96051f1ffee1473582cc9aac6ec4b6724e88c8bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 3 Feb 2024 12:25:14 +0000 Subject: [PATCH] Even more upstreamed lemmas --- LeanAPAP.lean | 2 - LeanAPAP/Mathlib/Data/Finset/Image.lean | 8 -- LeanAPAP/Mathlib/Data/Rat/Order.lean | 3 +- .../Mathlib/Order/Partition/Finpartition.lean | 99 ------------------- 4 files changed, 2 insertions(+), 110 deletions(-) delete mode 100644 LeanAPAP/Mathlib/Data/Finset/Image.lean delete mode 100644 LeanAPAP/Mathlib/Order/Partition/Finpartition.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index e5cc71e9d2..2bdb0002bb 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -27,7 +27,6 @@ import LeanAPAP.Mathlib.Data.Complex.Order import LeanAPAP.Mathlib.Data.ENNReal.Basic import LeanAPAP.Mathlib.Data.ENNReal.Inv import LeanAPAP.Mathlib.Data.Finset.Card -import LeanAPAP.Mathlib.Data.Finset.Image import LeanAPAP.Mathlib.Data.Fintype.Pi import LeanAPAP.Mathlib.Data.FunLike.Basic import LeanAPAP.Mathlib.Data.Nat.Parity @@ -46,7 +45,6 @@ import LeanAPAP.Mathlib.GroupTheory.GroupAction.Defs import LeanAPAP.Mathlib.GroupTheory.OrderOfElement import LeanAPAP.Mathlib.GroupTheory.Submonoid.Basic import LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations -import LeanAPAP.Mathlib.Order.Partition.Finpartition import LeanAPAP.Mathlib.Tactic.Positivity import LeanAPAP.Mathlib.Tactic.Positivity.Finset import LeanAPAP.Physics.AlmostPeriodicity diff --git a/LeanAPAP/Mathlib/Data/Finset/Image.lean b/LeanAPAP/Mathlib/Data/Finset/Image.lean deleted file mode 100644 index 3f2ea1d31a..0000000000 --- a/LeanAPAP/Mathlib/Data/Finset/Image.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Mathlib.Data.Finset.Image - -open Finset Function - -variable {α β : Type*} [DecidableEq β] {f : α → β} - -lemma Function.Injective.finset_image (hf : Injective f) : Injective (image f) := fun s t h ↦ - coe_injective $ hf.image_injective $ by simp_rw [←coe_image, h] diff --git a/LeanAPAP/Mathlib/Data/Rat/Order.lean b/LeanAPAP/Mathlib/Data/Rat/Order.lean index f86da967af..aff3975024 100644 --- a/LeanAPAP/Mathlib/Data/Rat/Order.lean +++ b/LeanAPAP/Mathlib/Data/Rat/Order.lean @@ -1,5 +1,6 @@ import Mathlib.Data.Rat.Order -import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Positivity.Basic +import Mathlib.Tactic.NormNum.Basic namespace Rat variable {q : ℚ} diff --git a/LeanAPAP/Mathlib/Order/Partition/Finpartition.lean b/LeanAPAP/Mathlib/Order/Partition/Finpartition.lean deleted file mode 100644 index ccf1cd3eaf..0000000000 --- a/LeanAPAP/Mathlib/Order/Partition/Finpartition.lean +++ /dev/null @@ -1,99 +0,0 @@ -import LeanAPAP.Mathlib.Data.Finset.Image -import Mathlib.Order.Partition.Finpartition - -open Finset Function - -variable {α β : Type*} [DecidableEq α] [DecidableEq β] - -namespace Finpartition - --- TODO: Fix field name -alias sup_parts := supParts - -@[simps] -def finsetImage {a : Finset α} (P : Finpartition a) (f : α → β) (hf : Injective f) : - Finpartition (a.image f) where - parts := P.parts.image (image f) - supIndep := by - rw [supIndep_iff_pairwiseDisjoint, coe_image, (hf.finset_image.injOn _).pairwiseDisjoint_image] - simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, Function.onFun, Ne.def, - Function.id_comp, disjoint_image hf] - exact P.disjoint - supParts := by - ext i - simp only [mem_sup, mem_image, exists_prop, id.def, exists_exists_and_eq_and] - constructor - · rintro ⟨j, hj, i, hij, rfl⟩ - exact ⟨_, P.le hj hij, rfl⟩ - rintro ⟨j, hj, rfl⟩ - rw [←P.sup_parts] at hj - simp only [mem_sup, id.def, exists_prop] at hj - obtain ⟨b, hb, hb'⟩ := hj - exact ⟨b, hb, _, hb', rfl⟩ - not_bot_mem := by - simpa only [bot_eq_empty, mem_image, image_eq_empty, exists_prop, exists_eq_right] using - P.not_bot_mem - -def extend' [DistribLattice α] [OrderBot α] {a b c : α} (P : Finpartition a) (hab : Disjoint a b) - (hc : a ⊔ b = c) : Finpartition c := - if hb : b = ⊥ then P.copy (by rw [←hc, hb, sup_bot_eq]) else P.extend hb hab hc - -def modPartitions (s d : ℕ) (hd : d ≠ 0) (h : d ≤ s) : Finpartition (range s) - where - parts := (range d).image fun i ↦ (range s).filter fun j ↦ j % d = i - supIndep := by - rw [supIndep_iff_pairwiseDisjoint, coe_image, Set.InjOn.pairwiseDisjoint_image] - · simp only [Set.PairwiseDisjoint, Function.onFun, Set.Pairwise, mem_coe, mem_range, - disjoint_left, Function.id_comp, mem_filter, not_and, and_imp] - rintro x hx y - hxy a - rfl - - exact hxy - simp only [Set.InjOn, coe_range, Set.mem_Iio] - intro x₁ hx₁ x₂ _ h' - have : x₁ ∈ (range s).filter fun j ↦ j % d = x₂ - · rw [←h', mem_filter, mem_range, Nat.mod_eq_of_lt hx₁] - simp only [hx₁.trans_le h, eq_self_iff_true, and_self_iff] - rw [mem_filter, Nat.mod_eq_of_lt hx₁] at this - exact this.2 - supParts := by - rw [sup_image, Function.id_comp] - refine' Subset.antisymm _ _ - · rw [Finset.sup_eq_biUnion, biUnion_subset] - simp only [filter_subset, imp_true_iff] - intro i hi - have : 0 < d := hd.bot_lt - simpa [mem_sup, Nat.mod_lt _ this] using hi - not_bot_mem := by - simp only [bot_eq_empty, mem_image, mem_range, exists_prop, not_exists, not_and, - filter_eq_empty_iff, not_forall, Classical.not_not] - intro i hi - exact ⟨_, hi.trans_le h, Nat.mod_eq_of_lt hi⟩ - -lemma modPartitions_parts_eq (s d : ℕ) (hd : d ≠ 0) (h : d ≤ s) : - (modPartitions s d hd h).parts = - (range d).image fun i ↦ (range ((s - i - 1) / d + 1)).image fun x ↦ i + d * x := by - rw [modPartitions] - ext x - simp only [mem_image, mem_range] - refine' exists_congr fun i ↦ and_congr_right fun hi ↦ _ - suffices - ((range ((s - i - 1) / d + 1)).image fun x ↦ i + d * x) = (range s).filter fun j ↦ j % d = i - by rw [this] - clear x - ext j - simp only [mem_image, mem_filter, mem_range, Nat.lt_add_one_iff] - constructor - · rintro ⟨j, hj, rfl⟩ - rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hi, eq_self_iff_true, and_true_iff, ← - lt_tsub_iff_left, mul_comm] - rwa [Nat.le_div_iff_mul_le hd.bot_lt, le_tsub_iff_right, Nat.succ_le_iff] at hj - rw [Nat.succ_le_iff] - exact Nat.sub_pos_of_lt (hi.trans_le h) - · rintro ⟨hj, rfl⟩ - refine' ⟨j / d, _, Nat.mod_add_div _ _⟩ - rwa [Nat.le_div_iff_mul_le' hd.bot_lt, le_tsub_iff_right, le_tsub_iff_left, ←add_assoc, - mul_comm, Nat.mod_add_div, Nat.add_one_le_iff] - · exact hi.le.trans h - rw [Nat.succ_le_iff] - exact Nat.sub_pos_of_lt (hi.trans_le h) - -end Finpartition