-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_eq_δAux (x : Q.ker) (hx) :
    δ Q P ⟨.mk x, hx⟩ = δAux R Q x.1

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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x

Tactic:
simp only [y, Extension.Cotangent.map_mk]

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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
⊢ Extension.Cotangent.mk ⟨(Q.ofComp P).toExtensionHom.toAlgHom ↑(Q.kerCompPreimage P x), ⋯⟩ = Extension.Cotangent.mk x

Proof state:
case hz.a
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2) =
    (CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)

Tactic:
ext

Result:
case hz.a.fst
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1

case hz.a.snd
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

Proof state:
case hz.a.fst
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1

case hz.a.snd
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

Tactic:
swap

Result:
case hz.a.snd
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

case hz.a.fst
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.ker
hx : Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1