From e9edb776ec1632643dcbbbc692253b319752f49c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 28 Nov 2024 11:06:07 +0000 Subject: [PATCH] Bump mathlib --- LeanCamCombi.lean | 7 - LeanCamCombi/DiscreteDeriv.lean | 4 +- LeanCamCombi/GroupMarking.lean | 2 +- .../GrowthInGroups/ApproximateSubgroup.lean | 10 +- .../GrowthInGroups/CardPowGeneratingSet.lean | 2 +- LeanCamCombi/GrowthInGroups/CardQuotient.lean | 2 +- LeanCamCombi/GrowthInGroups/Lecture2.lean | 6 +- LeanCamCombi/GrowthInGroups/Lecture3.lean | 6 +- LeanCamCombi/Kneser/Kneser.lean | 11 +- LeanCamCombi/Kneser/KneserRuzsa.lean | 2 +- .../Algebra/Group/Pointwise/Finset/Basic.lean | 33 ----- .../Algebra/Group/Pointwise/Set/Basic.lean | 40 ------ .../Algebra/Group/Subgroup/Pointwise.lean | 27 ---- .../Algebra/Group/Submonoid/Pointwise.lean | 1 - .../Mathlib/Algebra/Pointwise/Stabilizer.lean | 91 ------------- .../Combinatorics/Additive/RuzsaCovering.lean | 69 ---------- .../Mathlib/Data/Set/Pointwise/SMul.lean | 44 +----- LeanCamCombi/Mathlib/NumberTheory/Fermat.lean | 47 ------- LeanCamCombi/Mathlib/Order/Chain.lean | 66 --------- LeanCamCombi/Mathlib/Order/Flag.lean | 2 +- .../Mathlib/Order/Monotone/Monovary.lean | 53 -------- LeanCamCombi/Mathlib/Order/Zorn.lean | 3 +- .../Topology/MetricSpace/Pseudo/Defs.lean | 5 - LeanCamCombi/MonovaryOrder.lean | 2 +- lake-manifest.json | 128 +++++++++--------- lean-toolchain | 2 +- 26 files changed, 93 insertions(+), 572 deletions(-) delete mode 100644 LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean delete mode 100644 LeanCamCombi/Mathlib/Algebra/Pointwise/Stabilizer.lean delete mode 100644 LeanCamCombi/Mathlib/Combinatorics/Additive/RuzsaCovering.lean delete mode 100644 LeanCamCombi/Mathlib/NumberTheory/Fermat.lean delete mode 100644 LeanCamCombi/Mathlib/Order/Chain.lean delete mode 100644 LeanCamCombi/Mathlib/Order/Monotone/Monovary.lean delete mode 100644 LeanCamCombi/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 1a2ddaa96e..ede58c0601 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -37,7 +37,6 @@ import LeanCamCombi.Kneser.KneserRuzsa import LeanCamCombi.Kneser.MulStab import LeanCamCombi.LittlewoodOfford import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic -import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Lattice import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise @@ -45,7 +44,6 @@ import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Basic import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Pointwise import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv import LeanCamCombi.Mathlib.Algebra.Order.GroupWithZero.Unbundled -import LeanCamCombi.Mathlib.Algebra.Pointwise.Stabilizer import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas import LeanCamCombi.Mathlib.Algebra.Polynomial.Div import LeanCamCombi.Mathlib.Algebra.Polynomial.Eval.Degree @@ -56,7 +54,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Extreme import LeanCamCombi.Mathlib.Analysis.Convex.Independence import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic -import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment @@ -88,10 +85,7 @@ import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional import LeanCamCombi.Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar import LeanCamCombi.Mathlib.MeasureTheory.Measure.OpenPos -import LeanCamCombi.Mathlib.NumberTheory.Fermat -import LeanCamCombi.Mathlib.Order.Chain import LeanCamCombi.Mathlib.Order.Flag -import LeanCamCombi.Mathlib.Order.Monotone.Monovary import LeanCamCombi.Mathlib.Order.Partition.Finpartition import LeanCamCombi.Mathlib.Order.RelIso.Group import LeanCamCombi.Mathlib.Order.SupClosed @@ -101,7 +95,6 @@ import LeanCamCombi.Mathlib.RingTheory.FinitePresentation import LeanCamCombi.Mathlib.RingTheory.Ideal.Span import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal import LeanCamCombi.Mathlib.RingTheory.Localization.Integral -import LeanCamCombi.Mathlib.Topology.MetricSpace.Pseudo.Defs import LeanCamCombi.MetricBetween import LeanCamCombi.MinkowskiCaratheodory import LeanCamCombi.MonovaryOrder diff --git a/LeanCamCombi/DiscreteDeriv.lean b/LeanCamCombi/DiscreteDeriv.lean index 32ff1d7c9b..f9cbfa4245 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 +import Mathlib.Algebra.Polynomial.Eval.SMul +import Mathlib.Data.Finsupp.Notation open Finset open scoped BigOperators diff --git a/LeanCamCombi/GroupMarking.lean b/LeanCamCombi/GroupMarking.lean index 44bb1e5140..8f57d21a6d 100644 --- a/LeanCamCombi/GroupMarking.lean +++ b/LeanCamCombi/GroupMarking.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ import Mathlib.Analysis.Normed.Group.Basic -import Mathlib.GroupTheory.FreeGroup.Basic +import Mathlib.GroupTheory.FreeGroup.Reduce /-! # Marked groups diff --git a/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean b/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean index 5f91d0bcea..2cb1f2da16 100644 --- a/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean +++ b/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean @@ -1,8 +1,8 @@ import Mathlib.Algebra.Order.BigOperators.Ring.Finset +import Mathlib.Combinatorics.Additive.RuzsaCovering import Mathlib.Combinatorics.Additive.SmallTripling import Mathlib.Tactic.Bound -import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise -import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering +import Mathlib.Algebra.Group.Subgroup.Pointwise import LeanCamCombi.Mathlib.Data.Set.Lattice import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul import LeanCamCombi.GrowthInGroups.SMulCover @@ -117,7 +117,7 @@ lemma pow_inter_pow_covBySMul_sq_inter_sq obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul have := hA.one_le - choose f hf using exists_smul_inter_smul_subset_smul_sq_inter_sq hA.inv_eq_self hB.inv_eq_self + choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩ · calc (#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ) @@ -129,8 +129,10 @@ lemma pow_inter_pow_covBySMul_sq_inter_sq gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> omega _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast - _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A ^ 2 ∩ B ^ 2) := by gcongr; exact hf .. + _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by + gcongr; exact hf .. _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by + simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq] rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2] simp_rw [Finset.mem_coe] diff --git a/LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean b/LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean index 6fe5466f9b..cefaf7af10 100644 --- a/LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean +++ b/LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean @@ -68,7 +68,7 @@ lemma card_pow_strictMonoOn (hX₁ : 1 ∈ X) (hX : X.Nontrivial) : rw [eq_comm, coe_set_eq_one, closure_eq_bot_iff] at hm cases hX.not_subset_singleton hm calc (X : Set G) ^ (n - 1) = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; omega - _ = closure (X : Set G) := by rw [hm, Set.mul_subgroupClosure_pow hX.nonempty.to_set] + _ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set] @[to_additive] lemma card_pow_strictMono (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) : diff --git a/LeanCamCombi/GrowthInGroups/CardQuotient.lean b/LeanCamCombi/GrowthInGroups/CardQuotient.lean index a8034eb776..44ea2c3d5c 100644 --- a/LeanCamCombi/GrowthInGroups/CardQuotient.lean +++ b/LeanCamCombi/GrowthInGroups/CardQuotient.lean @@ -57,7 +57,7 @@ lemma le_card_quotient_mul_sq_inter_subgroup (hAsymm : A⁻¹ = A) : calc #(bipartiteBelow (π · = ·) A (π a)) _ ≤ #((bipartiteBelow (π · = ·) A (π a))⁻¹ * (bipartiteBelow (π · = ·) A (π a))) := - card_le_card_mul_left _ ⟨a⁻¹, by simpa⟩ + card_le_card_mul_left ⟨a⁻¹, by simpa⟩ _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by gcongr simp only [mul_subset_iff, mem_inv', mem_bipartiteBelow, map_inv, Finset.mem_filter, and_imp] diff --git a/LeanCamCombi/GrowthInGroups/Lecture2.lean b/LeanCamCombi/GrowthInGroups/Lecture2.lean index 7c0ab61b8e..a7fec82c2a 100644 --- a/LeanCamCombi/GrowthInGroups/Lecture2.lean +++ b/LeanCamCombi/GrowthInGroups/Lecture2.lean @@ -7,8 +7,8 @@ open scoped Pointwise namespace GrowthInGroups.Lecture2 variable {G : Type*} [DecidableEq G] [Group G] {A : Finset G} {k K : ℝ} {m : ℕ} -lemma lemma_4_2 (U V W : Finset G) : #U * #(V⁻¹ * W) ≤ #(U * V) * #(U * W) := by - exact ruzsa_triangle_inequality_invMul_mul_mul .. +lemma lemma_4_2 (U V W : Finset G) : #U * #(V⁻¹ * W) ≤ #(U * V) * #(U * W) := + ruzsa_triangle_inequality_invMul_mul_mul .. lemma lemma_4_3_2 (hA : #(A ^ 2) ≤ K * #A) : #(A⁻¹ * A) ≤ K ^ 2 * #A := by obtain rfl | hA₀ := A.eq_empty_or_nonempty @@ -61,6 +61,6 @@ lemma lemma_4_7 {A : Finset G} (hA₁ : 1 ∈ A) (hsymm : A⁻¹ = A) (hA : #(A IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) := .of_small_tripling hA₁ hsymm hA lemma lemma_4_8 {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) : - ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := ruzsa_covering_mul hB hK + ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := ruzsa_covering_mul hB hK end GrowthInGroups.Lecture2 diff --git a/LeanCamCombi/GrowthInGroups/Lecture3.lean b/LeanCamCombi/GrowthInGroups/Lecture3.lean index 8294ac2025..e7b91c2c97 100644 --- a/LeanCamCombi/GrowthInGroups/Lecture3.lean +++ b/LeanCamCombi/GrowthInGroups/Lecture3.lean @@ -12,7 +12,7 @@ lemma lemma_5_1 [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻ .of_small_tripling hA₁ hAsymm hA lemma lemma_5_2 [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) : - ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := ruzsa_covering_mul hB hK + ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := ruzsa_covering_mul hB hK open scoped RightActions lemma proposition_5_3 [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) : @@ -34,8 +34,8 @@ lemma proposition_5_6_2 (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubg hA.pow_inter_pow hB hm hn lemma lemma_5_7 (hA : A⁻¹ = A) (hB : B⁻¹ = B) (x y : G) : - ∃ z : G, x • A ∩ y • B ⊆ z • (A ^ 2 ∩ B ^ 2) := - Set.exists_smul_inter_smul_subset_smul_sq_inter_sq hA hB x y + ∃ z : G, x • A ∩ y • B ⊆ z • (A ^ 2 ∩ B ^ 2) := by + simpa [hA, hB, sq] using Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B x y open scoped Classical in lemma lemma_5_8_1 {H : Subgroup G} [H.Normal] {A : Finset G} : diff --git a/LeanCamCombi/Kneser/Kneser.lean b/LeanCamCombi/Kneser/Kneser.lean index 08b27aea61..1e11213ff0 100644 --- a/LeanCamCombi/Kneser/Kneser.lean +++ b/LeanCamCombi/Kneser/Kneser.lean @@ -469,8 +469,7 @@ theorem mul_kneser : (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $ (card_mulStab_dvd_card_mul_mulStab _ _).natCast).trans ?_ rw [sub_sub] - exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right _ hH₁ne) $ - Nat.cast_le.2 $ card_le_card_mul_right _ hH₁ne) _ + gcongr _ - (Nat.cast ?_ + Nat.cast ?_) <;> exact card_le_card_mul_right hH₁ne have aux2₂ : (#s₂ : ℤ) + #t₂ + #H₂ ≤ #H := by rw [← le_sub_iff_add_le'] refine (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_card $ @@ -479,8 +478,8 @@ theorem mul_kneser : (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $ (card_mulStab_dvd_card_mul_mulStab _ _).natCast).trans ?_ rw [sub_sub] - exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) $ - Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) _ + exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right hH₂ne) $ + Nat.cast_le.2 $ card_le_card_mul_right hH₂ne) _ -- Now we deduce inequality (3) using the above lemma in addition to the facts that `s * t` is not -- convergent and then induction hypothesis applied to `sᵢ` and `tᵢ` have aux3₁ : (#S : ℤ) + #T + #s₁ + #t₁ - #H₁ < #H := @@ -488,7 +487,7 @@ theorem mul_kneser : (#S : ℤ) + #T + #s₁ + #t₁ - #H₁ < #S + #T + #(s ∪ t) + #(s ∩ t) - #(s * t) + #(s₁ * t₁) := by have ih₁ := - (add_le_add (card_le_card_mul_right _ hH₁ne) $ card_le_card_mul_right _ hH₁ne).trans + (add_le_add (card_le_card_mul_right hH₁ne) $ card_le_card_mul_right hH₁ne).trans (ih _ _ hst₁) zify at ih₁ linarith [hstconv, ih₁] @@ -505,7 +504,7 @@ theorem mul_kneser : (#S : ℤ) + #T + #s₂ + #t₂ - #H₂ < #S + #T + #(s ∪ t) + #(s ∩ t) - #(s * t) + #(s₂ * t₂) := by have ih₂ := - (add_le_add (card_le_card_mul_right _ hH₂ne) $ card_le_card_mul_right _ hH₂ne).trans + (add_le_add (card_le_card_mul_right hH₂ne) $ card_le_card_mul_right hH₂ne).trans (ih _ _ hst₂) zify at hstconv ih₂ linarith [ih₂] diff --git a/LeanCamCombi/Kneser/KneserRuzsa.lean b/LeanCamCombi/Kneser/KneserRuzsa.lean index 637ab24885..b3681a73ac 100644 --- a/LeanCamCombi/Kneser/KneserRuzsa.lean +++ b/LeanCamCombi/Kneser/KneserRuzsa.lean @@ -220,7 +220,7 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) : rw [this] refine (le_inf' ht _ fun b hb ↦ ?_).trans (le_card_sup_add_card_mulStab_sup _) rw [← hstcard b hb] - refine add_le_add (card_le_card_mul_right _ ⟨_, hbt' _ hb⟩) + refine add_le_add (card_le_card_mul_right ⟨_, hbt' _ hb⟩) ((card_mono $ subset_mulStab_mul_left ⟨_, hbt' _ hb⟩).trans' ?_) rw [← card_smul_finset (b : α)⁻¹ (t' _)] refine card_mono ((mul_subset_left_iff $ hs.mono $ hs' _ hb).1 ?_) diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean index cf336ad889..61fbd4762b 100644 --- a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean +++ b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean @@ -14,37 +14,4 @@ lemma smul_finset_subset_mul : a ∈ s → a • t ⊆ s * t := image_subset_ima attribute [gcongr] div_subset_div_left div_subset_div_right end Mul - -section Monoid -variable [Monoid α] {s t : Finset α} {a : α} {n : ℕ} - -@[to_additive] -lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n := by - simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn - -end Monoid - -section CancelMonoid -variable [CancelMonoid α] {s t : Finset α} {a : α} {n : ℕ} - -@[to_additive] -lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial := by - rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩ - exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩ - -@[to_additive] -lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial := by - rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩ - exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩ - -@[to_additive] -lemma Nontrivial.mul (hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial := - hs.mul_right ht.nonempty - -@[to_additive] -lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial - | 1, _ => by simpa - | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs - -end CancelMonoid end Finset diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean deleted file mode 100644 index 9dd1d04794..0000000000 --- a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean +++ /dev/null @@ -1,40 +0,0 @@ -import Mathlib.Algebra.Group.Pointwise.Set.Basic - -open scoped Pointwise - -namespace Set -variable {α : Type*} - -section Monoid -variable [Monoid α] {s t : Set α} {a : α} {n : ℕ} - -@[to_additive] -lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n := by - simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn - -end Monoid - -section CancelMonoid -variable [CancelMonoid α] {s t : Set α} {a : α} {n : ℕ} - -@[to_additive] -lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial := by - rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩ - exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩ - -@[to_additive] -lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial := by - rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩ - exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩ - -@[to_additive] -lemma Nontrivial.mul (hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial := - hs.mul_right ht.nonempty - -@[to_additive] -lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial - | 1, _ => by simpa - | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs - -end CancelMonoid -end Set diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean b/LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean index 9d75345c82..e311869818 100644 --- a/LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean +++ b/LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean @@ -1,5 +1,4 @@ import Mathlib.Algebra.Group.Subgroup.Pointwise -import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Lattice open Set Subgroup @@ -24,29 +23,3 @@ lemma closure_pow (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s := (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn end Subgroup - - -namespace Set -variable {G : Type*} [Group G] {s : Set G} - -@[to_additive (attr := simp)] -lemma mul_subgroupClosure (hs : s.Nonempty) : s * closure s = closure s := by - rw [← smul_eq_mul, ← Set.iUnion_smul_set] - have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s := - smul_coe_set <| subset_closure ha - simp (config := {contextual := true}) [h, hs] - -@[to_additive (attr := simp)] -lemma mul_subgroupClosure_pow (hs : s.Nonempty) : ∀ n, s ^ n * closure s = closure s - | 0 => by simp - | n + 1 => by rw [pow_add, pow_one, mul_assoc, mul_subgroupClosure hs, mul_subgroupClosure_pow hs] - -end Set - -variable {G S : Type*} [Group G] [SetLike S G] [SubgroupClass S G] {s : Set G} {n : ℕ} - -set_option linter.unusedVariables false in -@[to_additive (attr := simp)] -lemma coe_set_pow : ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set G) = H - | 1, _, H => by simp - | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe] diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/LeanCamCombi/Mathlib/Algebra/Group/Submonoid/Pointwise.lean index cac774d661..2642f7faa8 100644 --- a/LeanCamCombi/Mathlib/Algebra/Group/Submonoid/Pointwise.lean +++ b/LeanCamCombi/Mathlib/Algebra/Group/Submonoid/Pointwise.lean @@ -1,5 +1,4 @@ import Mathlib.Algebra.Group.Submonoid.Pointwise -import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Basic open Set diff --git a/LeanCamCombi/Mathlib/Algebra/Pointwise/Stabilizer.lean b/LeanCamCombi/Mathlib/Algebra/Pointwise/Stabilizer.lean deleted file mode 100644 index c40465caf7..0000000000 --- a/LeanCamCombi/Mathlib/Algebra/Pointwise/Stabilizer.lean +++ /dev/null @@ -1,91 +0,0 @@ -import Mathlib.Algebra.Pointwise.Stabilizer - -open Set -open scoped Pointwise - -namespace MulAction -variable {G H α : Type*} - -section Group -variable [Group G] [Group H] [MulAction G α] {s t : Set α} {a : G} - -attribute [norm_cast] stabilizer_coe_finset - -@[to_additive] -lemma stabilizer_inf_stabilizer_le_stabilizer_union : - stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∪ t) := by - aesop (add simp [SetLike.le_def, smul_set_union]) - -@[to_additive] -lemma stabilizer_inf_stabilizer_le_stabilizer_inter : - stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∩ t) := by - aesop (add simp [SetLike.le_def, smul_set_inter]) - -@[to_additive] -lemma stabilizer_inf_stabilizer_le_stabilizer_sdiff : - stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s \ t) := by - aesop (add simp [SetLike.le_def, smul_set_sdiff]) - -@[to_additive] -lemma stabilizer_union_eq_left (hdisj : Disjoint s t) (hstab : stabilizer G s ≤ stabilizer G t) - (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) : - stabilizer G (s ∪ t) = stabilizer G s := by - refine le_antisymm ?_ ?_ - · calc - stabilizer G (s ∪ t) - ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa - _ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff - _ = stabilizer G s := by rw [union_diff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty] - · calc - stabilizer G s - ≤ stabilizer G s ⊓ stabilizer G t := by simpa - _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union - -@[to_additive] -lemma stabilizer_union_eq_right (hdisj : Disjoint s t) (hstab : stabilizer G t ≤ stabilizer G s) - (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) : - stabilizer G (s ∪ t) = stabilizer G t := by - rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)] - --- TODO: Replace `mem_stabilizer_of_finite_iff_smul_le` -@[to_additive] -lemma mem_stabilizer_iff_subset_smul_set (hs : s.Finite) : a ∈ stabilizer G s ↔ s ⊆ a • s := by - classical - lift s to Finset α using hs - norm_cast - exact mem_stabilizer_finset_iff_subset_smul_finset - -@[to_additive] -lemma mem_stabilizer_iff_smul_set_subset (hs : s.Finite) : a ∈ stabilizer G s ↔ a • s ⊆ s := by - classical - lift s to Finset α using hs - norm_cast - exact mem_stabilizer_finset_iff_smul_finset_subset - -variable {s t : Set G} - -open scoped RightActions in -@[to_additive] -lemma op_smul_set_stabilizer_subset (ha : a ∈ s) : (stabilizer G s : Set G) <• a ⊆ s := - smul_set_subset_iff.2 fun b hb ↦ by rw [← hb]; exact smul_mem_smul_set ha - -@[to_additive] -lemma stabilizer_subset_div_right (ha : a ∈ s) : ↑(stabilizer G s) ⊆ s / {a} := fun b hb ↦ - ⟨_, by rwa [← smul_eq_mul, mem_stabilizer_set.1 hb], _, mem_singleton _, mul_div_cancel_right _ _⟩ - -@[to_additive] -lemma stabilizer_finite (hs₀ : s.Nonempty) (hs : s.Finite) : (stabilizer G s : Set G).Finite := by - obtain ⟨a, ha⟩ := hs₀ - exact (hs.div <| finite_singleton _).subset <| stabilizer_subset_div_right ha - -end Group - -section CommGroup -variable [CommGroup G] {s t : Set G} {a : G} - -@[to_additive] -lemma smul_set_stabilizer_subset (ha : a ∈ s) : a • (stabilizer G s : Set G) ⊆ s := by - simpa using op_smul_set_stabilizer_subset ha - -end CommGroup -end MulAction diff --git a/LeanCamCombi/Mathlib/Combinatorics/Additive/RuzsaCovering.lean b/LeanCamCombi/Mathlib/Combinatorics/Additive/RuzsaCovering.lean deleted file mode 100644 index 9c6f6c1049..0000000000 --- a/LeanCamCombi/Mathlib/Combinatorics/Additive/RuzsaCovering.lean +++ /dev/null @@ -1,69 +0,0 @@ -/- -Copyright (c) 2022 Yaël Dillies. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yaël Dillies --/ -import Mathlib.Algebra.Group.Pointwise.Finset.Basic -import Mathlib.Data.Real.Basic -import Mathlib.SetTheory.Cardinal.Finite -import Mathlib.Tactic.Positivity.Finset - -/-! -# Ruzsa's covering lemma - -This file proves the Ruzsa covering lemma. This says that, for `A`, `B` finsets, we can cover `A` -with at most `#(A + B) / #B` copies of `B - B`. --/ - -open scoped Pointwise - -variable {G : Type*} [Group G] {K : ℝ} - -namespace Finset -variable [DecidableEq G] {A B : Finset G} - -/-- **Ruzsa's covering lemma**. -/ -@[to_additive "**Ruzsa's covering lemma**"] -theorem ruzsa_covering_mul (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) : - ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := by - haveI : ∀ F, Decidable ((F : Set G).PairwiseDisjoint (· • B)) := fun F ↦ Classical.dec _ - set C := {F ∈ A.powerset | F.toSet.PairwiseDisjoint (· • B)} - obtain ⟨F, hF, hFmax⟩ := C.exists_maximal <| filter_nonempty_iff.2 - ⟨∅, empty_mem_powerset _, by rw [coe_empty]; exact Set.pairwiseDisjoint_empty⟩ - rw [mem_filter, mem_powerset] at hF - obtain ⟨hFA, hF⟩ := hF - refine ⟨F, hFA, le_of_mul_le_mul_right ?_ (by positivity : (0 : ℝ) < #B), fun a ha ↦ ?_⟩ - · calc - (#F * #B : ℝ) = #(F * B) := by - rw [card_mul_iff.2 <| pairwiseDisjoint_smul_iff.1 hF, Nat.cast_mul] - _ ≤ #(A * B) := by gcongr - _ ≤ K * #B := hK - rw [mul_div_assoc] - by_cases hau : a ∈ F - · exact subset_mul_left _ hB.one_mem_div hau - by_cases H : ∀ b ∈ F, Disjoint (a • B) (b • B) - · refine (hFmax _ ?_ <| ssubset_insert hau).elim - rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert] - exact ⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩ - push_neg at H - simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H - obtain ⟨b, hb, c, hc₁, hc₂⟩ := H - exact mem_mul.2 ⟨b, hb, b⁻¹ * a, mem_div.2 ⟨_, hc₂, _, hc₁, by simp⟩, by simp⟩ - -end Finset - -namespace Set -variable {A B : Set G} - -/-- **Ruzsa's covering lemma** for sets. See also `Finset.exists_subset_mul_div`. -/ -@[to_additive "**Ruzsa's covering lemma** for sets. See also `Finset.exists_subset_add_sub`"] -lemma ruzsa_covering_mul (hA : A.Finite) (hB : B.Finite) (hB₀ : B.Nonempty) - (hK : Nat.card (A * B) ≤ K * Nat.card B) : - ∃ F ⊆ A, Nat.card F ≤ K ∧ A ⊆ F * B / B ∧ F.Finite := by - lift A to Finset G using hA - lift B to Finset G using hB - classical - obtain ⟨F, hFA, hF, hAF⟩ := Finset.ruzsa_covering_mul hB₀ (by simpa [← Finset.coe_mul] using hK) - exact ⟨F, by norm_cast; simp [*]⟩ - -end Set diff --git a/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean b/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean index 83e72edc96..3a623a40a2 100644 --- a/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean +++ b/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean @@ -1,6 +1,3 @@ -import Mathlib.Algebra.Group.Action.Basic -import Mathlib.Algebra.Group.Action.Opposite -import Mathlib.Algebra.Group.Pointwise.Set.Basic import Mathlib.Data.Set.Pointwise.SMul open MulOpposite @@ -18,55 +15,18 @@ lemma singleton_mul' (a : α) (s : Set α) : {a} * s = a • s := singleton_mul @[to_additive (attr := simp)] lemma mul_singleton' (s : Set α) (a : α) : s * {a} = op a • s := mul_singleton -@[to_additive] -lemma smul_set_subset_mul : a ∈ s → a • t ⊆ s * t := image_subset_image2_right - -@[to_additive] lemma pair_mul (a b : α) (s : Set α) : {a, b} * s = a • s ∪ b • s := by - rw [insert_eq, union_mul, singleton_mul', singleton_mul'] - -open scoped RightActions -@[to_additive] lemma mul_pair (s : Set α) (a b : α) : s * {a, b} = s <• a ∪ s <• b := by - rw [insert_eq, mul_union, mul_singleton', mul_singleton'] - end Mul - -section Group -variable [Group α] {s t : Set α} {a b : α} - -@[to_additive (attr := simp)] -lemma mem_smul_set_inv : a ∈ b • s⁻¹ ↔ b ∈ a • s := by simp [mem_smul_set_iff_inv_smul_mem] - -@[to_additive exists_inter_subset_two_nsmul_inter_two_nsmul] -lemma exists_smul_inter_smul_subset_smul_sq_inter_sq (hs : s⁻¹ = s) (ht : t⁻¹ = t) (a b : α) : - ∃ z : α, a • s ∩ b • t ⊆ z • (s ^ 2 ∩ t ^ 2) := by - obtain hAB | ⟨z, hzA, hzB⟩ := (a • s ∩ b • t).eq_empty_or_nonempty - · exact ⟨1, by simp [hAB]⟩ - refine ⟨z, ?_⟩ - calc - a • s ∩ b • t ⊆ (z • s⁻¹) * s ∩ ((z • t⁻¹) * t) := by - gcongr <;> apply smul_set_subset_mul <;> simpa - _ = z • (s ^ 2 ∩ t ^ 2) := by simp_rw [Set.smul_set_inter, sq, smul_mul_assoc, hs, ht] - -end Group end Set namespace Set variable {α β : Type*} -section Monoid -variable [Monoid α] [MulAction α β] {s : Set β} {a : α} {b : β} - -@[simp] lemma mem_invOf_smul_set [Invertible a] : b ∈ ⅟a • s ↔ a • b ∈ s := - mem_inv_smul_set_iff (a := unitOfInvertible a) - -end Monoid - section Group variable [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} +-- TODO: Replace @[to_additive (attr := simp)] -lemma smul_set_subset_smul_set_iff : a • s ⊆ a • t ↔ s ⊆ t := - image_subset_image_iff <| MulAction.injective _ +lemma smul_set_subset_smul_set_iff : a • s ⊆ a • t ↔ s ⊆ t := set_smul_subset_set_smul_iff end Group end Set diff --git a/LeanCamCombi/Mathlib/NumberTheory/Fermat.lean b/LeanCamCombi/Mathlib/NumberTheory/Fermat.lean deleted file mode 100644 index 5809a10f97..0000000000 --- a/LeanCamCombi/Mathlib/NumberTheory/Fermat.lean +++ /dev/null @@ -1,47 +0,0 @@ -import Mathlib.NumberTheory.Fermat - -open Finset Function -open scoped BigOperators - -namespace Nat -variable {m n : ℕ} - --- TODO: Replace -alias fermatNumber_strictMono := strictMono_fermatNumber - -lemma fermatNumber_mono : Monotone fermatNumber := fermatNumber_strictMono.monotone -lemma fermatNumber_injective : Injective fermatNumber := fermatNumber_strictMono.injective - -@[simp] -lemma fermatNumber_inj : fermatNumber m = fermatNumber n ↔ m = n := fermatNumber_injective.eq_iff - -lemma three_le_fermatNumber (n : ℕ) : 3 ≤ fermatNumber n := fermatNumber_mono n.zero_le - -lemma fermatNumber_ne_one (n : ℕ) : fermatNumber n ≠ 1 := - (n.three_le_fermatNumber.trans_lt' $ by norm_num).ne' - -/-- The recurence relation satisfied by Fermat numbers. -/ -lemma prod_fermatNumber_add_two (n : ℕ) : ∏ k in range n, fermatNumber k + 2 = fermatNumber n := by - zify - induction' n with n ih - · trivial - rw [prod_range_succ, eq_sub_iff_add_eq.2 ih] - -- We prove a form without subtraction of naturals - have h : fermatNumber n * fermatNumber n + 2 = fermatNumber n.succ + 2 * fermatNumber n := by - unfold fermatNumber; simp only [_root_.pow_succ, two_mul]; ring - -- Then we let linarith finish - linarith - --- TODO: Replace -alias prod_fermatNumber := fermatNumber_product - --- TODO: Replace `coprime_fermatNumber_fermatNumber`! -/-- Fermat numbers are coprime. - -This follows from the recurrence relations and divisibility, -as well as the parity of Fermat numbers. --/ -lemma pairwise_coprime_fermatNumber : - Pairwise fun m n ↦ Coprime (fermatNumber m) (fermatNumber n) := by - rintro m n hmn - exact coprime_fermatNumber_fermatNumber hmn.symm diff --git a/LeanCamCombi/Mathlib/Order/Chain.lean b/LeanCamCombi/Mathlib/Order/Chain.lean deleted file mode 100644 index b4aae246ef..0000000000 --- a/LeanCamCombi/Mathlib/Order/Chain.lean +++ /dev/null @@ -1,66 +0,0 @@ -import Mathlib.Order.Chain - -open Set - -variable {α β : Type*} - -theorem isChain_singleton (r : α → α → Prop) (a : α) : IsChain r {a} := - pairwise_singleton _ _ - -theorem isChain_pair (r : α → α → Prop) {a b : α} (h : r a b) : IsChain r {a, b} := - (isChain_singleton _ _).insert fun _ hb _ => Or.inl <| (eq_of_mem_singleton hb).symm.recOn ‹_› - -theorem IsMaxChain.image {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {c : Set α} - (hc : IsMaxChain r c) : IsMaxChain s (f '' c) where - left := hc.isChain.image _ _ _ fun _ _ => by exact f.map_rel_iff.2 - right t ht hf := - (f.toEquiv.eq_preimage_iff_image_eq _ _).1 - (by - rw [preimage_equiv_eq_image_symm] - exact - hc.2 (ht.image _ _ _ fun _ _ => by exact f.symm.map_rel_iff.2) - ((f.toEquiv.subset_symm_image _ _).2 hf)) - -namespace Flag - -section LE - -variable [LE α] {s t : Flag α} {a : α} - -/-- Reinterpret a maximal chain as a flag. -/ -def ofIsMaxChain (c : Set α) (hc : IsMaxChain (· ≤ ·) c) : Flag α := ⟨c, hc.isChain, hc.2⟩ - -@[simp, norm_cast] -theorem coe_ofIsMaxChain (c : Set α) (hc) : ofIsMaxChain c hc = c := rfl - -end LE - -section Preorder - -variable [Preorder α] [Preorder β] {s : Flag α} {a b : α} - -theorem mem_iff_forall_le_or_ge : a ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a := - ⟨fun ha b => s.le_or_le ha, fun hb => - of_not_not fun ha => - Set.ne_insert_of_not_mem _ ‹_› <| - s.maxChain.2 (s.chain_le.insert fun c hc _ => hb hc) <| Set.subset_insert _ _⟩ - -/-- Flags are preserved under order isomorphisms. -/ -def map (e : α ≃o β) : Flag α ≃ Flag β - where - toFun s := ofIsMaxChain _ (s.maxChain.image e) - invFun s := ofIsMaxChain _ (s.maxChain.image e.symm) - left_inv s := ext <| e.symm_image_image s - right_inv s := ext <| e.image_symm_image s - -@[simp, norm_cast] -theorem coe_map (e : α ≃o β) (s : Flag α) : ↑(map e s) = e '' s := - rfl - -@[simp] -theorem symm_map (e : α ≃o β) : (map e).symm = map e.symm := - rfl - -end Preorder - -end Flag diff --git a/LeanCamCombi/Mathlib/Order/Flag.lean b/LeanCamCombi/Mathlib/Order/Flag.lean index fd5196e720..963a744650 100644 --- a/LeanCamCombi/Mathlib/Order/Flag.lean +++ b/LeanCamCombi/Mathlib/Order/Flag.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ import Mathlib.Data.Set.Pointwise.SMul +import Mathlib.Order.Chain import Mathlib.Order.Grade -import LeanCamCombi.Mathlib.Order.Chain import LeanCamCombi.Mathlib.Order.RelIso.Group /-! diff --git a/LeanCamCombi/Mathlib/Order/Monotone/Monovary.lean b/LeanCamCombi/Mathlib/Order/Monotone/Monovary.lean deleted file mode 100644 index 18ddbec30f..0000000000 --- a/LeanCamCombi/Mathlib/Order/Monotone/Monovary.lean +++ /dev/null @@ -1,53 +0,0 @@ -import Mathlib.Order.Monotone.Monovary -import Mathlib.SetTheory.Cardinal.Basic - -open Function Set - -variable {ι ι' α β γ : Type*} - -section Preorder - -variable [Preorder α] [Preorder β] [Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} {g' : β → γ} - {s t : Set ι} - -theorem monovaryOn_iff_monovary : MonovaryOn f g s ↔ Monovary (fun i : s => f i) fun i => g i := by - simp [Monovary, MonovaryOn] - -theorem antivaryOn_iff_antivary : AntivaryOn f g s ↔ Antivary (fun i : s => f i) fun i => g i := by - simp [Antivary, AntivaryOn] - -section PartialOrder - -variable [PartialOrder ι] - -theorem StrictMono.trans_monovary (hf : StrictMono f) (h : Monovary g f) : Monotone g := - monotone_iff_forall_lt.2 fun _a _b hab => h <| hf hab - -theorem StrictMono.trans_antivary (hf : StrictMono f) (h : Antivary g f) : Antitone g := - antitone_iff_forall_lt.2 fun _a _b hab => h <| hf hab - -theorem StrictAnti.trans_monovary (hf : StrictAnti f) (h : Monovary g f) : Antitone g := - antitone_iff_forall_lt.2 fun _a _b hab => h <| hf hab - -theorem StrictAnti.trans_antivary (hf : StrictAnti f) (h : Antivary g f) : Monotone g := - monotone_iff_forall_lt.2 fun _a _b hab => h <| hf hab - -theorem StrictMonoOn.trans_monovaryOn (hf : StrictMonoOn f s) (h : MonovaryOn g f s) : - MonotoneOn g s := - monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab => h ha hb <| hf ha hb hab - -theorem StrictMonoOn.trans_antivaryOn (hf : StrictMonoOn f s) (h : AntivaryOn g f s) : - AntitoneOn g s := - antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab => h ha hb <| hf ha hb hab - -theorem StrictAntiOn.trans_monovaryOn (hf : StrictAntiOn f s) (h : MonovaryOn g f s) : - AntitoneOn g s := - antitoneOn_iff_forall_lt.2 fun _a ha _b hb hab => h hb ha <| hf ha hb hab - -theorem StrictAntiOn.trans_antivaryOn (hf : StrictAntiOn f s) (h : AntivaryOn g f s) : - MonotoneOn g s := - monotoneOn_iff_forall_lt.2 fun _a ha _b hb hab => h hb ha <| hf ha hb hab - -end PartialOrder - -end Preorder diff --git a/LeanCamCombi/Mathlib/Order/Zorn.lean b/LeanCamCombi/Mathlib/Order/Zorn.lean index acd3c40c35..97458daee6 100644 --- a/LeanCamCombi/Mathlib/Order/Zorn.lean +++ b/LeanCamCombi/Mathlib/Order/Zorn.lean @@ -1,5 +1,4 @@ import Mathlib.Order.Zorn -import LeanCamCombi.Mathlib.Order.Chain variable {α : Type} @@ -17,7 +16,7 @@ theorem exists_mem (a : α) : ∃ s : Flag α, a ∈ s := ⟨s, hs rfl⟩ theorem exists_mem_mem (hab : a ≤ b) : ∃ s : Flag α, a ∈ s ∧ b ∈ s := by - simpa [Set.insert_subset_iff] using (isChain_pair _ hab).exists_subset_flag + simpa [Set.insert_subset_iff] using (IsChain.pair hab).exists_subset_flag instance : Nonempty (Flag α) := ⟨.ofIsMaxChain _ maxChain_spec⟩ diff --git a/LeanCamCombi/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean b/LeanCamCombi/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean deleted file mode 100644 index 23533f00ad..0000000000 --- a/LeanCamCombi/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean +++ /dev/null @@ -1,5 +0,0 @@ -/-! -# TODO - -Use semi-implicits in `Metric.continuousAt_iff` --/ diff --git a/LeanCamCombi/MonovaryOrder.lean b/LeanCamCombi/MonovaryOrder.lean index bef0658448..b75db958c1 100644 --- a/LeanCamCombi/MonovaryOrder.lean +++ b/LeanCamCombi/MonovaryOrder.lean @@ -1,5 +1,5 @@ +import Mathlib.Order.Monotone.Monovary import Mathlib.SetTheory.Cardinal.Basic -import LeanCamCombi.Mathlib.Order.Monotone.Monovary open Function Set diff --git a/lake-manifest.json b/lake-manifest.json index a1a66d3e6b..ea9cbcac13 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,62 +1,72 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "7488499a8aad6ffada87ab6db73673d88dc04c97", - "name": "batteries", + "scope": "", + "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c", + "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", - "name": "Qq", + "scope": "", + "rev": "90f062feea36adad53b81925aa9dc3e09c268262", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, + "inputRev": null, + "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/aesop", + {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "de91b59101763419997026c35a41432ac8691f15", - "name": "aesop", + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "1383e72b40dd62a566896a6e348ffe868801b172", - "name": "proofwidgets", + "scope": "", + "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", + "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.46", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", + {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, - "scope": "leanprover", - "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d", - "name": "Cli", + "scope": "", + "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", + "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "119b022b3ea88ec810a677888528e50f8144a26e", - "name": "importGraph", + "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", + "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -71,65 +81,55 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/plausible", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa", - "name": "plausible", + "rev": "119b022b3ea88ec810a677888528e50f8144a26e", + "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "13fc0e8a77fcb3fc528f47e1e5a1b09df301bb0c", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", + {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", - "name": "MD4Lean", + "scope": "leanprover-community", + "rev": "1383e72b40dd62a566896a6e348ffe868801b172", + "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v0.0.46", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", + {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "scope": "", - "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014", - "name": "UnicodeBasic", + "scope": "leanprover-community", + "rev": "de91b59101763419997026c35a41432ac8691f15", + "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", + "scope": "leanprover-community", + "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41", + "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "scope": "", - "rev": "059eb7e86f1f5c16780657d14de1a560a9d6784c", - "name": "«doc-gen4»", + "scope": "leanprover-community", + "rev": "dfbe9387054e2972449de7bf346059d3609529fa", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}], + "inherited": true, + "configFile": "lakefile.toml"}], "name": "LeanCamCombi", "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 57a4710c03..6d9e70f733 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0-rc2 +leanprover/lean4:v4.14.0-rc3