Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case ha
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
i✝ : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val)).comp
          Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝
      ((((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁).comp Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝))

pp: case hb
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
x✝ : ↥(integralClosure R B)
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R
              ((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val))).comp
          Algebra.TensorProduct.includeRight)
        x✝) =
    MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R ((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁)).comp
          Algebra.TensorProduct.includeRight)
        x✝)

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
i✝ : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val)).comp
          Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝
      ((((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁).comp Algebra.TensorProduct.includeLeft)
        (MvPolynomial.X i✝))

case hb
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing B
inst✝ : Algebra R B
σ : Type u_4
x : MvPolynomial σ R ⊗[R] B
hx : x ∈ integralClosure (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B)
e₀ : MvPolynomial σ R ⊗[R] B ≃ₐ[R] MvPolynomial σ B :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) B).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R B))
e₁ : MvPolynomial σ R ⊗[R] ↥(integralClosure R B) ≃ₐ[R] MvPolynomial σ ↥(integralClosure R B) :=
  (Algebra.TensorProduct.comm R (MvPolynomial σ R) ↥(integralClosure R B)).trans
    (AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R ↥(integralClosure R B)))
e : MvPolynomial σ R ⊗[R] B ≃ₐ[MvPolynomial σ R] MvPolynomial σ B :=
  let __RingEquiv := e₀.toRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : ∀ (n : σ →₀ ℕ), IsIntegral R (MvPolynomial.coeff n (e x))
y : MvPolynomial σ R ⊗[R] ↥(integralClosure R B)
hy : (MvPolynomial.map (integralClosure R B).val.toRingHom) (e₁ y) = e x
x✝ : ↥(integralClosure R B)
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R
              ((↑e₀).comp (Algebra.TensorProduct.map (AlgHom.id R (MvPolynomial σ R)) (integralClosure R B).val))).comp
          Algebra.TensorProduct.includeRight)
        x✝) =
    MvPolynomial.coeff m✝
      (((AlgHom.restrictScalars R ((MvPolynomial.mapAlgHom (integralClosure R B).val).comp ↑e₁)).comp
          Algebra.TensorProduct.includeRight)
        x✝)