-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma Cotangent.surjective_map_ofComp :
    Function.Surjective (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 : Q.toExtension.Cotangent
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = x

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Result:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

Proof state:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

Tactic:
have : x ∈ Q.ker := hx

Result:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : x ∈ Q.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

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.Surjective ⇑(Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

Tactic:
intro x

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.Cotangent
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = x

Proof state:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

Tactic:
obtain ⟨x, hx', rfl⟩ := this

Result:
case 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).ker
hx : (Q.ofComp P).toAlgHom x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨(Q.ofComp P).toAlgHom x, hx⟩

Proof state:
case 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).ker
hx : (Q.ofComp P).toAlgHom x ∈ Q.toExtension.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨(Q.ofComp P).toAlgHom x, hx⟩

Tactic:
exact ⟨.mk ⟨x, hx'⟩, Extension.Cotangent.map_mk _ _⟩

Result:
no goals

Proof state:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : x ∈ Q.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

Tactic:
rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective
  _ (toAlgHom_ofComp_surjective Q P)] at this

Result:
case 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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩