awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
n_1 n : ℕ
IH :
  ∀ {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R))
    (hSn : ∀ C ∈ S, C.n ≤ k)
    (hS :
      ∀ C ∈ S,
        ∀ (j : Fin C.n),
          Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
            (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) (C.g j)),
    ∃ (T : ConstructibleSetData R),
      comap MvPolynomial.C '' S.toSet = T.toSet ∧
        ∀ C ∈ T,
          C.n ≤ numBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
            ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin (n + 1)) R))
        (coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)) (C.g j)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k * (1 + Multiset.count 0 d)
B : Multiset (Fin n) :=
  (Finsupp.toMultiset : (a : Fin n →₀ ℕ) → Multiset (Fin n))
    (Finsupp.comapDomain Fin.succ ((Multiset.toFinsupp : (a : Multiset (Fin (n + 1))) → Fin (n + 1) →₀ ℕ) d) ⋯)
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT₁ : comap Polynomial.C '' S'.toSet = T.toSet
hT₂ :
  ∀ C ∈ T,
    C.n ≤ S'.degBound ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
            (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) (S'.degBound ^ S'.degBound)
N : ℕ := (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d))
this :
  ∀ (C : BasicConstructibleSetData (MvPolynomial (Fin n) R)) (hCT : C ∈ T) (a : Fin C.n),
    Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))) (C.g a)
⊢ ∃ (T : ConstructibleSetData R),
    comap MvPolynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ numBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1) ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1)
have h1M : 1 ≤ M
Tactic: have h1M : 1 ≤ M := Submodule.one_le.mpr hM
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
⊢ ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
    Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
        (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
          (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
        T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
have hg : Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
  (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
  (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
Tactic: have hg : g.comp (algebraMap (MvPolynomial (Fin n) R) _) = f := by ext x : 2 <;> simp [g]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
⊢ g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
have hC : ∀ (x : R),
  Eq (α := MvPolynomial (Fin m) R)
    (((g.comp σ).comp MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) x : MvPolynomial (Fin m) R)
    ((RingHom.comp (RingHom.id (MvPolynomial (Fin m) R)) MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) x :
      MvPolynomial (Fin m) R)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial (Fin m) R)
      (((g.comp σ).comp MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) x : MvPolynomial (Fin m) R)
      ((RingHom.comp (RingHom.id (MvPolynomial (Fin m) R)) MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) x :
        MvPolynomial (Fin m) R)
⊢ g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
have hX : ∀ (i : Fin m) (m_1 : Fin m →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff m_1 ((g.comp σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)))
    (MvPolynomial.coeff m_1
      ((RingHom.id (MvPolynomial (Fin m) R) : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) R)
        (MvPolynomial.X i)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
⊢ ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
    Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
        (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
          (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
        T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
have hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
Tactic: have hσ : g.comp σ = .id _ := by ext : 2 <;> simp [g, σ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
⊢ ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
    Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
        (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
          (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
        T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
have hσ' : ∀ (x : MvPolynomial (Fin m) R),
  (g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
      ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) x) =
    x
Tactic: have hσ' (x) : g (σ x) = x := DFunLike.congr_fun hσ x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' :
  ∀ (x : MvPolynomial (Fin m) R),
    (g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
        ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) x) =
      x
⊢ ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
    Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
        (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
          (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
        T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
have hg' : Surjective (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β := MvPolynomial (Fin m) R)
  (⇑g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
Tactic: have hg' : Surjective g := LeftInverse.surjective hσ'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ map (RingHom.id R) = id
have h : ∀ (x : BasicConstructibleSetData R), map (RingHom.id R) x = id x
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
φ : S →+* T
ψ : R →+* S
⊢ map (φ.comp ψ) = map φ ∘ map ψ
have h : ∀ (x : BasicConstructibleSetData R), map (φ.comp ψ) x = (map φ ∘ map ψ) x
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ C ∈ image (BasicConstructibleSetData.map f) s, C.toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet
have rw : ⋃ y ∈ s, (BasicConstructibleSetData.map f y).toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet
Tactic: rw [set_biUnion_finset_image]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
⊢ IsConstructible (X := PrimeSpectrum R) S.toSet
have refine_1 : ∀ x ∈ (↑S : Set (BasicConstructibleSetData R)), IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))
Tactic: refine .biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
refine_1 :
  ∀ x ∈ (↑S : Set (BasicConstructibleSetData R)), IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))
⊢ IsConstructible (X := PrimeSpectrum R) S.toSet
have refine_2 : ∀ x ∈ (↑S : Set (BasicConstructibleSetData R)), IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})
Tactic: refine .biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
x : BasicConstructibleSetData R
h : x ∈ (↑S : Set (BasicConstructibleSetData R))
⊢ IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))
have refine_1 : IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))ᶜ
Tactic: rw [← isConstructible_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
x : BasicConstructibleSetData R
h : x ∈ (↑S : Set (BasicConstructibleSetData R))
⊢ IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})
have refine_2 : IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})ᶜ
Tactic: rw [← isConstructible_compl]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ (S : ConstructibleSetData R), S.toSet = s) ↔ IsConstructible s
have refine : ∀ (H : IsConstructible s), ∃ (S : ConstructibleSetData R), S.toSet = s
Tactic: refine ⟨fun ⟨S, H⟩ ↦ H ▸ S.isConstructible_toSet, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
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))
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Finite s := hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ (S : ConstructibleSetData R),
    S.toSet = (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
have sdiff : ConstructibleSetData.toSet
    {{ f := i, n := Nat.card.{u_1} (↑s : Type u_1),
        g := fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
          (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                i) :
            R) :
        BasicConstructibleSetData R }} =
  (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
Tactic: refine ⟨{⟨i, Nat.card s, fun i ↦ ((Finite.equivFin s).symm i).1⟩}, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ConstructibleSetData.toSet
      {{ f := i, n := Nat.card.{u_1} (↑s : Type u_1),
          g := fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
            (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                  i) :
              R) :
          BasicConstructibleSetData R }} =
    (↑(basicOpen i) : Set (PrimeSpectrum R)) \ ⋃ j ∈ s, (↑(basicOpen j) : Set (PrimeSpectrum R))
have sdiff : Eq (α := Set (PrimeSpectrum R))
  (zeroLocus
      (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
        (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
          R)) \
    zeroLocus {i})
  (zeroLocus s \ zeroLocus {i})
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Eq (α := Set (PrimeSpectrum R))
    (zeroLocus
        (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
          (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1))
                i) :
            R)) \
      zeroLocus {i})
    (zeroLocus s \ zeroLocus {i})
have sdiff : (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
    (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
      R)) =
  s
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
      (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
        R)) =
    s
have sdiff : ∀ (x : R),
  Membership.mem (γ := Set R)
      (Set.range fun (i : Fin (Nat.card.{u_1} (↑s : Type u_1))) ↦
        (↑((Equiv.symm (Finite.equivFin (↑s : Type u_1)) : (a : Fin (Nat.card (↑s : Type u_1))) → (↑s : Type u_1)) i) :
          R))
      x ↔
    x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s_1 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
have union : ∀ (S : ConstructibleSetData R) (hs : IsConstructible (X := PrimeSpectrum R) S.toSet),
  ∃ (S_1 : ConstructibleSetData R), S_1.toSet = S.toSet ∪ t
Tactic: obtain ⟨S, rfl⟩ := Hs
Cleared hypotheses: s, hs, Hs
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsConstructible t
Ht : ∃ (S : ConstructibleSetData R), S.toSet = t
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
⊢ ∃ (S_1 : ConstructibleSetData R), S_1.toSet = S.toSet ∪ t
have union : ∀ (T : ConstructibleSetData R) (ht : IsConstructible (X := PrimeSpectrum R) T.toSet),
  ∃ (S_1 : ConstructibleSetData R), Eq (α := Set (PrimeSpectrum R)) S_1.toSet (S.toSet ∪ T.toSet)
Tactic: obtain ⟨T, rfl⟩ := Ht
Cleared hypotheses: t, ht, Ht
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
S : ConstructibleSetData R
hs : IsConstructible (X := PrimeSpectrum R) S.toSet
T : ConstructibleSetData R
ht : IsConstructible (X := PrimeSpectrum R) T.toSet
⊢ ∃ (S_1 : ConstructibleSetData R), Eq (α := Set (PrimeSpectrum R)) S_1.toSet (S.toSet ∪ T.toSet)
have union : Eq (α := Set (PrimeSpectrum R)) (S ∪ T).toSet (S.toSet ∪ T.toSet)
Tactic: refine ⟨S ∪ T, ?_⟩
-- 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
⊢ ∃ (S : ConstructibleSetData R), S.toSet = s
have isCompact_basis : ∀ (i : R), IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))
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_1
inst : CommSemiring R
s : Set (PrimeSpectrum R)
H : IsConstructible s
isCompact_basis : ∀ (i : R), IsCompact (↑(basicOpen i) : Set (PrimeSpectrum R))
⊢ ∃ (S : ConstructibleSetData R), S.toSet = s
have 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))
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