-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma exact_map_δ :
    Function.Exact (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) (δ Q P)

Proof state:
case hF
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
⊢ Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι =
    Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
ext x

Result:
case hF.h.e
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).toExtension.H1Cotangent
⊢ ((Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι) x).val =
    ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) x).val

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
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
    ⇑(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) ⋯ ⋯ ⋯)

Tactic:
apply SnakeLemma.exact_δ_right
  (ι₂ := (Q.comp P).toExtension.h1Cotangentι)
  (hι₂ := LinearMap.exact_subtype_ker_map _)

Result:
case hF
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
⊢ Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι =
    Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

case h
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
⊢ Function.Injective ⇑Extension.h1Cotangentι

Proof state:
case hF.h.e
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).toExtension.H1Cotangent
⊢ ((Extension.Cotangent.map (Q.ofComp P).toExtensionHom ∘ₗ Extension.h1Cotangentι) x).val =
    ((Extension.h1Cotangentι ∘ₗ Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) x).val

Tactic:
rfl

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
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)

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
⊢ Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
    ⇑(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) ⋯ ⋯ ⋯)

Proof state:
case h
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
⊢ Function.Injective ⇑Extension.h1Cotangentι

Tactic:
exact Subtype.val_injective

Result:
no goals