diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index bc25000db5..bd847af052 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -1,5 +1,6 @@ import LeanCamCombi.Archive.CauchyDavenportFromKneser import LeanCamCombi.BernoulliSeq +import LeanCamCombi.ConvexContinuous import LeanCamCombi.DiscreteDeriv import LeanCamCombi.ErdosGinzburgZiv import LeanCamCombi.ErdosRenyi.Basic @@ -42,12 +43,11 @@ import LeanCamCombi.Mathlib.Data.Finset.PosDiffs import LeanCamCombi.Mathlib.Data.List.Basic import LeanCamCombi.Mathlib.Data.List.DropRight import LeanCamCombi.Mathlib.Data.Multiset.Basic +import LeanCamCombi.Mathlib.Data.Nat.Defs import LeanCamCombi.Mathlib.Data.Nat.Factors -import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas import LeanCamCombi.Mathlib.Data.Set.Finite import LeanCamCombi.Mathlib.Data.Set.Image import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul -import LeanCamCombi.Mathlib.Data.Subtype import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup import LeanCamCombi.Mathlib.Order.Category.BoolAlg diff --git a/LeanCamCombi/BernoulliSeq.lean b/LeanCamCombi/BernoulliSeq.lean index 5382e7dc31..dd46df78da 100644 --- a/LeanCamCombi/BernoulliSeq.lean +++ b/LeanCamCombi/BernoulliSeq.lean @@ -137,8 +137,8 @@ protected lemma union (h : IndepFun X Y μ) : add_tsub_assoc_of_le (mul_le_of_le_one_left' $ hX.le_one)] · exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq (add_tsub_cancel_of_le hX.le_one) - · rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl, MeasurableSpace.comap_compl measurable_compl, - ←IndepFun_iff] + · rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl, + MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff] end IsBernoulliSeq end ProbabilityTheory diff --git a/LeanCamCombi/DiscreteDeriv.lean b/LeanCamCombi/DiscreteDeriv.lean index edc358b1b6..6ac8a18000 100644 --- a/LeanCamCombi/DiscreteDeriv.lean +++ b/LeanCamCombi/DiscreteDeriv.lean @@ -1,7 +1,7 @@ +import Mathlib.Algebra.Polynomial.AlgebraMap import Mathlib.Algebra.Polynomial.BigOperators +import Mathlib.Algebra.Polynomial.Degree.Lemmas import Mathlib.Data.Finsupp.Notation -import Mathlib.Data.Polynomial.AlgebraMap -import Mathlib.Data.Polynomial.Degree.Lemmas open Finset open scoped BigOperators diff --git a/LeanCamCombi/ErdosGinzburgZiv.lean b/LeanCamCombi/ErdosGinzburgZiv.lean index bf5a9c115a..024b6ce717 100644 --- a/LeanCamCombi/ErdosGinzburgZiv.lean +++ b/LeanCamCombi/ErdosGinzburgZiv.lean @@ -7,8 +7,7 @@ import Mathlib.Data.Multiset.Fintype import Mathlib.FieldTheory.ChevalleyWarning import LeanCamCombi.Mathlib.Algebra.Order.Ring.Canonical import LeanCamCombi.Mathlib.Data.Multiset.Basic -import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas -import LeanCamCombi.Mathlib.Data.Subtype +import LeanCamCombi.Mathlib.Data.Nat.Defs import LeanCamCombi.Mathlib.FieldTheory.Finite.Basic import LeanCamCombi.Mathlib.RingTheory.Int.Basic @@ -98,8 +97,8 @@ private lemma aux (hs : Multiset.card s = 2 * p - 1) : · rw [Finset.card_attach, card_toEnumFinset, hs] exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`. - · simpa only [f₂, map_sum, ZMod.pow_card_sub_one, Finset.sum_map_val, Finset.sum_filter, smul_eval, - map_pow, eval_X, mul_ite, mul_zero, mul_one] using x.2.2 + · simpa only [f₂, map_sum, ZMod.pow_card_sub_one, Finset.sum_map_val, Finset.sum_filter, + smul_eval, map_pow, eval_X, mul_ite, mul_zero, mul_one] using x.2.2 --TODO: Rename `Multiset.pairwise_nil` to `Multiset.pairwise_zero` diff --git a/LeanCamCombi/Incidence.lean b/LeanCamCombi/Incidence.lean index 9fb5539248..6ded31da57 100644 --- a/LeanCamCombi/Incidence.lean +++ b/LeanCamCombi/Incidence.lean @@ -552,7 +552,7 @@ lemma mu_toDual (a b : α) : mu 𝕜 (toDual a) (toDual b) = mu 𝕜 b a := by ext a b simp only [mul_boole, one_apply, mul_apply, coe_mk, zeta_apply] obtain rfl | h := eq_or_ne a b - · simp + · simp [mud] · rw [if_neg h] convert_to ∑ x in Icc (ofDual b) (ofDual a), mu 𝕜 x a = 0 sorry @@ -683,7 +683,8 @@ variable (𝕜) [Ring 𝕜] [PartialOrder α] [PartialOrder β] [LocallyFiniteOr [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableRel ((· ≤ ·) : α → α → Prop)] [DecidableRel ((· ≤ ·) : β → β → Prop)] -/-- The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel and O'Donnell. -/ +/-- The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel +and O'Donnell. -/ @[simp] lemma mu_prod_mu : (mu 𝕜).prod (mu 𝕜) = (mu 𝕜 : IncidenceAlgebra 𝕜 (α × β)) := by refine left_inv_eq_right_inv ?_ zeta_mul_mu diff --git a/LeanCamCombi/Kneser/Kneser.lean b/LeanCamCombi/Kneser/Kneser.lean index 02e43a49f0..f7996bdd0e 100644 --- a/LeanCamCombi/Kneser/Kneser.lean +++ b/LeanCamCombi/Kneser/Kneser.lean @@ -240,7 +240,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s) norm_num all_goals apply subset_trans (mul_subset_mul_left hst) - rw [← inter_distrib_right] + rw [← union_inter_distrib_right] refine' subset_trans (mul_subset_mul_right (inter_subset_right _ _)) _ simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl] _ ≤ @@ -254,7 +254,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s) · apply smul_finset_subset_smul (mem_union_left t has) (mem_sdiff.mp hx).1 have hx' := (mem_sdiff.mp hx).2 contrapose! hx' - rw [← inter_distrib_right] + rw [← union_inter_distrib_right] obtain ⟨y, hyst, d, hd, hxyd⟩ := mem_mul.mp hx' obtain ⟨c, hc, hcx⟩ := mem_smul_finset.mp (mem_sdiff.mp hx).1 rw [← hcx, ← eq_mul_inv_iff_mul_eq] at hxyd @@ -345,7 +345,7 @@ theorem mul_kneser : rw [← inv_smul_eq_iff] at ht' subst ht' rename' t' => t - rw [mem_inv_smul_finset_iff, smul_eq_mul, div_mul_cancel'] at hc + rw [mem_inv_smul_finset_iff, smul_eq_mul, div_mul_cancel] at hc rw [div_mul_comm, mem_inv_smul_finset_iff, smul_eq_mul, ← mul_assoc, div_mul_div_cancel', div_self', one_mul] at hbac rw [smul_finset_nonempty] at ht @@ -419,13 +419,13 @@ theorem mul_kneser : obtain ht₂ | ht₂ne := t₂.eq_empty_or_nonempty · have aux₁_contr := disjoint_mul_sub_card_le b (hs₁s has₁) (disjoint_iff_inter_eq_empty.2 ht₂) hH₁H.subset - linarith [aux1₁, aux₁_contr, Int.coe_nat_nonneg (t₁ * (s₁ * t₁).mulStab).card] + linarith [aux1₁, aux₁_contr, Int.natCast_nonneg (t₁ * (s₁ * t₁).mulStab).card] obtain hs₂ | hs₂ne := s₂.eq_empty_or_nonempty · have aux1₁_contr := disjoint_mul_sub_card_le a (ht₁t hbt₁) (disjoint_iff_inter_eq_empty.2 hs₂) (by rw [mul_comm]; exact hH₁H.subset) simp only [union_comm t s, mul_comm t₁ s₁] at aux1₁_contr - linarith [aux1₁, aux1₁_contr, Int.coe_nat_nonneg (s₁ * (s₁ * t₁).mulStab).card] + linarith [aux1₁, aux1₁_contr, Int.natCast_nonneg (s₁ * (s₁ * t₁).mulStab).card] have hC₂stab : C₂.mulStab = H₂ := mulStab_union hs₂ne ht₂ne (by rwa [mul_comm]) hCst₂ have hH₂H : H₂ ⊂ H := mulStab_mul_ssubset_mulStab hs₂ne ht₂ne (by rwa [mul_comm]) have aux1₂ := @@ -444,17 +444,17 @@ theorem mul_kneser : habH).mono sdiff_le sdiff_le have hSst : S ⊆ a • H \ (s ∪ t) := by - simp only [hS, hs₁, ht₂, ← inter_distrib_right, sdiff_inter_self_right, Subset.rfl] + simp only [hS, hs₁, ht₂, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl] have hTst : T ⊆ b • H \ (s ∪ t) := by - simp only [hT, hs₂, ht₁, ← inter_distrib_right, sdiff_inter_self_right, Subset.rfl] + simp only [hT, hs₂, ht₁, ← union_inter_distrib_right, sdiff_inter_self_right, Subset.rfl] have hSTst : Disjoint (S ∪ T) (s ∪ t) := (subset_sdiff.1 hSst).2.sup_left (subset_sdiff.1 hTst).2 have hstconv : s * t ∉ convergent := by apply hCmin (s * t) rw [hstab] refine (hC.mulStab_nontrivial.mp hCstab).symm.ssubset_of_subset ?_ simp only [one_subset, one_mem_mulStab, hC] - simp only [Set.mem_setOf_eq, Subset.rfl, true_and_iff, not_le, hstab, mul_one, card_one] - at hstconv + simp only [Set.mem_setOf_eq, Subset.rfl, true_and_iff, not_le, hstab, mul_one, card_one, + convergent] at hstconv zify at hstconv have hSTcard : (S.card : ℤ) + T.card + (s ∪ t).card ≤ ((s ∪ t) * H).card := by norm_cast diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean index c62db57d7e..9c80a12ed0 100644 --- a/LeanCamCombi/Kneser/KneserRuzsa.lean +++ b/LeanCamCombi/Kneser/KneserRuzsa.lean @@ -38,7 +38,8 @@ namespace Finset -- Lemma 3.3 in Ruzsa's notes @[to_additive] lemma le_card_union_add_card_mulStab_union : - min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card := by + min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ + (s ∪ t).card + (s ∪ t).mulStab.card := by obtain rfl | hs := s.eq_empty_or_nonempty · simp [-zero_le'] -- TODO: `to_additive` chokes on `zero_le'` @@ -65,7 +66,7 @@ lemma le_card_union_add_card_mulStab_union : obtain ⟨w, hwx⟩ := Quotient.exists_rep x have : ⟦w⟧ = QuotientGroup.mk (s := N) w := by exact rfl rw [← hwx, this, QuotientGroup.eq] at hyx hzx ⊢ - simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff] at hyx hzx ⊢ + simp only [mul_one, inv_mem_iff, Subgroup.mem_inf, mem_stabilizer_iff, N] at hyx hzx ⊢ constructor · convert hyx.1 using 1 rw [mul_comm, mul_smul] @@ -76,7 +77,7 @@ lemma le_card_union_add_card_mulStab_union : congr simp only [← inv_smul_eq_iff, inv_inv, ← (mem_mulStab ht), hz] all_goals { aesop } - · aesop + · simp (config := { contextual := true }) [*] specialize this (α := α ⧸ N) (s := s.image (↑)) (t := t.image (↑)) simp only [image_nonempty, mulStab_nonempty, mul_nonempty, and_imp, forall_true_left, hs, ht, h1] at this @@ -100,89 +101,90 @@ lemma le_card_union_add_card_mulStab_union : (card (image (QuotientGroup.mk (s := N)) t) + card (mulStab (image (QuotientGroup.mk (s := N)) t))) := by rw [mulStab_quotient_commute_subgroup N t, mulStab_quotient_commute_subgroup N s] - all_goals { aesop } + all_goals simp [*] _ ≤ Nat.card N * (card (image (QuotientGroup.mk (s := N)) s ∪ image (QuotientGroup.mk (s := N)) t) + card (mulStab (image (QuotientGroup.mk (s := N)) s ∪ image (QuotientGroup.mk (s := N)) t))) := Nat.mul_le_mul_left _ this - _ ≤ card (s ∪ t) + card (mulStab (s ∪ t)) := by + _ ≤ card (s ∪ t) + card (s ∪ t).mulStab := by rw [mul_add, ← image_union, subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t), ← mulStab_quotient_commute_subgroup N (s ∪ t), - subgroup_mul_card_eq_mul_of_mul_stab_subset N (mulStab (s ∪ t))] + subgroup_mul_card_eq_mul_of_mul_stab_subset N (s ∪ t).mulStab] all_goals { simp only [hNmulstab, mulStab_idem]; norm_cast; exact inter_mulStab_subset_mulStab_union } - obtain hst | hst := (subset_union_left s t).eq_or_ssubset - · simp [hst.symm] - obtain hts | hts := (subset_union_right s t).eq_or_ssubset - · simp [hts.symm] - have : H.card = Hs.card * Ht.card := by - refine' card_mul_iff.2 fun a ha b hb hab => _ - replace hab : a.2 * b.2⁻¹ = a.1⁻¹ * b.1 := by - rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← inv_mul_eq_iff_eq_mul, inv_inv] - exact hab - have : a.1⁻¹ * b.1 ∈ Hs ∩ Ht := by - simp only [mem_inter] - constructor - · rw [mem_mulStab hs, mul_smul, inv_smul_eq_iff, - (mem_mulStab hs).mp (show b.1 ∈ mulStab s by aesop), - (mem_mulStab hs).mp (show a.1 ∈ mulStab s by aesop)] - · rw [← hab, mem_mulStab ht, mul_comm, mul_smul, inv_smul_eq_iff, - (mem_mulStab ht).mp (show b.2 ∈ mulStab t by aesop), - (mem_mulStab ht).mp (show a.2 ∈ mulStab t by aesop)] - simp only [h1, mem_one] at this - ext - · rw [← inv_mul_eq_one, this] - · rw [← mul_inv_eq_one, hab, this] + -- obtain hst | hst := (subset_union_left s t).eq_or_ssubset + -- · simp [hst.symm] + -- obtain hts | hts := (subset_union_right s t).eq_or_ssubset + -- · simp [hts.symm] + -- have : H.card = Hs.card * Ht.card := by + -- refine' card_mul_iff.2 fun a ha b hb hab => _ + -- replace hab : a.2 * b.2⁻¹ = a.1⁻¹ * b.1 := by + -- rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← inv_mul_eq_iff_eq_mul, inv_inv] + -- exact hab + -- have : a.1⁻¹ * b.1 ∈ Hs ∩ Ht := by + -- simp only [mem_inter] + -- constructor + -- · rw [mem_mulStab hs, mul_smul, inv_smul_eq_iff, + -- (mem_mulStab hs).mp hb.1, + -- (mem_mulStab hs).mp ha.1] + -- · rw [← hab, mem_mulStab ht, mul_comm, mul_smul, inv_smul_eq_iff, + -- (mem_mulStab ht).mp hb.2, + -- (mem_mulStab ht).mp ha.2] + -- simp only [h1, mem_one] at this + -- ext + -- · rw [← inv_mul_eq_one, this] + -- · rw [← mul_inv_eq_one, hab, this] -- mistake in proof sketch, need to interchange `Hs` and `Ht` - suffices h2 : Hs.card - (mulStab (s ∪ t)).card ≤ (s \ t).card ∨ - Ht.card - (mulStab (s ∪ t)).card ≤ (t \ s).card by - simp only [min_le_iff] - cases' h2 with h2 h2 - · left - sorry - · right - sorry - have Hst : (mulStab (s ∪ t)).Nonempty := ht.inr.mulStab - set k : α → ℕ := fun a => - card ((a • H).image (QuotientGroup.mk (s := stabilizer α s)) ∩ s.image QuotientGroup.mk) - set l : α → ℕ := fun a => - card ((a • H).image (QuotientGroup.mk (s := stabilizer α t)) ∩ t.image QuotientGroup.mk) - have hkt : ∀ a, k a ≤ Ht.card := sorry - have hls : ∀ a, l a ≤ Hs.card := sorry - have hk : ∀ a, (s \ t ∩ a • H).card = k a * (Hs.card - l a) := by sorry - have hl : ∀ a, (t \ s ∩ a • H).card = l a * (Ht.card - k a) := by sorry - by_cases hkl : - (∀ a, k a = 0 ∨ k a = Ht.card ∨ l a = 0 ∨ l a = Hs.card) ∧ - ((∀ a, k a = 0 → l a = 0) ∨ ∀ a, l a = 0 → k a = 0) - · obtain ⟨hkl, hkl' | hkl'⟩ := hkl - · refine' Or.inl ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _) - sorry - · refine' Or.inr ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _) - sorry - -- the remaining sketch is flawed since `H` is defined to be `Hbar` in Ruzsa's notes and - -- `mulStab (s ∪ t) = H` in the notes - suffices hHst : (Hs.card - 1) * (Ht.card - 1) ≤ (s \ t).card * (t \ s).card by - by_contra! - exact hHst.not_lt $ CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt (this.1.trans_le $ - tsub_le_tsub_left (one_le_card.2 Hst) _) $ this.2.trans_le $ - tsub_le_tsub_left (one_le_card.2 Hst) _ - simp (config := {zeta := false}) only - [not_and_or, not_or, Classical.not_forall, not_ne_iff, not_imp] at hkl - obtain ⟨a, hka, hka', hla, hla'⟩ | ⟨⟨a, hka, hla⟩, b, hlb, hkb⟩ := hkl - · refine le_trans ?_ (mul_le_mul' (card_mono $ inter_subset_left _ $ a • H) $ - card_mono $ inter_subset_left _ $ a • H) - rw [hk, hl, mul_comm (k a), mul_mul_mul_comm, mul_comm (k a)] - refine le_trans ?_ - (mul_le_mul' (Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hls _).lt_of_ne hla').ne' hla) $ - Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hkt _).lt_of_ne hka').ne' hka) - rw [tsub_add_cancel_of_le (hkt _), tsub_add_cancel_of_le (hls _)] - refine' - mul_le_mul' (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ b • H) - (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ a • H) - · rw [hk, hlb, tsub_zero] - exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hkb) - · rw [hl, hka, tsub_zero] - exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hla) + -- suffices h2 : Hs.card - (s ∪ t).mulStab.card ≤ (s \ t).card ∨ + -- Ht.card - (s ∪ t).mulStab.card ≤ (t \ s).card by + -- simp only [min_le_iff] + -- cases' h2 with h2 h2 + -- · left + -- sorry + -- · right + -- sorry + -- have Hst : (s ∪ t).mulStab.Nonempty := ht.inr.mulStab + -- set k : α → ℕ := fun a => + -- card ((a • H).image (QuotientGroup.mk (s := stabilizer α s)) ∩ s.image QuotientGroup.mk) + sorry + -- set l : α → ℕ := fun a => + -- card ((a • H).image (QuotientGroup.mk (s := stabilizer α t)) ∩ t.image QuotientGroup.mk) + -- have hkt : ∀ a, k a ≤ Ht.card := sorry + -- have hls : ∀ a, l a ≤ Hs.card := sorry + -- have hk : ∀ a, (s \ t ∩ a • H).card = k a * (Hs.card - l a) := by sorry + -- have hl : ∀ a, (t \ s ∩ a • H).card = l a * (Ht.card - k a) := by sorry + -- by_cases hkl : + -- (∀ a, k a = 0 ∨ k a = Ht.card ∨ l a = 0 ∨ l a = Hs.card) ∧ + -- ((∀ a, k a = 0 → l a = 0) ∨ ∀ a, l a = 0 → k a = 0) + -- · obtain ⟨hkl, hkl' | hkl'⟩ := hkl + -- · refine' Or.inl ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _) + -- sorry + -- · refine' Or.inr ((tsub_eq_zero_of_le $ card_mono _).trans_le $ zero_le _) + -- sorry + -- -- the remaining sketch is flawed since `H` is defined to be `Hbar` in Ruzsa's notes and + -- -- `mulStab (s ∪ t) = H` in the notes + -- suffices hHst : (Hs.card - 1) * (Ht.card - 1) ≤ (s \ t).card * (t \ s).card by + -- by_contra! + -- exact hHst.not_lt $ CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt (this.1.trans_le $ + -- tsub_le_tsub_left (one_le_card.2 Hst) _) $ this.2.trans_le $ + -- tsub_le_tsub_left (one_le_card.2 Hst) _ + -- simp (config := {zeta := false}) only + -- [not_and_or, not_or, Classical.not_forall, not_ne_iff, not_imp] at hkl + -- obtain ⟨a, hka, hka', hla, hla'⟩ | ⟨⟨a, hka, hla⟩, b, hlb, hkb⟩ := hkl + -- · refine le_trans ?_ (mul_le_mul' (card_mono $ inter_subset_left _ $ a • H) $ + -- card_mono $ inter_subset_left _ $ a • H) + -- rw [hk, hl, mul_comm (k a), mul_mul_mul_comm, mul_comm (k a)] + -- refine le_trans ?_ + -- (mul_le_mul' (Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hls _).lt_of_ne hla').ne' hla) $ + -- Nat.add_sub_one_le_mul (tsub_pos_of_lt $ (hkt _).lt_of_ne hka').ne' hka) + -- rw [tsub_add_cancel_of_le (hkt _), tsub_add_cancel_of_le (hls _)] + -- refine' + -- mul_le_mul' (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ b • H) + -- (tsub_le_self.trans $ le_trans _ $ card_mono $ inter_subset_left _ $ a • H) + -- · rw [hk, hlb, tsub_zero] + -- exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hkb) + -- · rw [hl, hka, tsub_zero] + -- exact le_mul_of_one_le_left' (pos_iff_ne_zero.2 hla) -- Lemma 3.4 in Ruzsa's notes @[to_additive] @@ -247,8 +249,8 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) : /-- **Kneser's multiplication lemma**: A lower bound on the size of `s * t` in terms of its stabilizer. -/ -@[to_additive - "**Kneser's addition lemma**: A lower bound on the size of `s + t` in terms of its\nstabilizer."] +@[to_additive "**Kneser's addition lemma**: A lower bound on the size of `s + t` in terms of its +stabilizer."] lemma mul_kneser' (s t : Finset α) : (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card := by @@ -263,10 +265,10 @@ lemma mul_kneser' (s t : Finset α) : _ rw [mul_mulStab_mul_mul_mul_mulStab_mul] -/-- The strict version of **Kneser's multiplication lemma**. If the LHS of `finset.mul_kneser` +/-- The strict version of **Kneser's multiplication theorem**. If the LHS of `Finset.mul_kneser` does not equal the RHS, then it is in fact much smaller. -/ -@[to_additive - "The strict version of **Kneser's addition lemma**. If the LHS of\n`finset.add_kneser` does not equal the RHS, then it is in fact much smaller."] +@[to_additive "The strict version of **Kneser's addition theorem**. If the LHS of +`Finset.add_kneser` does not equal the RHS, then it is in fact much smaller."] lemma mul_strict_kneser' (h : (s * (s * t).mulStab).card + (t * (s * t).mulStab).card < diff --git a/LeanCamCombi/Kneser/MulStab.lean b/LeanCamCombi/Kneser/MulStab.lean index 930e57c597..de880acbb0 100644 --- a/LeanCamCombi/Kneser/MulStab.lean +++ b/LeanCamCombi/Kneser/MulStab.lean @@ -38,14 +38,14 @@ def mulStab (s : Finset α) : Finset α := (s / s).filter fun a ↦ a • s = s lemma mem_mulStab (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s = s := by rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp] obtain ⟨b, hb⟩ := hs - exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel'' _ _⟩ + exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel_right _ _⟩ @[to_additive] lemma mulStab_subset_div : s.mulStab ⊆ s / s := filter_subset _ _ @[to_additive] lemma mulStab_subset_div_right (ha : a ∈ s) : s.mulStab ⊆ s / {a} := by - refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel'' _ _⟩ + refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel_right _ _⟩ rw [mem_mulStab ⟨a, ha⟩] at hb rw [← hb] exact smul_mem_smul_finset ha diff --git a/LeanCamCombi/LittlewoodOfford.lean b/LeanCamCombi/LittlewoodOfford.lean index 6b9c73d237..8db953b6c0 100644 --- a/LeanCamCombi/LittlewoodOfford.lean +++ b/LeanCamCombi/LittlewoodOfford.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ import Mathlib.Analysis.NormedSpace.HahnBanach.Extension -import Mathlib.Combinatorics.DoubleCounting +import Mathlib.Combinatorics.Enumerative.DoubleCounting import Mathlib.Order.Partition.Finpartition /-! diff --git a/LeanCamCombi/Mathlib/Combinatorics/Colex.lean b/LeanCamCombi/Mathlib/Combinatorics/Colex.lean index 94c0253d9f..c10542f366 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/Colex.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/Colex.lean @@ -57,7 +57,7 @@ lemma lt_iff_exists_forall_lt_mem_iff_mem : simp only [lt_iff_exists_forall_lt] refine ⟨fun h ↦ ?_, ?_⟩ · let u := (t \ s).filter fun w ↦ ∀ a ∈ s, a ∉ t → a < w - have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [and_assoc] + have mem_u {w : α} : w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w := by simp [u, and_assoc] have hu : u.Nonempty := h.imp fun _ ↦ mem_u.2 let m := max' _ hu have ⟨hmt, hms, hm⟩ : m ∈ t ∧ m ∉ s ∧ ∀ a ∈ s, a ∉ t → a < m := mem_u.1 $ max'_mem _ _ diff --git a/LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean b/LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean index 68b344e53e..54ecf1aa80 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean @@ -57,7 +57,9 @@ lemma sumset_contains_n (hA : 0 ∈ A) (hB : 0 ∈ B) (hc : n ≤ countelements apply h have lem1 : ((Ioo 0 n).filter (· ∈ {n} - B)).card = countelements B (n - 1) := by rw [countelements] - have hfim : Finset.image (n - ·) (filter (fun x ↦ x ∈ B) (Ioo 0 n)) = (filter (fun x ↦ x ∈ {n} - B) (Ioo 0 n)) := by ext; aesop + have hfim : + (filter (fun x ↦ x ∈ B) (Ioo 0 n)).image (n - ·) = + (filter (fun x ↦ x ∈ {n} - B) (Ioo 0 n)) := by ext; aesop rw [← hfim, card_image_of_injOn] congr exact (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 hn1).symm @@ -79,16 +81,21 @@ lemma sumset_contains_n (hA : 0 ∈ A) (hB : 0 ∈ B) (hc : n ≤ countelements -- have hip : 0 ≤ Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := by positivity have hun1 : Finset.card ((Ioo 0 n).filter (· ∈ A) ∪ (Ioo 0 n).filter (· ∈ {n} - B)) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ (n - 1) - + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := add_le_add hun le_rfl - have hip0 : n ≤ (n - 1) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := le_trans hc hun1 + + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) := + add_le_add hun le_rfl + have hip0 : n ≤ (n - 1) + ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)).card := + le_trans hc hun1 by_contra! hip - have hip1 : (n - 1) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ (n - 1) := add_le_add le_rfl hip + have hip1 : + (n - 1) + Finset.card ((Ioo 0 n).filter (· ∈ A) ∩ (Ioo 0 n).filter (· ∈ {n} - B)) ≤ n - 1 := + add_le_add le_rfl hip have hnn : n ≤ (n - 1) := le_trans hip0 hip1 rw [← not_lt] at hnn apply hnn rw [propext (Nat.lt_iff_le_pred hn1)] rwa [← Finset.card_pos] - simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Ioo, and_imp, Set.singleton_sub, Set.mem_image, ne_eq] at lem3 -- set is nonempty iff ? + simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Ioo, and_imp, Set.singleton_sub, + Set.mem_image, ne_eq] at lem3 -- set is nonempty iff ? have lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty := by rw [← filter_and, ← coe_nonempty, coe_filter, Set.setOf_and, Set.setOf_and, Set.setOf_mem_eq, Set.inter_comm] at lem3 @@ -177,10 +184,13 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n := by -- simp only [tsub_pos_iff_lt, Set.sep_and, Set.iUnion_coe_set] --have hab (a : A) (b : B) : 0 < (b : ℕ) → (b : ℕ) ≤ (next_elm A a n) - a → (a : ℕ) + (b : ℕ) ∈ (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) := by sorry - have hcc (a : A) : 1 + countelements B (next_elm A a n - a - 1) ≤ countelements {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} n := by + have hcc (a : A) : + 1 + countelements B (next_elm A a n - a - 1) ≤ + countelements {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} n := by sorry - have hax (a x : A) : a ≠ x → {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} ∩ {c ∈ A + B | 0 < c - x ∧ (c : ℕ) ≤ (next_elm A x n)} = ∅ := by sorry - -- intro hh + have hax (a x : A) (hh : a ≠ x) : + {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} ∩ + {c ∈ A + B | 0 < c - x ∧ (c : ℕ) ≤ next_elm A x n} = ∅ := by sorry -- by_contra! hin -- rw? at hin -- have hcount : ∑ a in A, (1 + countelements B (next_elm A a n - a - 1)) ≤ countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n := by sorry @@ -212,15 +222,15 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) rw [hc3] at hc2 exact le_trans hc2 ht -lemma schnirelmannDensity_for_two (A B : Set ℕ) : (0 ∈ A) → (0 ∈ B) → - (1 - schnirelmannDensity (A + B)) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B) := by +lemma schnirelmannDensity_for_two (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B) : + 1 - schnirelmannDensity (A + B) ≤ + (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B) := by let α := schnirelmannDensity A have halpha : α = schnirelmannDensity A := rfl let β := schnirelmannDensity B have hbeta : β = schnirelmannDensity B := rfl let γ := schnirelmannDensity (A + B) have hgamma : γ = schnirelmannDensity (A + B) := rfl - intro hA hB rw [← halpha, ← hbeta, ← hgamma] have h : 1 - γ ≤ 1 - (α + β - α * β) := by rw [sub_le_iff_le_add, add_comm_sub] @@ -237,4 +247,6 @@ lemma schnirelmannDensity_for_two (A B : Set ℕ) : (0 ∈ A) → (0 ∈ B) → -theorem mannTheorem (A B : Set ℕ) : min 1 (schnirelmannDensity A + schnirelmannDensity B) ≤ schnirelmannDensity (A + B) := by sorry +theorem mannTheorem (A B : Set ℕ) : + min 1 (schnirelmannDensity A + schnirelmannDensity B) ≤ schnirelmannDensity (A + B) := by + sorry diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean index 1540c8af23..82bf64ba39 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean @@ -233,7 +233,8 @@ end LabelledCopyCount An important aspect of graph containment is that we can remove not too many edges from a graph `H` to get a graph `H'` that doesn't contain `G`. -`SimpleGraph.kill G H` is a subgraph of `H` where an edge was removed from each copy of `G` in `H`. by construction, it doesn't contain `G` and has at most the number of copies of `G` edges less than +`SimpleGraph.kill G H` is a subgraph of `H` where an edge was removed from each copy of `G` in `H`. +By construction, it doesn't contain `G` and has at most the number of copies of `G` edges less than `H` -/ diff --git a/LeanCamCombi/Mathlib/Data/List/Basic.lean b/LeanCamCombi/Mathlib/Data/List/Basic.lean index b609081efe..736cddafb0 100644 --- a/LeanCamCombi/Mathlib/Data/List/Basic.lean +++ b/LeanCamCombi/Mathlib/Data/List/Basic.lean @@ -31,6 +31,6 @@ attribute [simp] nil_subperm lemma subperm_cons_self : l <+~ a :: l := ⟨l, Perm.refl _, sublist_cons _ _⟩ @[simp] lemma subperm_nil : l <+~ [] ↔ l = [] := - ⟨fun h ↦ length_eq_zero.1 $ le_bot_iff.1 h.length_le, by rintro rfl; rfl⟩ + ⟨fun h ↦ length_eq_zero.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩ end List diff --git a/LeanCamCombi/Mathlib/Data/List/DropRight.lean b/LeanCamCombi/Mathlib/Data/List/DropRight.lean index a0fdcb0914..d15f304203 100644 --- a/LeanCamCombi/Mathlib/Data/List/DropRight.lean +++ b/LeanCamCombi/Mathlib/Data/List/DropRight.lean @@ -8,7 +8,7 @@ variable {α : Type*} {l l' l₀ l₁ l₂ : List α} {a b : α} {m n : ℕ} lemma rtake_suffix (n : ℕ) (l : List α) : l.rtake n <:+ l := drop_suffix _ _ lemma length_rtake (n : ℕ) (l : List α) : (l.rtake n).length = min n l.length := - (length_drop _ _).trans $ by rw [tsub_tsub_eq_min, min_comm] + (length_drop _ _).trans $ by rw [Nat.sub_sub_eq_min, min_comm] @[simp] lemma take_reverse (n : ℕ) (l : List α) : l.reverse.take n = (l.rtake n).reverse := by rw [rtake_eq_reverse_take_reverse, reverse_reverse] @@ -40,10 +40,10 @@ lemma take_prefix_take (h : m ≤ n) : l.take m <+: l.take n := by lemma drop_suffix_drop (h : m ≤ n) : l.drop n <:+ l.drop m := sorry lemma rtake_suffix_rtake (h : m ≤ n) : l.rtake m <:+ l.rtake n := - drop_suffix_drop $ tsub_le_tsub_left h _ + drop_suffix_drop $ Nat.sub_le_sub_left h _ lemma rdrop_prefix_rdrop (h : m ≤ n) : l.rdrop n <+: l.rdrop m := - take_prefix_take $ tsub_le_tsub_left h _ + take_prefix_take $ Nat.sub_le_sub_left h _ protected lemma IsPrefix.take (hl : l <+: l') (h : l.length ≤ n) : l <+: l'.take n := by rw [hl.eq_take]; exact take_prefix_take h @@ -90,6 +90,6 @@ lemma Subperm.exists_intermediate (hl : l₀ <+~ l₂) (h₀ : l₀.length ≤ n exact ⟨l₁, ⟨_, hl₀, h₀₁⟩, h₁₂.subperm, hn⟩ lemma exists_subperm_length_eq (hn : n ≤ l.length) : ∃ l', l' <+~ l ∧ l'.length = n := by - simpa using nil_subperm.exists_intermediate bot_le hn + simpa using nil_subperm.exists_intermediate (Nat.zero_le _) hn end List diff --git a/LeanCamCombi/Mathlib/Data/Multiset/Basic.lean b/LeanCamCombi/Mathlib/Data/Multiset/Basic.lean index 3056521101..309a0ba087 100644 --- a/LeanCamCombi/Mathlib/Data/Multiset/Basic.lean +++ b/LeanCamCombi/Mathlib/Data/Multiset/Basic.lean @@ -19,11 +19,11 @@ lemma exists_intermediate (hst : s ≤ t) (hs : card s ≤ n) (ht : n ≤ card t exact ⟨l₁, h⟩ lemma exists_le_card_eq (hn : n ≤ card s) : ∃ t, t ≤ s ∧ card t = n := by - simpa using exists_intermediate (zero_le _) bot_le hn + simpa using exists_intermediate (zero_le _) (Nat.zero_le _) hn variable [DecidableEq α] lemma le_card_sub : card s - card t ≤ card (s - t) := - tsub_le_iff_left.2 $ (card_mono le_add_tsub).trans_eq $ card_add _ _ + Nat.sub_le_iff_le_add'.2 $ (card_mono le_add_tsub).trans_eq $ card_add _ _ end Multiset diff --git a/LeanCamCombi/Mathlib/Data/Nat/Order/Lemmas.lean b/LeanCamCombi/Mathlib/Data/Nat/Defs.lean similarity index 56% rename from LeanCamCombi/Mathlib/Data/Nat/Order/Lemmas.lean rename to LeanCamCombi/Mathlib/Data/Nat/Defs.lean index 3daa6d15bd..a65f443aa8 100644 --- a/LeanCamCombi/Mathlib/Data/Nat/Order/Lemmas.lean +++ b/LeanCamCombi/Mathlib/Data/Nat/Defs.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Nat.Order.Lemmas +import Mathlib.Data.Nat.Defs namespace Nat variable {a b : ℕ} @@ -6,7 +6,8 @@ variable {a b : ℕ} lemma eq_of_dvd_of_lt_two_mul (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b := by obtain ⟨_ | _ | c, rfl⟩ := hdvd · simp at ha - · exact mul_one _ - · cases hlt.not_le ((mul_comm _ _).trans_le $ mul_le_mul_left' (by omega) _) + · exact Nat.mul_one _ + · rw [Nat.mul_comm] at hlt + cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega)) end Nat diff --git a/LeanCamCombi/Mathlib/Data/Subtype.lean b/LeanCamCombi/Mathlib/Data/Subtype.lean deleted file mode 100644 index 095567dbe7..0000000000 --- a/LeanCamCombi/Mathlib/Data/Subtype.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Mathlib.Data.Subtype - -namespace Subtype -variable {α : Type*} {p : α → Prop} {a b : {a // p a}} - -lemma coe_ne_coe : (a : α) ≠ b ↔ a ≠ b := coe_inj.not - -end Subtype diff --git a/LeanCamCombi/Mathlib/Order/Sublattice.lean b/LeanCamCombi/Mathlib/Order/Sublattice.lean index 3bbc903a10..16af967be0 100644 --- a/LeanCamCombi/Mathlib/Order/Sublattice.lean +++ b/LeanCamCombi/Mathlib/Order/Sublattice.lean @@ -223,7 +223,8 @@ def eqLocus (f g : α →* M) : Sublattice α := lemma eqLocus_same (f : LatticeHom α β) : f.eqLocus f = ⊤ := SetLike.ext fun _ ↦ eq_self_iff_true _ -/-- If two monoid homomorphisms are equal on a set, then they are equal on its Sublattice closure. -/ +/-- If two monoid homomorphisms are equal on a set, then they are equal on its sublattice +closure. -/ lemma eqOn_closure {f g : α →* M} {s : Set α} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) := show closure s ≤ f.eqLocus g from (closure_le _).2 h @@ -235,7 +236,8 @@ lemma eq_of_eqOn_dense {s : Set α} (hs : closure s = ⊤) {f g : α →* M} (h end EqLocus -lemma closure_preimage_le (f : LatticeHom α β) (s : Set β) : closure (f ⁻¹' s) ≤ (closure s).comap f := +lemma closure_preimage_le (f : LatticeHom α β) (s : Set β) : + closure (f ⁻¹' s) ≤ (closure s).comap f := (closure_le _).2 fun a hx ↦ by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx /-- The image under a monoid homomorphism of the Sublattice generated by a set equals the Sublattice @@ -290,7 +292,8 @@ lemma comap_map_eq (L : Sublattice α) : comap f (map f L) = L ⊔ f.ker := by rw [← mul_inv_cancel_left y a] exact mul_mem_sup hy (by simp [mem_ker, hy']) -lemma map_comap_eq_self {f : LatticeHom α β} {L : Sublattice β} (h : L ≤ f.range) : map f (comap f L) = L := by rwa [map_comap_eq, inf_eq_right] +lemma map_comap_eq_self {f : LatticeHom α β} {L : Sublattice β} (h : L ≤ f.range) : + map f (comap f L) = L := by rwa [map_comap_eq, inf_eq_right] lemma map_comap_eq_self_of_surjective {f : LatticeHom α β} (h : Surjective f) (L : Sublattice β) : map f (comap f L) = L := @@ -310,14 +313,15 @@ lemma comap_lt_comap_of_surjective {f : LatticeHom α β} {L L : Sublattice β} lemma comap_injective {f : LatticeHom α β} (h : Surjective f) : Injective (comap f) := fun L L ↦ by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self] -lemma comap_map_eq_self {f : LatticeHom α β} (h : f.ker ≤ L) : comap f (map f L) = L := by rwa [comap_map_eq, sup_eq_left] +lemma comap_map_eq_self {f : LatticeHom α β} (h : f.ker ≤ L) : comap f (map f L) = L := by + rwa [comap_map_eq, sup_eq_left] lemma comap_map_eq_self_of_injective {f : LatticeHom α β} (h : Injective f) (L : Sublattice α) : comap f (map f L) = L := comap_map_eq_self (((ker_eq_bot_iff _).mpr h).symm ▸ bot_le) -lemma map_le_map_iff {f : LatticeHom α β} {L M : Sublattice α} : L.map f ≤ L.map f ↔ L ≤ L ⊔ f.ker := by - rw [map_le_iff_le_comap, comap_map_eq] +lemma map_le_map_iff {f : LatticeHom α β} {L M : Sublattice α} : + L.map f ≤ L.map f ↔ L ≤ L ⊔ f.ker := by rw [map_le_iff_le_comap, comap_map_eq] lemma map_le_map_iff' {f : LatticeHom α β} {L M : Sublattice α} : L.map f ≤ L.map f ↔ L ⊔ f.ker ≤ L ⊔ f.ker := by @@ -326,7 +330,8 @@ lemma map_le_map_iff' {f : LatticeHom α β} {L M : Sublattice α} : lemma map_eq_map_iff {f : LatticeHom α β} {L M : Sublattice α} : L.map f = L.map f ↔ L ⊔ f.ker = L ⊔ f.ker := by simp only [le_antisymm_iff, map_le_map_iff'] -lemma map_eq_range_iff {f : LatticeHom α β} : L.map f = f.range ↔ Codisjoint L f.ker := by rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq] +lemma map_eq_range_iff {f : LatticeHom α β} : L.map f = f.range ↔ Codisjoint L f.ker := by + rw [f.range_eq_map, map_eq_map_iff, codisjoint_iff, top_sup_eq] lemma map_le_map_iff_of_injective {f : LatticeHom α β} (hf : Injective f) {L M : Sublattice α} : L.map f ≤ L.map f ↔ L ≤ L := by rw [map_le_iff_le_comap, comap_map_eq_self_of_injective hf] diff --git a/LeanCamCombi/MinkowskiCaratheodory.lean b/LeanCamCombi/MinkowskiCaratheodory.lean index 061e4abf98..d9c41ae5d2 100644 --- a/LeanCamCombi/MinkowskiCaratheodory.lean +++ b/LeanCamCombi/MinkowskiCaratheodory.lean @@ -14,7 +14,8 @@ open Set open scoped Affine BigOperators Classical --TODO: Generalise to LCTVS -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s B : Set E} +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} + {s B : Set E} /-- The **Minkowski-Carathéodory Theorem**. A compact convex set in a finite dimensional space is the convex hull of its extreme points. -/ diff --git a/LeanCamCombi/SimplicialComplex/Simplex.lean b/LeanCamCombi/SimplicialComplex/Simplex.lean index c2ec3c4be6..9ecb0cf21e 100644 --- a/LeanCamCombi/SimplicialComplex/Simplex.lean +++ b/LeanCamCombi/SimplicialComplex/Simplex.lean @@ -33,7 +33,8 @@ def combiInterior (s : Finset E) : Set E := convexHull 𝕜 ↑s \ combiFrontier variable {𝕜} -lemma mem_combiFrontier_iff : x ∈ combiFrontier 𝕜 s ↔ ∃ t, t ⊂ s ∧ x ∈ convexHull 𝕜 (t : Set E) := by simp [combiFrontier] +lemma mem_combiFrontier_iff : + x ∈ combiFrontier 𝕜 s ↔ ∃ t, t ⊂ s ∧ x ∈ convexHull 𝕜 (t : Set E) := by simp [combiFrontier] lemma combiFrontier_subset_convexHull : combiFrontier 𝕜 s ⊆ convexHull 𝕜 ↑s := iUnion₂_subset fun _t ht => convexHull_mono ht.1 @@ -270,7 +271,7 @@ lemma subset_closure_combiInterior (hs : AffineIndependent ℝ ((↑) : s → E) -- simp [hx] · apply centroid_weights · simp [Finset.sum_boole, Finset.filter_eq, hx] - · simp only [add_sub_cancel'_right] + · simp only [add_sub_cancel] apply Finset.sum_centroidWeights_eq_one_of_nonempty ℝ _ hsnonempty · rw [tendsto_iff_norm_sub_tendsto_zero] convert_to Filter.Tendsto (fun e : ℕ => ((e : ℝ) + 2)⁻¹ * ‖s.centroid ℝ id - x‖) Filter.atTop _ @@ -283,7 +284,7 @@ lemma subset_closure_combiInterior (hs : AffineIndependent ℝ ((↑) : s → E) suffices Filter.Tendsto (fun e : ℕ => (↑(e + 2) : ℝ)⁻¹) Filter.atTop (nhds 0) by simpa using this.mul_const _ refine' tendsto_inv_atTop_zero.comp _ - rw [tendsto_nat_cast_atTop_iff] + rw [tendsto_natCast_atTop_iff] apply Filter.tendsto_add_atTop_nat variable [T2Space E] diff --git a/LeanCamCombi/SliceRank.lean b/LeanCamCombi/SliceRank.lean index b73fb5cfe3..029a868f6d 100644 --- a/LeanCamCombi/SliceRank.lean +++ b/LeanCamCombi/SliceRank.lean @@ -21,7 +21,8 @@ inductive HasSliceRankLE : ℕ → ((∀ i, α i) → R) → Prop lemma hasSliceRankLE_succ : HasSliceRankLE (n + 1) f ↔ ∃ f' i, ∃ (g : α i → R) (h : (∀ j ≠ i, α j) → R), HasSliceRankLE n f' ∧ f = f' + fun x ↦ g (x i) * h fun j _ ↦ x j := by - rw [hasSliceRankLE_iff]; aesop + rw [hasSliceRankLE_iff] + sorry -- aesop lemma hasSliceRankLE_one : HasSliceRankLE 1 f ↔ ∃ i, ∃ (g : α i → R) (h : (∀ j ≠ i, α j) → R), diff --git a/LeanCamCombi/SylvesterChvatal.lean b/LeanCamCombi/SylvesterChvatal.lean index 2651242bd6..fc34ecb1b5 100644 --- a/LeanCamCombi/SylvesterChvatal.lean +++ b/LeanCamCombi/SylvesterChvatal.lean @@ -299,7 +299,7 @@ lemma exists_min_dist (V : Type*) [MetricSpace V] [Finite V] : cases subsingleton_or_nontrivial V · exact ⟨1, zero_lt_one, fun x y ↦ by simp [Subsingleton.elim x y]⟩ let S : Set (V × V) := (Set.diagonal V)ᶜ - have : S.Nonempty := have ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨(x, y), by simp [hxy]⟩ + have : S.Nonempty := have ⟨x, y, hxy⟩ := exists_pair_ne V; ⟨(x, y), by simp [S, hxy]⟩ obtain ⟨⟨x, y⟩, (hxy : x ≠ y), h⟩ := S.toFinite.exists_minimal_wrt (Function.uncurry dist) _ this simp only [Set.mem_compl_iff, Set.mem_diagonal_iff, Function.uncurry_apply_pair, Prod.forall] at h exact ⟨dist x y, by simp [hxy], fun a b hab => le_of_not_lt (fun h' => h'.ne' (h _ _ hab h'.le))⟩ @@ -405,8 +405,8 @@ lemma case1 {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : SimpleTriangle a b have hP'₂ : P'.pathLength ≤ (a₁ :: b :: d :: []).pathLength := ha₁ ▸ hP'lt.le.trans (hPmin _ (abd_special habc hacd hbd' hbd)) have hP'₃ : P'.Chain' (· ≠ ·) := by - simp only [ne_eq, List.chain'_cons] at hPc - simp only [List.chain'_cons, and_true, ← ha₁, hb₁₂.ne12, true_and, not_false_eq_true, ne_eq, + simp only [P', ne_eq, List.chain'_cons] at hPc + simp only [P', List.chain'_cons, and_true, ← ha₁, hb₁₂.ne12, true_and, not_false_eq_true, ne_eq, ha₃b₁₂.symm, ha₃b₂₃.symm, hPc.2.2, hP'₁.2] simp only [List.Special, hP'₁, List.getLast_cons_cons, List.getLast_cons_cons, hPd, hP'₂, hP'₃, ← ha₁, and_true, true_and, not_or, not_not] at hP'ns @@ -456,8 +456,8 @@ lemma case2 {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : SimpleTriangle a b have hP'₂ : P'.pathLength ≤ (a₁ :: b :: d :: []).pathLength := ha₁ ▸ hP'lt.le.trans (hPmin _ (abd_special habc hacd hbd' hbd)) have hP'₃ : P'.Chain' (· ≠ ·) := by - simp only [ne_eq, List.chain'_cons] at hPc - simp only [List.chain'_cons, and_true, ← ha₁, true_and, not_false_eq_true, ne_eq, + simp only [P', ne_eq, List.chain'_cons] at hPc + simp only [P', List.chain'_cons, and_true, ← ha₁, true_and, not_false_eq_true, ne_eq, ha₃b₂₃.symm, hPc.2.2, hP'₁.2, hP'₁.1] simp only [List.Special, hP'₁, List.getLast_cons_cons, List.getLast_cons_cons, hPd, hP'₂, hP'₃, ← ha₁, and_true, true_and, not_or, not_not] at hP'ns @@ -510,8 +510,8 @@ lemma case3 {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : SimpleTriangle a b have hP'₂ : P'.pathLength ≤ (a₁ :: b :: d :: []).pathLength := ha₁ ▸ hP'lt.le.trans (hPmin _ (abd_special habc hacd hbd' hbd)) have hP'₃ : P'.Chain' (· ≠ ·) := by - simp only [ne_eq, List.chain'_cons] at hPc - simp only [List.chain'_cons, and_true, ← ha₁, hb₁₂.ne12, true_and, not_false_eq_true, ne_eq, + simp only [P', ne_eq, List.chain'_cons] at hPc + simp only [P', List.chain'_cons, and_true, ← ha₁, hb₁₂.ne12, true_and, not_false_eq_true, ne_eq, ha₃b₁₂.symm, hPc.2.2, hP'₁.2] simp only [List.Special, hP'₁, List.getLast_cons_cons, List.getLast_cons_cons, hPd, hP'₂, hP'₃, ← ha₁, and_true, true_and, not_or, not_not] at hP'ns diff --git a/LeanCamCombi/VanDenBergKesten.lean b/LeanCamCombi/VanDenBergKesten.lean index ae55eedd84..3778a26c74 100644 --- a/LeanCamCombi/VanDenBergKesten.lean +++ b/LeanCamCombi/VanDenBergKesten.lean @@ -54,7 +54,7 @@ lemma certificator_subset_inter : s □ t ⊆ s ∩ t := filter_subset _ _ lemma certificator_subset_disjSups : s □ t ⊆ s ○ t := by simp_rw [subset_iff, mem_certificator, mem_disjSups] rintro x ⟨u, v, huv, hu, hv⟩ - refine' ⟨x ⊓ u, hu inf_right_idem.symm, x ⊓ v, hv inf_right_idem.symm, + refine' ⟨x ⊓ u, hu (inf_right_idem _ _).symm, x ⊓ v, hv (inf_right_idem _ _).symm, huv.disjoint.mono inf_le_right inf_le_right, _⟩ rw [←inf_sup_left, huv.codisjoint.eq_top, inf_top_eq] diff --git a/lake-manifest.json b/lake-manifest.json index 9dd96bd2b0..318736c59e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,16 +4,16 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "a7543d1a6934d52086971f510e482d743fe30cf3", + "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "fd760831487e6835944e7eeed505522c9dd47563", + "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,25 +22,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b", + "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.6.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "16cae05860b208925f54e5581ec5fd264823440c", + "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.29", + "inputRev": "v0.0.30", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec", + "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f", + "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "dad5e8c449e037e72c9890baa70a85b2a307db68", + "rev": "d3917c3f6a5fb4a7f8e7e5da96bbb7f85bbd7bb5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -76,7 +76,7 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "5b096942260d7805cc90bacf4ea4a0f8e9700ccb", + "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -94,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "780bbec107cba79d18ec55ac2be3907a77f27f98", + "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 50262040de..9ad304042c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.6.0 +leanprover/lean4:v4.7.0