-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma Cotangent.exact :
    Function.Exact
      ((Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T)
      (Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

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 : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom x =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) x

Tactic:
congr

Result:
case e_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 : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
e_2✝ : ↥Q.toExtension.ker = ↥Q.ker
⊢ ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom =
    (IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)

Proof state:
case h2.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
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
hx : ∃ x_1 ∈ (Q.comp P).ker * (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = (Q.ofComp P).toAlgHom x
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    LinearMap.range (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
obtain ⟨y, hy, e⟩ := hx

Result:
case h2.intro.mk.intro.intro
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : (Q.ofComp P).toAlgHom y = (Q.ofComp P).toAlgHom x
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    LinearMap.range (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Proof state:
case h2.intro.mk.intro.intro
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ ∃ (x : (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker),
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩ ∈
      Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
refine ⟨?_, Submodule.subset_span ⟨Extension.Cotangent.mk ⟨w, hw⟩, ?_⟩⟩

Result:
case h2.intro.mk.intro.intro.refine_1
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker

case h2.intro.mk.intro.intro.refine_2
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Proof state:
case h2.intro.mk.intro.intro
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ w ∈
    Ideal.comap (Q.toComp P).toAlgHom.toRingHom
      (Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
        (Submodule.comap Extension.Cotangent.mk
          (Submodule.restrictScalars (Q.comp P).Ring
            (Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Ideal.mem_comap, RingHom.coe_coe,
  Submodule.mem_map, Submodule.mem_comap, Submodule.restrictScalars_mem, Submodule.coe_subtype,
  Subtype.exists, exists_and_right, exists_eq_right,
  toExtension_Ring, toExtension_commRing, toExtension_algebra₂]

Result:
case h2.intro.mk.intro.intro
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ ∃ (x : (Q.toComp P).toAlgHom w ∈ (Q.comp P).toExtension.ker),
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩ ∈
      Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))