-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δ_eq (x : Q.toExtension.H1Cotangent) (y)
    (hy : Extension.Cotangent.map (ofComp Q P).toExtensionHom y = x.1) (z)
    (hz : (Extension.CotangentSpace.map (toComp Q P).toExtensionHom).liftBaseChange T z =
      (Q.comp P).toExtension.cotangentComplex y) :
    δ Q P x = P.toExtension.toKaehler.baseChange T z

Proof state:
case hy
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ?y = Extension.h1Cotangentι x

case hz
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex ?y

case y
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (Q.comp P).toExtension.Cotangent

Tactic:
exacts [hy, hz]

Result:
no goals

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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (δ Q P) x = (LinearMap.baseChange T P.toExtension.toKaehler) z

Tactic:
simp only [δ]

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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
        Q.toExtension.cotangentComplex
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
        (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Extension.h1Cotangentι ⋯
        (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯)
      x =
    (LinearMap.baseChange T P.toExtension.toKaehler) z

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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
        Q.toExtension.cotangentComplex
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
        (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Extension.h1Cotangentι ⋯
        (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯)
      x =
    (LinearMap.baseChange T P.toExtension.toKaehler) z

Tactic:
apply SnakeLemma.δ_eq

Result:
case hy
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ?y = Extension.h1Cotangentι x

case hz
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex ?y

case y
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.toExtension.H1Cotangent
y : (Q.comp P).toExtension.Cotangent
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x
z : T ⊗[S] P.toExtension.CotangentSpace
hz :
  (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
⊢ (Q.comp P).toExtension.Cotangent