GrowthInGroups: replace `comap_C_eq_comap_localization_union_comap_qu…

…otient` by two lower level lemmas

LeanCamCombi.lean

@@ -54,6 +54,7 @@ import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
+import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean

@@ -10,6 +10,7 @@ import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
+import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.GrowthInGroups.ConstructibleSetData
 
 variable {R S M A : Type*} [CommRing R] [CommRing S] [AddCommGroup M] [Module R M] [CommRing A]
@@ -255,7 +256,9 @@ lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n)
             (comap (mapRingHom q₁.toRingHom) ⁻¹' (zeroLocus (.range e.val) \ zeroLocus {f}))) ∪
           comap q₂ '' (comap C ''
             (comap (mapRingHom q₂) ⁻¹' (zeroLocus (.range e.val) \ zeroLocus {f}))) :=
-        comap_C_eq_comap_localization_union_comap_quotient _ c
+        Set.image_of_range_union_range_eq_univ (by ext; simp) (by ext; simp)
+          (by rw [← range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk,
+            RingHom.algebraMap_toAlgebra]; exact Set.union_compl_self _) _
       _ = (⋃ C ∈ S₁, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1}) ∪
           ⋃ C ∈ S₂, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1} := ?_
       _ = ⋃ C ∈ S₁ ∪ S₂, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1} := by

LeanCamCombi/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -9,24 +9,15 @@ lemma coe_comap (f : R →+* S) : comap f = f.specComap := rfl
 
 lemma comap_apply (f : R →+* S) (x) : comap f x = f.specComap x := rfl
 
-open Polynomial
-
-open Localization in
-lemma comap_C_eq_comap_localization_union_comap_quotient
-    {R : Type*} [CommRing R] (s : Set (PrimeSpectrum R[X])) (c : R) :
-    comap C '' s =
-      comap (algebraMap R (Away c)) '' (comap C ''
-        (comap (mapRingHom (algebraMap R (Away c))) ⁻¹' s)) ∪
-      comap (Ideal.Quotient.mk (.span {c})) '' (comap C ''
-        (comap (mapRingHom (Ideal.Quotient.mk _)) ⁻¹' s)) := by
-  rw [Set.union_comm]
-  simp_rw [← Set.image_comp, ← ContinuousMap.coe_comp, ← comap_comp, ← mapRingHom_comp_C,
-    comap_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range,
-    ← Set.image_union, ← Set.inter_union_distrib_left]
+open Localization Polynomial Set
+
+variable {R : Type*} [CommRing R] (c : R)
+
+lemma range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk (c : R) :
+    letI := (mapRingHom (algebraMap R (Away c))).toAlgebra
+    (range (comap (algebraMap R[X] (Away c)[X])))ᶜ
+      = range (comap (mapRingHom (Ideal.Quotient.mk (.span {c})))) := by
   letI := (mapRingHom (algebraMap R (Away c))).toAlgebra
-  suffices Set.range (comap (mapRingHom (Ideal.Quotient.mk (.span {c})))) =
-      (Set.range (comap (algebraMap R[X] (Away c)[X])))ᶜ by
-    rw [this, RingHom.algebraMap_toAlgebra, Set.compl_union_self, Set.inter_univ]
   have := Polynomial.isLocalization (.powers c) (Away c)
   rw [Submonoid.map_powers] at this
   have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) :=

LeanCamCombi/Mathlib/Data/Set/Image.lean

@@ -0,0 +1,13 @@
+import Mathlib.Data.Set.Image
+
+namespace Set
+variable {α β γ γ₁ γ₂ δ δ₁ δ₂ : Type*} {h : β → α} {f : γ → β} {f₁ : γ₁ → α} {f₂ : γ → γ₁}
+  {g : δ → β} {g₁ : δ₁ → α} {g₂ : δ → δ₁}
+
+lemma image_of_range_union_range_eq_univ (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂)
+    (hfg : range f ∪ range g = univ) (s : Set β) :
+    h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s)) := by
+  rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
+    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
+
+end Set