Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι := ⋯
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring := ⋯
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring := ⋯
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := ⋯
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ⋯
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S := ⋯
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ := ⋯
i j : σ
⊢ (algebraMap P'.Ring S).mapMatrix P'.jacobiMatrix i j =
    (algebraMap P.Ring S) (e ((MvPolynomial.pderiv i) (e.symm (P.relation j))))

pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι := ⋯
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring := ⋯
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring := ⋯
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := ⋯
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ⋯
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S := ⋯
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ := ⋯
i j : σ
⊢ (algebraMap P.Ring S) (e ((MvPolynomial.pderiv i) (e.symm (P.relation j)))) =
    (algebraMap P.Ring S).mapMatrix P.jacobiMatrix i j

Tactic:
· simpa [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, P',
          Algebra.Generators.ofSurjective] using congr($H _)

Goal state after:
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι := ⋯
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring := ⋯
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring := ⋯
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := ⋯
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ⋯
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S := ⋯
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ := ⋯
i j : σ
⊢ (algebraMap P.Ring S) (e ((MvPolynomial.pderiv i) (e.symm (P.relation j)))) =
    (algebraMap P.Ring S).mapMatrix P.jacobiMatrix i j