Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case hC
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)))
r : MvPolynomial σ R
x✝ : R
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B))).comp MvPolynomial.C)
        x✝) =
    MvPolynomial.coeff m✝ (((algebraMap (MvPolynomial σ R) (MvPolynomial σ B)).comp MvPolynomial.C) x✝)

pp: case hX
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)))
r : MvPolynomial σ R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B))) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((algebraMap (MvPolynomial σ R) (MvPolynomial σ B)) (MvPolynomial.X i✝))

Tactic:
<;>

Goal state after:
case hC
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)))
r : MvPolynomial σ R
x✝ : R
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      (((e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B))).comp MvPolynomial.C)
        x✝) =
    MvPolynomial.coeff m✝ (((algebraMap (MvPolynomial σ R) (MvPolynomial σ B)).comp MvPolynomial.C) x✝)

case hX
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)))
r : MvPolynomial σ R
i✝ : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((e₀.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] B))) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((algebraMap (MvPolynomial σ R) (MvPolynomial σ B)) (MvPolynomial.X i✝))