-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_map
    (Q : Generators.{u₁} S T) (P : Generators.{u₂} R S)
    (Q' : Generators.{u₃} S T) (P' : Generators.{u₄} R S) (f : Hom Q' Q) (x) :
    δ Q P (Extension.H1Cotangent.map f.toExtensionHom x) = δ Q' P' x

Proof state:
case mk.intro.mk
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
Q' : Generators S T
P' : Generators R S
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δ Q P)
      ⟨((Extension.Cotangent.map f.toExtensionHom).domRestrict (LinearMap.ker Q'.toExtension.cotangentComplex))
          ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx✝⟩,
        ⋯⟩ =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx✝⟩

Tactic:
simp only [LinearMap.domRestrict_apply, Extension.Cotangent.map_mk, δ_eq_δAux]

Result:
case mk.intro.mk
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
Q' : Generators S T
P' : Generators R S
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δAux R Q) (f.toExtensionHom.toAlgHom y) = (δAux R Q') y

Proof state:
case mk.intro.mk
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
Q' : Generators S T
P' : Generators R S
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
⊢ (δ Q P)
      ⟨((Extension.Cotangent.map f.toExtensionHom).domRestrict (LinearMap.ker Q'.toExtension.cotangentComplex))
          ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩,
        ⋯⟩ =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx⟩

Tactic:
replace hx : (1 : T) ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0 := by
  simpa only [LinearMap.mem_ker, Extension.cotangentComplex_mk, ker, RingHom.mem_ker] using hx

Result:
case mk.intro.mk
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
Q' : Generators S T
P' : Generators R S
f : Q'.Hom Q
this : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
y : Q'.toExtension.Ring
hy : y ∈ Q'.toExtension.ker
hx✝ : Extension.Cotangent.mk ⟨y, hy⟩ ∈ LinearMap.ker Q'.toExtension.cotangentComplex
hx : 1 ⊗ₜ[Q'.Ring] (D S Q'.Ring) y = 0
⊢ (δ Q P)
      ⟨((Extension.Cotangent.map f.toExtensionHom).domRestrict (LinearMap.ker Q'.toExtension.cotangentComplex))
          ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx✝⟩,
        ⋯⟩ =
    (δ Q' P') ⟨Extension.Cotangent.mk ⟨y, hy⟩, hx✝⟩