awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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.{u_1, u_2} R (A := S) 0

Tactic:
exact isIntegral_zero

Premises used: isIntegral_zero
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 σ
revert :
  ∀ {f : MvPolynomial σ S}
    (H : RingHom.IsIntegralElem (R := MvPolynomial σ R) (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)) f)
    (n : σ →₀ ℕ), IsIntegral R (coeff n f)
⊢ IsIntegral R (coeff n f)

Tactic:
revert f n
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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)
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)
⊢ ∀ {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 _ _ _ σ

Premises used: Finite.induction_empty_option
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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) (algebraMap (MvPolynomial β R) (MvPolynomial β S)) f

Tactic:
H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : β →₀ ℕ
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))
h₁ :
  (AlgHom.toRingHom (rename (⇑e : (a : α) → β)) : (a : MvPolynomial α S) → MvPolynomial β S)
      ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f) =
    f
⊢ 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)

Tactic:
convert! H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : β →₀ ℕ
⊢ 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:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : β →₀ ℕ
⊢ (AlgHom.toRingHom (rename (⇑e : (a : α) → β)) : (a : MvPolynomial α S) → MvPolynomial β S)
      ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f) =
    f

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 : β →₀ ℕ
⊢ IsIntegral.{u_1, u_2} R (A := S)
    (coeff (Finsupp.embDomain e.symm.toEmbedding n)
      ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β S) → MvPolynomial α S) f))

Tactic:
have := @IH (rename e.symm f) (.of_map (g := (rename e).toRingHom)
      (rename_injective _ e.injective) <| .of_comp (f := (rename e.symm).toRingHom)
        (by convert! H <;> aesop)) (n.embDomain e.symm)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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:
.of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)

Premises used: RingHom.IsIntegralElem.of_map, RingHom.IsIntegralElem.of_comp, IsIntegral
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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} →₀ ℕ
refine :
  RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R) (A := MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
          (algebraMap R S))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))) :
      MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
          (a : S) → MvPolynomial PEmpty.{w + 1} S)
        (coeff n f) :
      MvPolynomial PEmpty.{w + 1} S)
⊢ IsIntegral R (coeff n f)

Tactic:
refine .of_map (g := (isEmptyAlgEquiv _ PEmpty).symm.toRingHom)
      (isEmptyAlgEquiv _ PEmpty).symm.injective
      (.of_comp (f := (isEmptyAlgEquiv _ PEmpty).toRingHom) ?_)
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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} →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R)
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)) f

Tactic:
H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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} →₀ ℕ
h :
  Eq (α := MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
        (algebraMap R S))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))))
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S))
h₁ :
  (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff n f) =
    f
⊢ RingHom.IsIntegralElem (R := MvPolynomial PEmpty.{w + 1} R) (A := MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
          (algebraMap R S))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))) :
      MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
          (a : S) → MvPolynomial PEmpty.{w + 1} S)
        (coeff n f) :
      MvPolynomial PEmpty.{w + 1} S)

Tactic:
convert! H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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} →₀ ℕ
⊢ Eq (α := MvPolynomial PEmpty.{w + 1} R →+* MvPolynomial PEmpty.{w + 1} S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))))
        (algebraMap R S))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv R PEmpty.{w + 1}))))
    (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S))

Tactic:
aesop (add simp MvPolynomial.isEmptyAlgEquiv)

Premises used: MvPolynomial.isEmptyAlgEquiv
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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} →₀ ℕ
h :
  (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff 0 f) =
    f
⊢ (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff n f) =
    f

Tactic:
obtain rfl := Subsingleton.elim n 0

Premises used: Subsingleton.elim, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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
⊢ Eq (α := MvPolynomial PEmpty.{w + 1} S →+* S) constantCoeff
    (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv S PEmpty.{w + 1})))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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
⊢ Eq (α := MvPolynomial PEmpty.{w + 1} S →+* S) constantCoeff
    (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv S PEmpty.{w + 1})))

Tactic:
have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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 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
this :
  Eq (α := MvPolynomial PEmpty.{w + 1} S →+* S) constantCoeff
    (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (isEmptyAlgEquiv S PEmpty.{w + 1})))
⊢ (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (isEmptyAlgEquiv S PEmpty.{w + 1}))) :
        (a : S) → MvPolynomial PEmpty.{w + 1} S)
      (coeff 0 f) =
    f

Tactic:
simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))

Premises used: EmbeddingLike.apply_eq_iff_eq, MvPolynomial.isEmptyAlgEquiv_apply
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
_ :
  ∀ [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)
⊢ ∀ [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:
_
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
inst_3 : Fintype α
IH :
  ∀ {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 α →₀ ℕ
⊢ RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R)
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) f

Tactic:
H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
inst_3 : Fintype α
IH :
  ∀ {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 α →₀ ℕ
h :
  Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
        (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))
h₁ :
  (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
        (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
      ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) =
    f
⊢ RingHom.IsIntegralElem (R := MvPolynomial.{w, u_1} (Option α) R) (A := MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
        (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
          (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
        (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
      MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    ((RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))) :
          (a : Polynomial (MvPolynomial α S)) → MvPolynomial (Option α) S)
        ((optionEquivLeft S α : (a : MvPolynomial (Option α) S) → Polynomial (MvPolynomial α S)) f) :
      MvPolynomial.{w, u_2} (Option α) S)

Tactic:
convert! H
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
inst_3 : Fintype α
IH :
  ∀ {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 α →₀ ℕ
h :
  ∀ (i : R) (m : Option α →₀ ℕ),
    Eq.{u_2 + 1} (α := S)
      (coeff m
        ((RingHom.comp
              (RingHom.comp
                (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                  (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
                (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
              C :
            (a : R) → MvPolynomial (Option α) S)
          i))
      (coeff m
        ((RingHom.comp (β := MvPolynomial.{w, u_1} (Option α) R)
              (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) C :
            (a : R) → MvPolynomial (Option α) S)
          i))
h₁ :
  ∀ (i : Option α) (m : Option α →₀ ℕ),
    Eq.{u_2 + 1} (α := S)
      (coeff m
        ((RingHom.comp
              (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))) :
            (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
          (X i)))
      (coeff m
        ((algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S) :
            (a : MvPolynomial (Option α) R) → MvPolynomial (Option α) S)
          (X i)))
⊢ Eq (α := MvPolynomial.{w, u_1} (Option α) R →+* MvPolynomial.{w, u_2} (Option α) S)
    (RingHom.comp
      (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
        (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
      (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
    (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S))

Tactic:
ext i m
-- Module: Mathlib.RingTheory.Polynomial.IsIntegral
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
inst_3 : Fintype α
IH :
  ∀ {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 α →₀ ℕ
i : R
m : Option α →₀ ℕ
⊢ Eq.{u_2 + 1} (α := S)
    (coeff m
      ((RingHom.comp
            (RingHom.comp
              (RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (AlgEquiv.symm (optionEquivLeft S α))))
                (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S))))
              (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (optionEquivLeft R α))))
            C :
          (a : R) → MvPolynomial (Option α) S)
        i))
    (coeff m
      ((RingHom.comp (β := MvPolynomial.{w, u_1} (Option α) R)
            (algebraMap (MvPolynomial.{w, u_1} (Option α) R) (MvPolynomial.{w, u_2} (Option α) S)) C :
          (a : R) → MvPolynomial (Option α) S)
        i))

Tactic:
aesop