awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
H : IsConstructible s
isCompact_basis : ∀ (i : R), IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))
sdiff :
  ∀ (i : R) (s : Set R) (hs : s.Finite),
    ∃ (S : ConstructibleSetData R),
      S.toSet = (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
⊢ ∃ (S : ConstructibleSetData R), S.toSet = s
have union : ∀ (s : Set (PrimeSpectrum R)) (hs : IsConstructible s) (t : Set (PrimeSpectrum R)) (ht : IsConstructible t)
  (Hs : ∃ (S : ConstructibleSetData R), S.toSet = s) (Ht : ∃ (S : ConstructibleSetData R), S.toSet = t),
  ∃ (S : ConstructibleSetData R), S.toSet = s ∪ t
Tactic: induction s, H using IsConstructible.induction_of_isTopologicalBasis
      _ (isTopologicalBasis_basic_opens (R := R)) with
  | isCompact_basis i => exact isCompact_basicOpen _
  | sdiff i s hs =>
    have : Finite s := hs
    refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
    simp only [ConstructibleSetData.toSet, Finset.mem_singleton, BasicConstructibleSetData.toSet,
      Set.iUnion_iUnion_eq_left, basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂,
        compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
    congr! 2
    ext
    simp [← (Finite.equivFin s).exists_congr_right, -Nat.card_coe_set_eq]
  | union s hs t ht Hs Ht =>
    obtain ⟨S, rfl⟩ := Hs
    obtain ⟨T, rfl⟩ := Ht
    refine ⟨S ∪ T, ?_⟩
    simp only [ConstructibleSetData.toSet, Set.biUnion_union, ← Finset.mem_coe, Finset.coe_union]
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : IsConstructible s
⊢ ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s
have obtain : ∀ (s : ConstructibleSetData R) (hs : IsConstructible (X := PrimeSpectrum R) s.toSet),
  ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s.toSet
Tactic: obtain ⟨s, rfl⟩ := exists_constructibleSetData_iff.mpr hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
⊢ ∃ (S : Type u) (x : CommRing S) (f : R →+* S), Set.range (comap f) = s.toSet
have refine : Eq (α := Set (PrimeSpectrum R))
  (Set.range (ι :=
    PrimeSpectrum
      ((i : ↥s) →
        Localization.Away (M :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
          ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
              (↑i : BasicConstructibleSetData R).f :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))
    (comap
      (algebraMap R
        ((i : ↥s) →
          Localization.Away (M :=
            HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))
            ((Ideal.Quotient.mk (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)) :
                  (a : R) → R ⧸ Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g))
                (↑i : BasicConstructibleSetData R).f :
              HasQuotient.Quotient R (B := Ideal R) (Ideal.span (Set.range (↑i : BasicConstructibleSetData R).g)))))))
  s.toSet
Tactic: refine ⟨Π i : s, Localization.Away (Ideal.Quotient.mk (Ideal.span (Set.range i.1.g)) i.1.f),
    inferInstance, algebraMap _ _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw : Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₁ : Eq (α := Set (PrimeSpectrum R))
  (comap (Ideal.Quotient.mk I) ''
    (↑((TopologicalSpace.Opens.comap
                { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := sorry :
                  C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
              (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
            (basicOpen (↑C : BasicConstructibleSetData R).f) :
          TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
      Set (PrimeSpectrum (R ⧸ I))))
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₂ : Eq (α := Set (PrimeSpectrum R))
  (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
    ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := sorry } :
        (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
      (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₂ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } :
          (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
        (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₃ : Eq (α := Set (PrimeSpectrum R))
  (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
    (comap (Ideal.Quotient.mk I) ⁻¹' (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₂ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } :
          (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
        (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₃ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (comap (Ideal.Quotient.mk I) ⁻¹' (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₄ : (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
    Set.range (ι := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I)) =
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₂ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } :
          (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
        (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₃ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (comap (Ideal.Quotient.mk I) ⁻¹' (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₄ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      Set.range (ι := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I)) =
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₅ : (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
    zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
  (↑C : BasicConstructibleSetData R).toSet
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u
inst : CommRing R
s : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) s.toSet
e_2 : ↥s = (↑(↑s : Set (BasicConstructibleSetData R)) : Type u)
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C : BasicConstructibleSetData R).g)
f : R ⧸ I := (Ideal.Quotient.mk I : (a : R) → R ⧸ I) (↑C : BasicConstructibleSetData R).f
rw :
  Eq (α := Set (PrimeSpectrum R)) (comap (Ideal.Quotient.mk I) '' (↑(basicOpen f) : Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₁ :
  Eq (α := Set (PrimeSpectrum R))
    (comap (Ideal.Quotient.mk I) ''
      (↑((TopologicalSpace.Opens.comap
                  { toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ :
                    C(PrimeSpectrum (R ⧸ I), PrimeSpectrum R) } :
                (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I)))
              (basicOpen (↑C : BasicConstructibleSetData R).f) :
            TopologicalSpace.Opens (PrimeSpectrum (R ⧸ I))) :
        Set (PrimeSpectrum (R ⧸ I))))
    (↑C : BasicConstructibleSetData R).toSet
rw₂ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      ((⇑{ toFun := comap (Ideal.Quotient.mk I), continuous_toFun := ⋯ } :
          (a : PrimeSpectrum (R ⧸ I)) → PrimeSpectrum R) ⁻¹'
        (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₃ :
  Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (comap (Ideal.Quotient.mk I) ⁻¹' (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R))))
    (↑C : BasicConstructibleSetData R).toSet
rw₄ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      Set.range (ι := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I)) =
    (↑C : BasicConstructibleSetData R).toSet
rw₅ :
  (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
      zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
    (↑C : BasicConstructibleSetData R).toSet
⊢ Eq (α := Set (PrimeSpectrum R))
    (Set.image (α := PrimeSpectrum (R ⧸ I)) (comap (Ideal.Quotient.mk I))
      (Set.range (ι := PrimeSpectrum (Localization.Away f)) (comap (algebraMap (R ⧸ I) (Localization.Away f)))))
    (↑C : BasicConstructibleSetData R).toSet
have rw₆ : (↑(basicOpen (↑C : BasicConstructibleSetData R).f) : Set (PrimeSpectrum R)) ∩
    zeroLocus (↑(RingHom.ker (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)) : Set R) =
  zeroLocus (Set.range (↑C : BasicConstructibleSetData R).g) \ zeroLocus {(↑C : BasicConstructibleSetData R).f}
Tactic: rw [localization_away_comap_range _ f, ← comap_basicOpen, TopologicalSpace.Opens.coe_comap,
      ContinuousMap.coe_mk, Set.image_preimage_eq_inter_range,
      range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective, BasicConstructibleSetData.toSet,
      Set.diff_eq_compl_inter, basicOpen_eq_zeroLocus_compl, Ideal.mk_ker, zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderSpecialization s
hs' : IsConstructible s
⊢ IsClosed s
have obtain : ∀ (S : Type u_4) (w : CommRing S) (f : R →+* S) (hs : StableUnderSpecialization (Set.range (comap f)))
  (hs' : IsConstructible (Set.range (comap f))), IsClosed (Set.range (comap f))
Tactic: obtain ⟨S, _, f, rfl⟩ := exists_range_eq_of_isConstructible hs'
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_4
inst : CommRing R
s : Set (PrimeSpectrum R)
hs : StableUnderGeneralization s
hs' : IsConstructible s
⊢ IsOpen s
have rw : IsClosed sᶜ
Tactic: rw [← isClosed_compl_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p ↔ Free Rₚ Mₚ
have apply : LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[(↑e : Localization.AtPrime p.asIdeal →+* Rₚ)] Mₚ
Tactic: apply Module.Free.iff_of_equiv (σ := e)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst_3 : CommRing Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization.AtPrime Rₚ p.asIdeal
inst_6 : AddCommGroup Mₚ
inst_7 : Module R Mₚ
f : M →ₗ[R] Mₚ
inst_8 : IsLocalizedModule p.asIdeal.primeCompl f
inst_9 : Module Rₚ Mₚ
inst_10 : IsScalarTower R Rₚ Mₚ
e : RingEquiv.{uR, u_1} (Localization.AtPrime p.asIdeal) Rₚ :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ)
⊢ LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[(↑e : Localization.AtPrime p.asIdeal →+* Rₚ)] Mₚ
have refine : ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
  (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun (m • x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Rₚ)
      (((↑e : Localization.AtPrime p.asIdeal →+* Rₚ) : (a : Localization.AtPrime p.asIdeal) → Rₚ) m : Rₚ)
      ((↑(IsLocalizedModule.iso p.asIdeal.primeCompl f) : LocalizedModule p.asIdeal.primeCompl M →ₗ[R] Mₚ).toFun x)
Tactic: refine { __ := IsLocalizedModule.iso p.asIdeal.primeCompl f, map_smul' := ?_ }