Delete now-unused code

LeanCamCombi.lean

@@ -17,7 +17,6 @@ import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.Chevalley
 import LeanCamCombi.GrowthInGroups.ChevalleyComplex
 import LeanCamCombi.GrowthInGroups.Constructible
-import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
 import LeanCamCombi.GrowthInGroups.ConstructibleSetData
 import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
@@ -47,24 +46,18 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 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.VerySmallDoubling
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
-import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
-import LeanCamCombi.Mathlib.Data.Finset.Basic
-import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
-import LeanCamCombi.Mathlib.Data.Finset.Powerset
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Defs
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
-import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
@@ -76,16 +69,17 @@ import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 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.RingTheory.PrimeSpectrum
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
+import LeanCamCombi.Multipartite
 import LeanCamCombi.PhD.VCDim.Basic
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter
 import LeanCamCombi.PlainCombi.VanDenBergKesten
+import LeanCamCombi.PosDiffs
 import LeanCamCombi.SimplicialComplex.Basic
 import LeanCamCombi.SimplicialComplex.Finite
 import LeanCamCombi.SimplicialComplex.Pure

LeanCamCombi/GrowthInGroups/Chevalley.lean

@@ -3,7 +3,6 @@ import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
-import LeanCamCombi.Mathlib.RingTheory.Ideal.Span
 import LeanCamCombi.Mathlib.RingTheory.Localization.Integral
 import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial
 
@@ -51,15 +50,15 @@ lemma foo_induction
   obtain ⟨n, e, rfl⟩ : ∃ (n : ℕ) (e : Fin (n + 1) → R[X]), I = Ideal.span (Set.range e) := by
     obtain ⟨s, rfl⟩ := hI
     exact ⟨s.card, Fin.cons 0 (Subtype.val ∘ s.equivFin.symm),
-      by simp [← Set.union_singleton, Ideal.span_union]⟩
+      by simp [← Set.union_singleton, Ideal.span_union, Set.singleton_zero]⟩
   clear hI
   set v : (Fin (n + 1) → WithBot ℕ) ×ₗ Prop := toLex
     (degree ∘ e, ¬ ∃ i, IsUnit (e i).leadingCoeff ∧ ∀ j, e j ≠ 0 →
       (e i).degree ≤ (e j).degree) with hv
   clear_value v
   induction' v using WellFoundedLT.induction with v H_IH generalizing R
   by_cases he0 : e = 0
-  · rw [he0, Set.range_zero, Ideal.span_singleton_zero]; exact hP₁ R
+  · simpa [he0, Set.range_zero, Set.singleton_zero] using hP₁ R
   cases subsingleton_or_nontrivial R
   · rw [Subsingleton.elim (Ideal.span (Set.range e)) ⊥]; exact hP₁ R
   simp only [funext_iff, Pi.zero_apply, not_forall] at he0

LeanCamCombi/Mathlib/Data/Set/Basic.lean

@@ -6,12 +6,4 @@ variable {α : Type*} {s : Set α} {a : α}
 lemma diff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t := by
   ext; simp [and_right_comm]
 
-lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s := by aesop
-
-lemma insert_erase_invOn :
-    InvOn (insert a) (fun s ↦ s \ {a}) {s : Set α | a ∈ s} {s : Set α | a ∉ s} :=
-  ⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_not_mem⟩
-
-@[gcongr] protected alias ⟨_, GCongr.singleton_subset_singleton⟩ := singleton_subset_singleton
-
 end Set

LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean → LeanCamCombi/PosDiffs.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Combinatorics.SetFamily.Compression.Down
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Combinatorics.SetFamily.Compression.Down
 import Mathlib.Data.Finset.Sups
 import Mathlib.Order.Interval.Set.OrdConnected
 import Mathlib.Order.UpperLower.Basic