From db6f91763fac5041df043966429612977abe760d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 9 Jun 2024 08:09:08 +0000 Subject: [PATCH] Bump mathlib --- LeanCamCombi/Kneser/Kneser.lean | 40 +++++++++--------- LeanCamCombi/Kneser/KneserRuzsa.lean | 4 +- LeanCamCombi/Kneser/Mathlib.lean | 3 +- LeanCamCombi/Kneser/MulStab.lean | 13 +++++- LeanCamCombi/KruskalKatona.lean | 42 +++++++++---------- .../Mathlib/Analysis/Convex/Extreme.lean | 2 +- .../Combinatorics/SimpleGraph/Degree.lean | 2 +- LeanCamCombi/Mathlib/Data/Finset/Lattice.lean | 4 +- .../Mathlib/Order/Partition/Finpartition.lean | 2 +- LeanCamCombi/SimplicialComplex/Basic.lean | 6 +-- LeanCamCombi/SimplicialComplex/Finite.lean | 2 +- LeanCamCombi/SimplicialComplex/Simplex.lean | 4 +- lake-manifest.json | 16 +++---- lean-toolchain | 2 +- 14 files changed, 75 insertions(+), 67 deletions(-) diff --git a/LeanCamCombi/Kneser/Kneser.lean b/LeanCamCombi/Kneser/Kneser.lean index f7996bdd0e..724b5e1d96 100644 --- a/LeanCamCombi/Kneser/Kneser.lean +++ b/LeanCamCombi/Kneser/Kneser.lean @@ -49,7 +49,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty) have hxymem : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy apply subset_trans (mulStab_subset_div_right hxymem) have : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (x * y) • C.mulStab := by - apply subset_trans (mul_subset_mul (inter_subset_right s _) (inter_subset_right t _)) + apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right) rw [smul_mul_smul] rw [← hac, ← had, smul_mul_smul, smul_assoc] apply smul_finset_subset_smul_finset @@ -67,7 +67,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty) mul_assoc, ← mul_assoc, mul_assoc _ a b, inv_mul_self (a * b), one_mul, ← smul_eq_mul, smul_assoc, smul_mulStab hc, smul_mulStab hd] have hsub : s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊆ (a * b) • C.mulStab := by - apply subset_trans (mul_subset_mul (inter_subset_right s _) (inter_subset_right t _)) + apply subset_trans (mul_subset_mul inter_subset_right inter_subset_right) simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl] have hxy : x * y ∈ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := mul_mem_mul hx hy rw [this] at hsub @@ -79,7 +79,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty) push_neg refine' ⟨a * c * (b * d), by convert hxy, _⟩ rw [smul_eq_mul, mul_comm, ← smul_eq_mul, hwz] - exact not_mem_mono (mul_subset_mul (inter_subset_left s _) (inter_subset_left t _)) hzst + exact not_mem_mono (mul_subset_mul inter_subset_left inter_subset_left) hzst @[to_additive] lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b • C.mulStab).Nonempty) @@ -93,7 +93,7 @@ lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b ((subset_inter (mulStab_mul_ssubset_mulStab hs₁ ht₁ hab).subset Subset.rfl).trans inter_mulStab_subset_mulStab_union).antisymm' fun x hx => _ - replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono $ subset_union_right _ _).mp hx + replace hx := (mem_mulStab $ (hs₁.mul ht₁).mono subset_union_right).mp hx rw [smul_finset_union] at hx suffices hxC : x ∈ C.mulStab by rw [(mem_mulStab hCne).mp hxC] at hx @@ -119,16 +119,16 @@ lemma mulStab_union (hs₁ : (s ∩ a • C.mulStab).Nonempty) (ht₁ : (t ∩ b rw [mul_mulStab] at hxyC exact hyne.not_disjoint (hC.mono_left $ le_iff_subset.2 hxyC) have hxysub : (x * y) • C.mulStab ⊆ s ∩ a • C.mulStab * (t ∩ b • C.mulStab) := - hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ (subset_union_left _ _).trans hx.subset') + hxyC.left_le_of_le_sup_left (hxyCsubC.trans $ subset_union_left.trans hx.subset') suffices s ∩ a • C.mulStab * (t ∩ b • C.mulStab) ⊂ (a * b) • C.mulStab by have := (card_le_card hxysub).not_lt ((card_lt_card this).trans_eq ?_) cases this simp_rw [card_smul_finset] apply ssubset_of_subset_not_subset - · refine' (mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _)).trans _ + · refine' (mul_subset_mul inter_subset_right inter_subset_right).trans _ simp only [smul_mul_smul, mulStab_mul_mulStab, subset_refl] · contrapose! hab - exact hab.trans (mul_subset_mul (inter_subset_left _ _) (inter_subset_left _ _)) + exact hab.trans (mul_subset_mul inter_subset_left inter_subset_left) @[to_additive] lemma mul_aux1 @@ -184,12 +184,12 @@ lemma disjoint_mul_sub_card_le {a : α} (b : α) {s t C : Finset α} (has : a (s ∩ a • C.mulStab * (s ∩ a • C.mulStab * (t ∩ b • C.mulStab)).mulStab)).card := by rw [card_sdiff (subset_trans (mul_subset_mul_left hst) - (subset_trans (mul_subset_mul_right (inter_subset_right s _)) _)), + (subset_trans (mul_subset_mul_right inter_subset_right) _)), card_smul_finset, Int.ofNat_sub] · apply le_trans (card_le_card (mul_subset_mul_left hst)) apply le_trans (card_le_card inter_mul_subset) - (le_of_le_of_eq (card_le_card (inter_subset_right _ _)) _) + (le_of_le_of_eq (card_le_card inter_subset_right) _) rw [smul_mul_assoc, mulStab_mul_mulStab, card_smul_finset] · simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl] _ ≤ ((s ∪ t) * C.mulStab).card - @@ -241,7 +241,7 @@ lemma inter_mul_sub_card_le {a : α} {s t C : Finset α} (has : a ∈ s) all_goals apply subset_trans (mul_subset_mul_left hst) rw [← union_inter_distrib_right] - refine' subset_trans (mul_subset_mul_right (inter_subset_right _ _)) _ + refine' subset_trans (mul_subset_mul_right inter_subset_right) _ simp only [smul_mul_assoc, mulStab_mul_mulStab, Subset.rfl] _ ≤ ((s ∪ t) * C.mulStab).card - @@ -352,13 +352,13 @@ theorem mul_kneser : simp only [mul_smul_comm, smul_mul_assoc, mulStab_smul, card_smul_finset] at * have hst : (s ∩ t).Nonempty := ⟨_, mem_inter.2 ⟨ha, hc⟩⟩ have hsts : s ∩ t ⊂ s := - ⟨inter_subset_left _ _, not_subset.2 ⟨_, hb, fun h => hbac $ inter_subset_right _ _ h⟩⟩ + ⟨inter_subset_left, not_subset.2 ⟨_, hb, fun h => hbac $ inter_subset_right h⟩⟩ clear! a b set convergent : Set (Finset α) := {C | C ⊆ s * t ∧ (s ∩ t).card + ((s ∪ t) * C.mulStab).card ≤ C.card + C.mulStab.card} have convergent_nonempty : convergent.Nonempty := by refine' ⟨s ∩ t * (s ∪ t), inter_mul_union_subset, (add_le_add_right (card_le_card $ - subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono $ subset_union_left _ _) _).trans $ + subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono subset_union_left) _).trans $ ih (s ∩ t) (s ∪ t) _⟩ exact add_lt_add_of_le_of_lt (card_le_card inter_mul_union_subset) (card_lt_card hsts) let C := argminOn (fun C : Finset α => C.mulStab.card) IsWellFounded.wf _ convergent_nonempty @@ -385,10 +385,10 @@ theorem mul_kneser : set s₂ := s ∩ b • H with hs₂ set t₁ := t ∩ b • H with ht₁ set t₂ := t ∩ a • H with ht₂ - have hs₁s : s₁ ⊆ s := inter_subset_left _ _ - have hs₂s : s₂ ⊆ s := inter_subset_left _ _ - have ht₁t : t₁ ⊆ t := inter_subset_left _ _ - have ht₂t : t₂ ⊆ t := inter_subset_left _ _ + have hs₁s : s₁ ⊆ s := inter_subset_left + have hs₂s : s₂ ⊆ s := inter_subset_left + have ht₁t : t₁ ⊆ t := inter_subset_left + have ht₂t : t₂ ⊆ t := inter_subset_left have has₁ : a ∈ s₁ := mem_inter.mpr ⟨ha, mem_smul_finset.2 ⟨1, one_mem_mulStab.2 hC, mul_one _⟩⟩ have hbt₁ : b ∈ t₁ := mem_inter.mpr ⟨hb, mem_smul_finset.2 ⟨1, one_mem_mulStab.2 hC, mul_one _⟩⟩ have hs₁ne : s₁.Nonempty := ⟨_, has₁⟩ @@ -401,10 +401,10 @@ theorem mul_kneser : have hC₂st : C₂ ⊆ s * t := union_subset hCst (mul_subset_mul hs₂s ht₂t) have hstabH₁ : s₁ * t₁ ⊆ (a * b) • H := by rw [hH, ← mulStab_mul_mulStab C, ← smul_mul_smul] - apply mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _) + apply mul_subset_mul inter_subset_right inter_subset_right have hstabH₂ : s₂ * t₂ ⊆ (a * b) • H := by rw [hH, ← mulStab_mul_mulStab C, ← smul_mul_smul, mul_comm s₂ t₂] - apply mul_subset_mul (inter_subset_right _ _) (inter_subset_right _ _) + apply mul_subset_mul inter_subset_right inter_subset_right have hCst₁ := disjoint_of_subset_right hstabH₁ (disjoint_smul_mulStab hCst hab) have hCst₂ := disjoint_of_subset_right hstabH₂ (disjoint_smul_mulStab hCst hab) have hst₁ : (s₁ * t₁).card + s₁.card < (s * t).card + s.card := @@ -461,8 +461,8 @@ theorem mul_kneser : conv_lhs => rw [← card_union_of_disjoint hST, ← card_union_of_disjoint hSTst, ← mul_one (s ∪ t)] refine' card_le_card (union_subset (union_subset _ _) $ mul_subset_mul_left $ one_subset.2 hC.one_mem_mulStab) - · exact hSst.trans ((sdiff_subset _ _).trans $ smul_finset_subset_smul $ mem_union_left _ ha) - · exact hTst.trans ((sdiff_subset _ _).trans $ smul_finset_subset_smul $ mem_union_right _ hb) + · exact hSst.trans (sdiff_subset.trans $ smul_finset_subset_smul $ mem_union_left _ ha) + · exact hTst.trans (sdiff_subset.trans $ smul_finset_subset_smul $ mem_union_right _ hb) have hH₁ne : H₁.Nonempty := (hs₁ne.mul ht₁ne).mulStab have hH₂ne : H₂.Nonempty := (hs₂ne.mul ht₂ne).mulStab -- Now we prove inequality (2) diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean index 9c80a12ed0..c4cbb36aa6 100644 --- a/LeanCamCombi/Kneser/KneserRuzsa.lean +++ b/LeanCamCombi/Kneser/KneserRuzsa.lean @@ -238,11 +238,11 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) : rw [← mul_smul] refine' smul_finset_subset_iff.2 - (inter_eq_left.1 $ eq_of_subset_of_card_le (inter_subset_left _ _) _) + (inter_eq_left.1 $ eq_of_subset_of_card_le inter_subset_left _) rw [← ht'] refine' Nat.find_min' _ - ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans $ subset_union_left _ _, + ⟨_, _, mem_inter.2 ⟨hbt' _, _⟩, (hs' _).trans subset_union_left, (mulDysonETransform.subset _ (s' b, t' b)).trans $ hst' _, (mulDysonETransform.card _ _).trans $ hstcard _, rfl⟩ rwa [mem_inv_smul_finset_iff, smul_eq_mul, inv_mul_cancel_right] diff --git a/LeanCamCombi/Kneser/Mathlib.lean b/LeanCamCombi/Kneser/Mathlib.lean index 0b87970e4b..0f78657f7e 100644 --- a/LeanCamCombi/Kneser/Mathlib.lean +++ b/LeanCamCombi/Kneser/Mathlib.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mantas Bakšys, Yaël Dillies -/ import Mathlib.Algebra.CharP.Basic -import Mathlib.Algebra.Group.Subgroup.Basic -import Mathlib.Data.Finset.Pointwise +import Mathlib.GroupTheory.Coset /-! # For mathlib diff --git a/LeanCamCombi/Kneser/MulStab.lean b/LeanCamCombi/Kneser/MulStab.lean index 4035e814a9..37c7d60538 100644 --- a/LeanCamCombi/Kneser/MulStab.lean +++ b/LeanCamCombi/Kneser/MulStab.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mantas Bakšys, Yaël Dillies -/ import Mathlib.Algebra.Pointwise.Stabilizer +import Mathlib.GroupTheory.GroupAction.Quotient import LeanCamCombi.Kneser.Mathlib import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup @@ -146,7 +147,7 @@ lemma inter_mulStab_subset_mulStab_union : s.mulStab ∩ t.mulStab ⊆ (s ∪ t) obtain rfl | ht := t.eq_empty_or_nonempty · simp intro x hx - rw [mem_mulStab (Finset.Nonempty.mono (subset_union_left s t) hs), smul_finset_union, + rw [mem_mulStab (hs.mono subset_union_left), smul_finset_union, (mem_mulStab hs).mp (mem_of_mem_inter_left hx), (mem_mulStab ht).mp (mem_of_mem_inter_right hx)] @@ -269,7 +270,15 @@ lemma card_mulStab_dvd_card_mulStab (hs : s.Nonempty) (h : s.mulStab ⊆ t.mulSt rw [← coe_subset, coe_mulStab hs, coe_mulStab ht, SetLike.coe_subset_coe] at h letI : Fintype (stabilizer α s) := fintypeStabilizerOfMulStab hs letI : Fintype (stabilizer α t) := fintypeStabilizerOfMulStab ht - convert Subgroup.card_dvd_of_le h using 1 <;> exact ((card_map _).trans card_attach).symm + convert Subgroup.card_dvd_of_le h using 1 + simp [-mem_stabilizer_iff] + change _ = (s.mulStab.attach.map + ⟨Subtype.map id fun _ ↦ (mem_mulStab hs).1, Subtype.map_injective _ injective_id⟩).card + simp + simp [-mem_stabilizer_iff] + change _ = (t.mulStab.attach.map + ⟨Subtype.map id fun _ ↦ (mem_mulStab ht).1, Subtype.map_injective _ injective_id⟩).card + simp /-- A version of Lagrange's theorem. -/ @[to_additive "A version of Lagrange's theorem."] diff --git a/LeanCamCombi/KruskalKatona.lean b/LeanCamCombi/KruskalKatona.lean index f8718efa61..1d8c17eedb 100644 --- a/LeanCamCombi/KruskalKatona.lean +++ b/LeanCamCombi/KruskalKatona.lean @@ -107,7 +107,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) : have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›) have : j ∉ t := mem_compl.1 (min'_mem _ _) have hcard : card s = card (insert j t) := by - rw [card_insert_of_not_mem ‹j ∉ t›, ←‹_ = card t›, card_erase_add_one (min'_mem _ _)] + rw [card_insert_of_not_mem ‹j ∉ t›, ← ‹_ = card t›, card_erase_add_one (min'_mem _ _)] refine' ⟨j, ‹_›, hcard, _⟩ -- Cases on j < k or j = k obtain hjk | r₁ := hjk.lt_or_eq @@ -125,7 +125,7 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) : apply min'_le _ _ (mem_of_mem_erase ‹_›) · rw [r₁]; apply mem_insert_self · apply mem_insert_of_mem - rw [←r₁] at gt + rw [← r₁] at gt by_contra apply (min'_le tᶜ _ _).not_lt gt rwa [mem_compl] @@ -134,14 +134,14 @@ lemma shadow_initSeg [Fintype α] (hs : s.Nonempty) : protected lemma IsInitSeg.shadow [Finite α] (h₁ : IsInitSeg 𝒜 r) : IsInitSeg (∂ 𝒜) (r - 1) := by cases nonempty_fintype α obtain rfl | hr := Nat.eq_zero_or_pos r - · have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ←Finset.card_eq_zero]; exact h₁.1 hs + · have : 𝒜 ⊆ {∅} := fun s hs ↦ by rw [mem_singleton, ← Finset.card_eq_zero]; exact h₁.1 hs have := shadow_monotone this simp only [subset_empty, le_eq_subset, shadow_singleton_empty] at this simp [this] obtain rfl | h𝒜 := 𝒜.eq_empty_or_nonempty · simp obtain ⟨s, rfl, rfl⟩ := h₁.exists_initSeg h𝒜 - rw [shadow_initSeg (card_pos.1 hr), ←card_erase_of_mem (min'_mem _ _)] + rw [shadow_initSeg (card_pos.1 hr), ← card_erase_of_mem (min'_mem _ _)] exact isInitSeg_initSeg end Colex @@ -180,19 +180,19 @@ lemma compression_improved (𝒜 : Finset (Finset α)) (h₁ : UsefulCompression obtain ⟨UVd, same_size, hU, hV, max_lt⟩ := h₁ refine' card_shadow_compression_le _ _ fun x Hx ↦ ⟨min' V hV, min'_mem _ _, _⟩ obtain hU' | hU' := eq_or_lt_of_le (succ_le_iff.2 hU.card_pos) - · rw [←hU'] at same_size - have : erase U x = ∅ := by rw [←Finset.card_eq_zero, card_erase_of_mem Hx, ←hU'] + · rw [← hU'] at same_size + have : erase U x = ∅ := by rw [← Finset.card_eq_zero, card_erase_of_mem Hx, ← hU'] have : erase V (min' V hV) = ∅ := by - rw [←Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ←same_size] + rw [← Finset.card_eq_zero, card_erase_of_mem (min'_mem _ _), ← same_size] rw [‹erase U x = ∅›, ‹erase V (min' V hV) = ∅›] exact isCompressed_self _ _ refine' h₂ ⟨UVd.mono (erase_subset _ _) (erase_subset _ _), _, _, _, _⟩ (card_erase_lt_of_mem Hx) · rw [card_erase_of_mem (min'_mem _ _), card_erase_of_mem Hx, same_size] - · rwa [←card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt] - · rwa [←Finset.card_pos, card_erase_of_mem (min'_mem _ _), ←same_size, tsub_pos_iff_lt] + · rwa [← card_pos, card_erase_of_mem Hx, tsub_pos_iff_lt] + · rwa [← Finset.card_pos, card_erase_of_mem (min'_mem _ _), ← same_size, tsub_pos_iff_lt] · refine' (Finset.max'_subset _ $ erase_subset _ _).trans_lt (max_lt.trans_le $ le_max' _ _ $ mem_erase.2 ⟨(min'_lt_max'_of_card _ _).ne', max'_mem _ _⟩) - rwa [←same_size] + rwa [← same_size] /-- If we're compressed by all useful compressions, then we're an initial segment. This is the other key Kruskal-Katona part. -/ @@ -206,15 +206,15 @@ lemma isInitSeg_of_compressed {ℬ : Finset (Finset α)} {r : ℕ} (h₁ : (ℬ have hU : (A \ B).Nonempty := sdiff_nonempty.2 fun h ↦ hAB $ eq_of_subset_of_card_le h hAB'.ge have hV : (B \ A).Nonempty := sdiff_nonempty.2 fun h ↦ hAB.symm $ eq_of_subset_of_card_le h hAB'.le - have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left (sdiff_subset _ _) + have disj : Disjoint (B \ A) (A \ B) := disjoint_sdiff.mono_left sdiff_subset have smaller : max' _ hV < max' _ hU := by obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV) - · rw [←compress_sdiff_sdiff A B] at hAB hBA + · rw [← compress_sdiff_sdiff A B] at hAB hBA cases hBA.not_lt $ toColex_compress_lt_toColex hlt hAB · exact (disjoint_right.1 disj (max'_mem _ hU) $ heq.symm ▸ max'_mem _ _).elim · assumption refine' hB _ - rw [←(h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq] + rw [← (h₂ _ _ ⟨disj, card_sdiff_comm hAB'.symm, hV, hU, smaller⟩).eq] exact mem_compression.2 (Or.inr ⟨hB, A, hA, compress_sdiff_sdiff _ _⟩) attribute [-instance] Fintype.decidableForallFintype @@ -246,11 +246,11 @@ lemma familyMeasure_compression_lt_familyMeasure {U V : Finset (Fin n)} {hU : U. rw [filter_image, z, image_empty, union_empty] rwa [z, union_empty] at uA rw [familyMeasure, familyMeasure, sum_union compress_disjoint] - conv_rhs => rw [←uA] + conv_rhs => rw [← uA] rw [sum_union (disjoint_filter_filter_neg _ _ _), add_lt_add_iff_left, filter_image, sum_image compress_injOn] refine' sum_lt_sum_of_nonempty ne₂ fun A hA ↦ _ - simp_rw [←sum_image (Fin.val_injective.injOn _)] + simp_rw [← sum_image Fin.val_injective.injOn] rw [geomSum_lt_geomSum_iff_toColex_lt_toColex le_rfl, toColex_image_lt_toColex_image Fin.val_strictMono] exact toColex_compress_lt_toColex h $ q _ hA @@ -359,7 +359,7 @@ lemma lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n) simp_rw [mem_image] rintro _ ⟨a, ha, q⟩ rw [mem_powersetCard] at hA - rw [←q, ←mem_range] + rw [← q, ← mem_range] have := hA.1 ha rwa [mem_attachFin] at this suffices ∂^[i] 𝒞 = powersetCard (r - i) range'k by @@ -371,15 +371,15 @@ lemma lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n) rw [mem_powersetCard] at Ah refine' ⟨BsubA.trans Ah.1, _⟩ symm - rw [Nat.sub_eq_iff_eq_add hir, ←Ah.2, ←card_sdiff_i, ←card_union_of_disjoint disjoint_sdiff, + rw [Nat.sub_eq_iff_eq_add hir, ← Ah.2, ← card_sdiff_i, ← card_union_of_disjoint disjoint_sdiff, union_sdiff_of_subset BsubA] rintro ⟨hBk, hB⟩ have := exists_intermediate_set i ?_ hBk obtain ⟨C, BsubC, hCrange, hcard⟩ := this - rw [hB, ←Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard + rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard refine' ⟨C, _, BsubC, _⟩; rw [mem_powersetCard]; exact ⟨hCrange, hcard⟩ · rw [card_sdiff BsubC, hcard, hB, Nat.sub_sub_self hir] - · rwa [hB, card_attachFin, card_range, ←Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] + · rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] end KK @@ -393,7 +393,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse · convert Nat.zero_le _ rw [Finset.card_eq_zero, eq_empty_iff_forall_not_mem] refine' fun A HA ↦ h𝒜 HA HA _ - rw [disjoint_self_iff_empty, ←Finset.card_eq_zero, ←b] + rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b] exact h₂ HA refine' le_of_not_lt fun size ↦ _ -- Consider 𝒜ᶜˢ = {sᶜ | s ∈ 𝒜} @@ -418,7 +418,7 @@ lemma EKR {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finse have q : n - r - (n - 2 * r) = r := by rw [tsub_right_comm, Nat.sub_sub_self, two_mul] apply Nat.add_sub_cancel - rw [mul_comm, ←Nat.le_div_iff_mul_le' zero_lt_two] + rw [mul_comm, ← Nat.le_div_iff_mul_le' zero_lt_two] exact h₃ rw [q] at kk -- But this gives a contradiction: `n choose r < |𝒜| + |∂^[n-2k] 𝒜ᶜˢ|` diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean b/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean index af453131ea..5a4de767c3 100644 --- a/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean +++ b/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean @@ -68,7 +68,7 @@ variable [NormedLinearOrderedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace -- beurk lemma inter_frontier_self_inter_convexHull_extreme : IsExtreme 𝕜 (closure s) (closure s ∩ frontier (convexHull 𝕜 s)) := by - refine' ⟨inter_subset_left _ _, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩ + refine' ⟨inter_subset_left, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩ sorry sorry diff --git a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean index a471bb683c..384c4183c6 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean @@ -23,7 +23,7 @@ lemma degOn_univ (a : α) : G.degOn univ a = G.degree a := by rw [degOn, degree, lemma degOn_union (h : Disjoint s t) (a) : G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a := by unfold degOn rw [← card_union_of_disjoint, ← union_inter_distrib_right] - exact h.mono (inter_subset_left _ _) (inter_subset_left _ _) + exact h.mono inter_subset_left inter_subset_left -- edges from t to s\t equals edges from s\t to t lemma sum_degOn_comm (s t : Finset α) : ∑ a in s, G.degOn t a = ∑ a in t, G.degOn s a := by diff --git a/LeanCamCombi/Mathlib/Data/Finset/Lattice.lean b/LeanCamCombi/Mathlib/Data/Finset/Lattice.lean index 690f8c2c12..aa8cd1d751 100644 --- a/LeanCamCombi/Mathlib/Data/Finset/Lattice.lean +++ b/LeanCamCombi/Mathlib/Data/Finset/Lattice.lean @@ -14,7 +14,7 @@ variable [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} lemma prod_mk_sup'_sup' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (sup' s hs f, sup' t ht g) = sup' (s ×ˢ t) (hs.product ht) (Prod.map f g) := eq_of_forall_ge_iff fun a ↦ by - simp only [Prod_map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def] + simp only [Prod.map_apply, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def] obtain ⟨a, ha⟩ := hs obtain ⟨b, hb⟩ := ht exact ⟨by aesop, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩ @@ -33,7 +33,7 @@ variable [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} lemma prod_mk_inf'_inf' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (inf' s hs f, inf' t ht g) = inf' (s ×ˢ t) (hs.product ht) (Prod.map f g) := eq_of_forall_le_iff fun a ↦ by - simp only [Prod_map, le_inf'_iff, mem_product, and_imp, Prod.forall, Prod.le_def] + simp only [Prod.map_apply, le_inf'_iff, mem_product, and_imp, Prod.forall, Prod.le_def] obtain ⟨a, ha⟩ := hs obtain ⟨b, hb⟩ := ht exact ⟨by aesop, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩ diff --git a/LeanCamCombi/Mathlib/Order/Partition/Finpartition.lean b/LeanCamCombi/Mathlib/Order/Partition/Finpartition.lean index 3b8e1faa57..23760cd2d0 100644 --- a/LeanCamCombi/Mathlib/Order/Partition/Finpartition.lean +++ b/LeanCamCombi/Mathlib/Order/Partition/Finpartition.lean @@ -12,7 +12,7 @@ def finsetImage {a : Finset α} (P : Finpartition a) (f : α → β) (hf : Injec parts := P.parts.image (image f) supIndep := by rw [supIndep_iff_pairwiseDisjoint, coe_image, - ((image_injective hf).injOn _).pairwiseDisjoint_image] + (image_injective hf).injOn.pairwiseDisjoint_image] simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, Function.onFun, Ne, Function.id_comp, disjoint_image hf] exact P.disjoint diff --git a/LeanCamCombi/SimplicialComplex/Basic.lean b/LeanCamCombi/SimplicialComplex/Basic.lean index c525ce8de7..2120c28877 100644 --- a/LeanCamCombi/SimplicialComplex/Basic.lean +++ b/LeanCamCombi/SimplicialComplex/Basic.lean @@ -35,10 +35,10 @@ lemma disjoint_interiors (hs : s ∈ K) (ht : t ∈ K) (hxs : x ∈ combiInterio classical by_contra h have hst : s ∩ t ⊂ s := by - use inter_subset_left s t + use inter_subset_left intro H - exact hxt.2 $ Set.mem_biUnion ⟨H.trans $ inter_subset_right _ _, fun H2 => h $ (H.trans $ - inter_subset_right _ _).antisymm H2⟩ hxs.1 + exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right, + fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1 refine' hxs.2 (Set.mem_biUnion hst _) push_cast exact K.inter_subset_convexHull hs ht ⟨hxs.1, hxt.1⟩ diff --git a/LeanCamCombi/SimplicialComplex/Finite.lean b/LeanCamCombi/SimplicialComplex/Finite.lean index 318633e6fc..0c8ce56f55 100644 --- a/LeanCamCombi/SimplicialComplex/Finite.lean +++ b/LeanCamCombi/SimplicialComplex/Finite.lean @@ -73,7 +73,7 @@ lemma locallyFinite_iff_mem_finitely_many_faces [DecidableEq E] : have hXYhull := K.inter_subset_convexHull hX hY.1 ⟨hXhull, hY.2⟩ rw [← Finset.coe_inter] at hXYhull by_contra hXY - exact hXbound (mem_combiFrontier_iff.2 ⟨s ∩ t, ⟨Finset.inter_subset_left s t, + exact hXbound (mem_combiFrontier_iff.2 ⟨s ∩ t, ⟨Finset.inter_subset_left, fun hXXY => hXY (Finset.subset_inter_iff.1 hXXY).2⟩, hXYhull⟩) · refine (hx ?_).elim convert finite_empty diff --git a/LeanCamCombi/SimplicialComplex/Simplex.lean b/LeanCamCombi/SimplicialComplex/Simplex.lean index 69501beddd..b67e4e3098 100644 --- a/LeanCamCombi/SimplicialComplex/Simplex.lean +++ b/LeanCamCombi/SimplicialComplex/Simplex.lean @@ -39,7 +39,7 @@ lemma mem_combiFrontier_iff : lemma combiFrontier_subset_convexHull : combiFrontier 𝕜 s ⊆ convexHull 𝕜 ↑s := iUnion₂_subset fun _t ht => convexHull_mono ht.1 -lemma combiInterior_subset_convexHull : combiInterior 𝕜 s ⊆ convexHull 𝕜 ↑s := diff_subset _ _ +lemma combiInterior_subset_convexHull : combiInterior 𝕜 s ⊆ convexHull 𝕜 ↑s := diff_subset @[simp] lemma combiFrontier_empty : combiFrontier 𝕜 (∅ : Finset E) = ∅ := by apply Set.eq_empty_of_subset_empty @@ -79,7 +79,7 @@ lemma simplex_combiInteriors_cover : convexHull 𝕜 ↑s = ⋃ (t) (_ : t ⊆ s obtain ⟨Z, Zt, hZ⟩ := ih exact ⟨_, Zt.trans st.1, hZ⟩ · exact subset_iUnion₂ s Subset.rfl ⟨hx, h⟩ - · exact iUnion₂_subset fun t ht => (diff_subset _ _).trans $ convexHull_mono ht + · exact iUnion₂_subset fun t ht ↦ diff_subset.trans $ convexHull_mono ht end OrderedRing diff --git a/lake-manifest.json b/lake-manifest.json index 31c398c2d3..5c1bf79b73 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,10 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "dfe82086e9904edfc04eb0f5205c85647956897d", + "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0", + "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7", + "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", "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": "6f758e582b2ad1cb121bf88aa1a178e284315af5", + "rev": "ed63385753ed24f23d780e567364a1e001f6ee91", "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": "effd8b8771cfd7ece69db99448168078e113c61f", + "rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -94,7 +94,7 @@ {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "rev": "87022a3314f973c59f130ee581afb4797d7f890e", + "rev": "4e570fed8c4147bdafbd5eada08503ed307252e0", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 78f39e211a..0ba3faf807 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.9.0-rc1