-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δAux_ofComp (x : (Q.comp P).Ring) :
    δAux R Q ((Q.ofComp P).toAlgHom x) =
      P.toExtension.toKaehler.baseChange T (CotangentSpace.compEquiv Q P
        (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x : _)).2

Proof state:
case h_X
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (Q.comp P).vars R
n : (Q.comp P).vars
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (p * X n)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (p * X n))).2

Tactic:
simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul,
  ← @IsScalarTower.algebraMap_smul Q.Ring T, algebraMap_apply, Hom.algebraMap_toAlgHom,
  id.map_eq_id, map_aeval, RingHomCompTriple.comp_eq, comp_val, RingHom.id_apply, coe_eval₂Hom,
  IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply,
  ← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, LinearEquiv.map_add,
  LinearMapClass.map_smul, Prod.snd_add, Prod.smul_snd, LinearMap.map_add]

Result:
case h_X
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (Q.comp P).vars R
n : (Q.comp P).vars
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
⊢ eval₂ (algebraMap R T) (fun i => Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) n) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis n)).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) n •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : (Q.comp P).Ring
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom x) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x)).2

Tactic:
have : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T := IsScalarTower.left _

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : (Q.comp P).Ring
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom x) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x)).2

Proof state:
case h_add
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
x₁ x₂ : MvPolynomial (Q.comp P).vars R
hx₁ :
  (δAux R Q) ((Q.ofComp P).toAlgHom x₁) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x₁)).2
hx₂ :
  (δAux R Q) ((Q.ofComp P).toAlgHom x₂) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x₂)).2
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (x₁ + x₂)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (x₁ + x₂))).2

Tactic:
simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]

Result:
no goals

Proof state:
case h_X.inl
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
p : MvPolynomial (Q.comp P).vars R
IH :
  (δAux R Q) ((Q.ofComp P).toAlgHom p) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2
n : Q.vars
⊢ eval₂ (algebraMap R T) (fun i => Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p •
        (δAux R Q) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inl n)) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2 =
    (aeval (Q.comp P).val) p •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) ((Q.comp P).cotangentSpaceBasis (Sum.inl n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inl n) •
        (LinearMap.baseChange T P.toExtension.toKaehler)
          ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) p)).2

Tactic:
simp only [comp_vars, Sum.elim_inl, δAux_X, smul_zero, aeval_X,
  CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply, zero_add,
  Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply, LinearMap.coe_inl,
  LinearMap.coe_inr, Function.comp_apply, one_smul, map_zero]

Result:
no goals