-- 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:
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
⊢ (δ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:
letI : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance

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
⊢ (δ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_X.inr
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 : P.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.inr n)) +
      (aeval Q.val) (Sum.elim X (⇑C ∘ P.val) (Sum.inr 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.inr n))).2 +
      Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) (Sum.inr 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_inr, Function.comp_apply, algHom_C, δAux_C,
  CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
  algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
  LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
  toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]

Result:
case h_X.inr
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 : P.vars
⊢ eval₂ (algebraMap R T) (fun i => Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) i) p • 1 ⊗ₜ[S] (D R S) (P.val n) =
    (aeval (Q.comp P).val) p • 1 ⊗ₜ[S] (D R S) (P.val n)

Proof state:
case h_C
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
s : R
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (C s)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (C s))).2

Tactic:
simp only [algHom_C, δAux_C, sub_self, derivation_C, Derivation.map_algebraMap,
  tmul_zero, map_zero, add_zero, MvPolynomial.algebraMap_apply, Prod.snd_zero]

Result:
no goals