awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have mp : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
Tactic: refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
mp : ∀ (H : IsIntegral (MvPolynomial σ R) f) (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f ↔ ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have refine : ∀ (H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)), IsIntegral (MvPolynomial σ R) f
Tactic: refine ⟨fun H n ↦ ?mp, fun H ↦ ?mpr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) f
have rw : IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
  (∑ v ∈ f.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v f))
Tactic: rw [← f.support_sum_monomial_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ v ∈ f.support, (monomial v : (a : S) → MvPolynomial σ S) (coeff v f))
have simp_rw : IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
  (∑ x ∈ f.support,
    HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
      ((C : (a : S) → MvPolynomial σ S) (coeff x f) : MvPolynomial σ S)
      (x.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ S) (X n) e : MvPolynomial σ S))
Tactic: simp_rw [monomial_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S)
    (∑ x ∈ f.support,
      HMul.hMul (α := MvPolynomial σ S) (β := MvPolynomial σ S)
        ((C : (a : S) → MvPolynomial σ S) (coeff x f) : MvPolynomial σ S)
        (x.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial σ S) (X n) e : MvPolynomial σ S))
have refine : ∀ n ∈ f.support, ∀ i ∈ n.support, IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S) (X i)
Tactic: refine IsIntegral.sum _ fun n _ ↦ .mul ((H n).map (Algebra.ofId _ _)).tower_top
      (.prod _ fun i _ ↦ .pow ?_ _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : ∀ (n : σ →₀ ℕ), IsIntegral R (coeff n f)
n : σ →₀ ℕ
h : n ∈ f.support
i : σ
h_1 : i ∈ n.support
⊢ IsIntegral (MvPolynomial σ R) (A := MvPolynomial σ S) (X i)
have h : Eq (α := MvPolynomial σ S) (X i)
  ((algebraMap (MvPolynomial σ R) (MvPolynomial σ S) : (a : MvPolynomial σ R) → MvPolynomial σ S) (X i))
Tactic: convert! isIntegral_algebraMap (x := MvPolynomial.X i)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
⊢ IsIntegral R (coeff n f)
have mp : ∀
  (this :
    ∀ {σ : Type w} {f : MvPolynomial σ S}
      (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
      (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f))
  (hσ : ¬Finite σ), IsIntegral R (coeff n f)
Tactic: wlog hσ : Finite σ generalizing σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
mp :
  ∀
    (this :
      ∀ {σ : Type w} {f : MvPolynomial σ S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
        (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f))
    (hσ : ¬Finite σ), IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)
have wlog : ∀ {σ : Type w} {f : MvPolynomial σ S}
  (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f) (n : σ →₀ ℕ)
  (hσ : Finite σ), IsIntegral R (coeff n f)
Tactic: wlog hσ : Finite σ generalizing σ
Cleared hypotheses: σ, f, H, n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
⊢ IsIntegral R (coeff n f)
have mp : ∀ (g : MvPolynomial.{w, u_2} (↥f.vars) S)
  (hg :
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f),
  IsIntegral R (coeff n f)
Tactic: obtain ⟨g, hg⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range (τ := f.vars) f _
      Subtype.val_injective (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
⊢ IsIntegral R (coeff n f)
have pos : ∀
  (hn :
    Membership.mem (γ := Set (σ →₀ ℕ))
      (Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))) n),
  IsIntegral R (coeff n f)
Tactic: by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
pos :
  ∀
    (hn :
      Membership.mem (γ := Set (σ →₀ ℕ))
        (Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))) n),
    IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)
have neg : ∀ (hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))),
  IsIntegral R (coeff n f)
Tactic: by_cases hn : n ∈ Set.range (Finsupp.mapDomain ((↑) : f.vars → σ))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn :
  Membership.mem (γ := Set (σ →₀ ℕ))
    (Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))) n
⊢ IsIntegral R (coeff n f)
have pos : ∀ (n : ↥f.vars →₀ ℕ), IsIntegral R (coeff (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) n) f)
Tactic: obtain ⟨n, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) n) f)
have pos : IsIntegral R (coeff n g)
Tactic: simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial σ R) (A := MvPolynomial σ S)
    (RingHom.comp (β := MvPolynomial.{w, u_1} (↥f.vars) R)
        (RingHom.comp (β := MvPolynomial.{w, u_2} (↥f.vars) S)
          (AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))))
          (algebraMap (MvPolynomial.{w, u_1} (↥f.vars) R) (MvPolynomial.{w, u_2} (↥f.vars) S)))
        (AlgHom.toRingHom (killCompl ⋯)) :
      MvPolynomial σ R →+* MvPolynomial σ S)
    ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) :
          (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S)
        g :
      MvPolynomial σ S)
have simp : RingHom.IsIntegralElem
  (RingHom.comp
    (RingHom.comp
      (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
      (map (algebraMap R S)))
    (↑(killCompl sorry) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
  f
Tactic: simp only [AlgHom.toRingHom_eq_coe, algebraMap_def, RingHom.coe_coe, hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ RingHom.IsIntegralElem
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    f
have h : Eq (α := MvPolynomial σ R →+* MvPolynomial σ S)
  (RingHom.comp
    (RingHom.comp
      (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
      (map (algebraMap R S)))
    (↑(killCompl sorry) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
  (RingHom.comp
    (AlgHom.toRingHom
      (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
        (killCompl sorry)))
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)))
Tactic: convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
h :
  Eq (α := MvPolynomial σ R →+* MvPolynomial σ S)
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    (RingHom.comp
      (AlgHom.toRingHom
        (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
          (killCompl ⋯)))
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)))
⊢ RingHom.IsIntegralElem
    (RingHom.comp
      (RingHom.comp
        (↑(rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars))) : MvPolynomial (↥f.vars) S →+* MvPolynomial σ S)
        (map (algebraMap R S)))
      (↑(killCompl ⋯) : MvPolynomial σ R →+* MvPolynomial (↥f.vars) R))
    f
have h₁ : f =
  (AlgHom.toRingHom
        (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
          (killCompl sorry)) :
      (a : MvPolynomial σ S) → MvPolynomial σ S)
    f
Tactic: convert!
          H.map
            ((rename Subtype.val).comp
                (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
n : ↥f.vars →₀ ℕ
⊢ f =
    (AlgHom.toRingHom
          (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
            (killCompl ⋯)) :
        (a : MvPolynomial σ S) → MvPolynomial σ S)
      f
have h : Eq (α := MvPolynomial σ S)
  ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g :
    MvPolynomial σ S)
  ((AlgHom.toRingHom
          (AlgHom.comp (B := MvPolynomial.{w, u_2} (↥f.vars) S) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
            (killCompl sorry)) :
        (a : MvPolynomial σ S) → MvPolynomial σ S)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g) :
    MvPolynomial σ S)
Tactic: nth_rw 1 12 [← hg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ) (hσ : Finite σ), IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial.{w, u_2} (↥f.vars) S
hg : (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)) : (a : MvPolynomial (↥f.vars) S) → MvPolynomial σ S) g = f
hn : n ∉ Set.range (ι := ↥f.vars →₀ ℕ) (Finsupp.mapDomain (Subtype.val (p := fun (x : σ) ↦ x ∈ f.vars)))
⊢ IsIntegral R (coeff n f)
have neg : IsIntegral.{u_1, u_2} R (A := S) 0
Tactic: rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f
n : σ →₀ ℕ
hσ : Finite σ
⊢ IsIntegral R (coeff n f)
have revert : ∀ {f : MvPolynomial σ S}
  (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
  (n : σ →₀ ℕ), IsIntegral R (coeff n f)
Tactic: revert f n
Cleared hypotheses: f, H, n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
⊢ ∀ {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have apply : ∀ {α β : Type w} (a : α ≃ β),
  (∀ {f : MvPolynomial α S}
      (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
      (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
    ∀ {f : MvPolynomial β S}
      (H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f)
      (n : β →₀ ℕ), IsIntegral R (coeff n f)
Tactic: apply Finite.induction_empty_option _ _ _ σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
apply :
  ∀ {α β : Type w} (a : α ≃ β),
    (∀ {f : MvPolynomial α S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
        (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial β S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f)
        (n : β →₀ ℕ), IsIntegral R (coeff n f)
⊢ ∀ {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have apply₁ : ∀ {f : MvPolynomial PEmpty.{w + 1} S}
  (H :
    RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
      (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f)
  (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)
Tactic: apply Finite.induction_empty_option _ _ _ σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
apply :
  ∀ {α β : Type w} (a : α ≃ β),
    (∀ {f : MvPolynomial α S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
        (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
      ∀ {f : MvPolynomial β S}
        (H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f)
        (n : β →₀ ℕ), IsIntegral R (coeff n f)
apply₁ :
  ∀ {f : MvPolynomial PEmpty.{w + 1} S}
    (H :
      RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
        (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f)
    (n : PEmpty.{w + 1} →₀ ℕ), IsIntegral R (coeff n f)
⊢ ∀ {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
have apply₂ : ∀ {α : Type w} [Fintype α],
  (∀ {f : MvPolynomial α S}
      (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
      (n : α →₀ ℕ), IsIntegral R (coeff n f)) →
    ∀ {f : MvPolynomial.{w, u_2} (Option α) S}
      (H :
        RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
          (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f)
      (n : Option α →₀ ℕ), IsIntegral R (coeff n f)
Tactic: apply Finite.induction_empty_option _ _ _ σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.IsIntegral (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ : Type w
hσ : Finite σ
α β : Type w
e : α ≃ β
IH :
  ∀ {f : MvPolynomial α S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial α R) (algebraMap (MvPolynomial α R) (MvPolynomial α S)) f)
    (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial β S
H : RingHom.IsIntegralElem (R := MvPolynomial β R) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f
n : β →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial β R) (A := MvPolynomial β S)
    (RingHom.comp (β := MvPolynomial α R)
        (RingHom.comp (β := MvPolynomial α S) (AlgHom.toRingHom (rename (⇑e : (a : α) → β)))
          (algebraMap (MvPolynomial α R) (MvPolynomial α S)))
        (AlgHom.toRingHom (rename (⇑e.symm : (a : β) → α))) :
      MvPolynomial β R →+* MvPolynomial β S)
    ((AlgHom.toRingHom (rename (⇑e : (a : α) → β)) : (a : MvPolynomial α S) → MvPolynomial β S)
        ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f) :
      MvPolynomial β S)
have h : Eq (α := MvPolynomial β R →+* MvPolynomial β S)
  (RingHom.comp (β := MvPolynomial α R)
    (RingHom.comp (β := MvPolynomial α S) (AlgHom.toRingHom (rename (⇑e : (a : α) → β)))
      (algebraMap (MvPolynomial α R) (MvPolynomial α S)))
    (AlgHom.toRingHom (rename (⇑e.symm : (a : β) → α))))
  (algebraMap (MvPolynomial β R) (MvPolynomial β S))
Tactic: convert! H