-- 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:
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
i : P.vars
⊢ ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom (X i) =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i)

Tactic:
show (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) = _

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
i : P.vars
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i)

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, ⋯⟩
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e

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
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Proof state:
case h1.h.e.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 : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ ((Extension.Cotangent.map ((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.mk ⟨x, hx⟩)).val =
    (0 (Extension.Cotangent.mk ⟨x, hx⟩)).val

Tactic:
simp only [map_mk, Hom.toAlgHom_comp_apply, val_mk, LinearMap.zero_apply, val_zero]

Result:
case h1.h.e.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 : P.toExtension.Ring
hx : x ∈ P.toExtension.ker
⊢ Q.toExtension.ker.toCotangent ⟨((Q.ofComp P).toExtensionHom.comp (Q.toComp P).toExtensionHom).toAlgHom x, ⋯⟩ = 0

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
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
let z : (Q.comp P).ker := ⟨x - y, Ideal.sub_mem _ hx' (Ideal.mul_le_left hy)⟩

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, ⋯⟩
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    Submodule.span T ↑(LinearMap.range (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Proof state:
case 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).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
⊢ (Extension.Cotangent.mk ⟨x, hx'⟩).val = (Extension.Cotangent.mk z).val

Tactic:
simpa only [comp_vars, val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]

Result:
no goals

Proof state:
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
i : P.vars
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom (X i)) =
    ((IsScalarTower.toAlgHom R S Q.toExtension.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i)

Tactic:
simp

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.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
hx : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) (Extension.Cotangent.mk ⟨x, hx'⟩) = 0
⊢ (Q.ofComp P).toAlgHom x ∈ Q.ker ^ 2

Tactic:
simpa only [map_mk, val_mk, val_zero, Ideal.toCotangent_eq_zero] using congr(($hx).val)

Result:
no goals

Proof state:
case h2
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.Cotangent),
    (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0 →
      x ∈ LinearMap.range (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))

Tactic:
intro x hx

Result:
case h2
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.Cotangent
hx : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) x = 0
⊢ x ∈ LinearMap.range (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))