Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_5.hX.none
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X none)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X none))

pp: case e'_5.hX.some
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
val✝ : α
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X (some val✝))) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X (some val✝)))

Tactic:
<;>

Goal state after:
case e'_5.hX.none
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X none)) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X none))

case e'_5.hX.some
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
σ : Type w
hσ : Finite σ
α : Type w
inst✝ : Fintype α
IH :
  ∀ {f : MvPolynomial α S},
    (algebraMap (MvPolynomial α R) (MvPolynomial α S)).IsIntegralElem f → ∀ (n : α →₀ ℕ), IsIntegral R (coeff n f)
f : MvPolynomial (Option α) S
H : (algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)).IsIntegralElem f
n m : Option α →₀ ℕ
val✝ : α
⊢ coeff m
      ((((optionEquivLeft S α).symm.toRingEquiv.toRingHom.comp
              (algebraMap (Polynomial (MvPolynomial α R)) (Polynomial (MvPolynomial α S)))).comp
          (optionEquivLeft R α).toRingEquiv.toRingHom)
        (X (some val✝))) =
    coeff m ((algebraMap (MvPolynomial (Option α) R) (MvPolynomial (Option α) S)) (X (some val✝)))