awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)
h1M : 1 ≤ M
U : ConstructibleSetData R
hU₁ : comap MvPolynomial.C '' T.toSet = U.toSet
hU₂ :
  ∀ C ∈ U,
    C.n ≤
        numBound S'.degBound
          (fun (i : ℕ) ↦
            1 +
              (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                Multiset.count i (Multiset.map Fin.val B))
          n ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          M ^
            ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
              degBound S'.degBound
                (fun (i : ℕ) ↦
                  1 +
                    (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                      Multiset.count i (Multiset.map Fin.val B))
                n)
t : ℕ
ht : t + 1 < n + 1
⊢ t < n

Tactic:
simp only [add_lt_add_iff_right] at ht

Premises used: add_lt_add_iff_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)
h1M : 1 ≤ M
U : ConstructibleSetData R
hU₁ : comap MvPolynomial.C '' T.toSet = U.toSet
hU₂ :
  ∀ C ∈ U,
    C.n ≤
        numBound S'.degBound
          (fun (i : ℕ) ↦
            1 +
              (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                Multiset.count i (Multiset.map Fin.val B))
          n ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          M ^
            ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
              degBound S'.degBound
                (fun (i : ℕ) ↦
                  1 +
                    (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                      Multiset.count i (Multiset.map Fin.val B))
                n)
t : ℕ
ht_1 : t + 1 < n + 1
ht : t < n
⊢ 1 + Multiset.count (⟨t, ht⟩ : Fin n) B ≤ 1 + Multiset.count (⟨t + 1, ht_1⟩ : Fin (n + 1)) d

Tactic:
simp [B]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
x : R
⊢ Eq (α := MvPolynomial (Fin m) R)
    ((RingHom.comp (β := MvPolynomial (Fin n) R)
            (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
            MvPolynomial.C :
          (a : R) → MvPolynomial (Fin m) R)
        x :
      MvPolynomial (Fin m) R)
    ((RingHom.comp (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R) MvPolynomial.C :
          (a : R) → MvPolynomial (Fin m) R)
        x :
      MvPolynomial (Fin m) R)

Tactic:
simp [g]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
x : Fin n
m_1 : Fin m →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (MvPolynomial.coeff m_1
      ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) :
          (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R)
        (MvPolynomial.X x)))
    (MvPolynomial.coeff m_1
      (((↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R) :
          (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R)
        (MvPolynomial.X x)))

Tactic:
simp [g]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ 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]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)
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)))
⊢ g.comp σ = RingHom.id (MvPolynomial (Fin m) R)

Tactic:
ext : 2
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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))
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:
simp [g, σ]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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))
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:
simp [g, σ]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)

Tactic:
have hσ : g.comp σ = .id _ := by ext : 2 <;> simp [g, σ]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)
⊢ ∀ (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
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ 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σ'
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
C : BasicConstructibleSetData R
⊢ map (RingHom.id R) C = C

Tactic:
simp [map]

Premises used: PrimeSpectrum.BasicConstructibleSetData.map
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
h : ∀ (x : BasicConstructibleSetData R), map (RingHom.id R) x = id x
⊢ map (RingHom.id R) = id

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
x : BasicConstructibleSetData R
⊢ map (RingHom.id R) x = id x

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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
C : BasicConstructibleSetData R
⊢ map (φ.comp ψ) C = map φ (map ψ C)

Tactic:
simp [map, Function.comp_def]

Premises used: Function.comp_def, PrimeSpectrum.BasicConstructibleSetData.map
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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
h : ∀ (x : BasicConstructibleSetData R), map (φ.comp ψ) x = (map φ ∘ map ψ) x
⊢ map (φ.comp ψ) = map φ ∘ map ψ

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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
x : BasicConstructibleSetData R
⊢ map (φ.comp ψ) x = (map φ ∘ map ψ) x

Tactic:
simp [map_comp]

Premises used: PrimeSpectrum.BasicConstructibleSetData.map_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
φ : R →+* S
C : BasicConstructibleSetData R
⊢ (map φ C).toSet = comap φ ⁻¹' C.toSet

Tactic:
simp [toSet, map, ← Set.range_comp]

Premises used: Set.range_comp, PrimeSpectrum.BasicConstructibleSetData.toSet, PrimeSpectrum.BasicConstructibleSetData.map
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
s : ConstructibleSetData R
⊢ map (RingHom.id R) s = s

Tactic:
simp [map]

Premises used: PrimeSpectrum.ConstructibleSetData.map
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : S →+* T
g : R →+* S
s : ConstructibleSetData R
⊢ map (f.comp g) s = map f (map g s)

Tactic:
simp [map, image_image, Function.comp_def, BasicConstructibleSetData.map_comp']

Premises used: PrimeSpectrum.BasicConstructibleSetData.map_comp', Function.comp_def, PrimeSpectrum.ConstructibleSetData.map, Finset.image_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
rw : ⋃ y ∈ s, (BasicConstructibleSetData.map f y).toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet
⊢ ⋃ C ∈ image (BasicConstructibleSetData.map f) s, C.toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet

Tactic:
rw [set_biUnion_finset_image]

Premises used: Finset.set_biUnion_finset_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ y ∈ s, (BasicConstructibleSetData.map f y).toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
⊢ IsConstructible (X := PrimeSpectrum R) S.toSet

Tactic:
.biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_

Premises used: Topology.IsConstructible.biUnion, Finset.finite_toSet, Topology.IsConstructible.sdiff, PrimeSpectrum.ConstructibleSetData.toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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))
refine_2 : ∀ x ∈ (↑S : Set (BasicConstructibleSetData R)), IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})
⊢ IsConstructible (X := PrimeSpectrum R) S.toSet

Tactic:
refine .biUnion S.finite_toSet fun _ _ ↦ .sdiff ?_ ?_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
x : BasicConstructibleSetData R
h : x ∈ (↑S : Set (BasicConstructibleSetData R))
refine_1 : IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))ᶜ
⊢ IsConstructible (X := PrimeSpectrum R) (zeroLocus (Set.range x.g))

Tactic:
rw [← isConstructible_compl]

Premises used: Topology.isConstructible_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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))ᶜ

Tactic:
(isRetrocompact_zeroLocus_compl (Set.finite_range _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.finite_range, PrimeSpectrum.isRetrocompact_zeroLocus_compl, IsRetrocompact.isConstructible
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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))ᶜ

Tactic:
exact (isRetrocompact_zeroLocus_compl (Set.finite_range _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.finite_range, PrimeSpectrum.isRetrocompact_zeroLocus_compl, IsRetrocompact.isConstructible
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
Goal:
R : Type u_1
inst : CommSemiring R
S : ConstructibleSetData R
x : BasicConstructibleSetData R
h : x ∈ (↑S : Set (BasicConstructibleSetData R))
refine_2 : IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})ᶜ
⊢ IsConstructible (X := PrimeSpectrum R) (zeroLocus {x.f})

Tactic:
rw [← isConstructible_compl]

Premises used: Topology.isConstructible_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
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})ᶜ

Tactic:
(isRetrocompact_zeroLocus_compl (Set.finite_singleton _)).isConstructible
      (isClosed_zeroLocus _).isOpen_compl

Premises used: IsClosed.isOpen_compl, PrimeSpectrum.isRetrocompact_zeroLocus_compl, IsRetrocompact.isConstructible, Set.finite_singleton