-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma H1Cotangent.map_toInfinitesimal_bijective (P : Extension.{u} R S) :
    Function.Bijective (H1Cotangent.map P.toInfinitesimal)

Proof state:
case right.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ x ∈ LinearMap.ker P.cotangentComplex

Tactic:
simpa [← CotangentSpace.map_cotangentComplex,
  map_eq_zero_iff _ (CotangentSpace.map_toInfinitesimal_bijective P).injective] using hx

Result:
no goals

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Bijective ⇑(map P.toInfinitesimal)

Tactic:
constructor

Result:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective ⇑(map P.toInfinitesimal)

case right
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Surjective ⇑(map P.toInfinitesimal)

Proof state:
case right.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨(Cotangent.map P.toInfinitesimal) x, hx⟩

Tactic:
refine ⟨⟨x, ?_⟩, rfl⟩

Result:
case right.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ x ∈ LinearMap.ker P.cotangentComplex

Proof state:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective ⇑(map P.toInfinitesimal)

Tactic:
intro x y e

Result:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ x = y

Proof state:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ x = y

Tactic:
ext1

Result:
case left.e
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ ↑x = ↑y

Proof state:
case left.e
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : P.H1Cotangent
e : (map P.toInfinitesimal) x = (map P.toInfinitesimal) y
⊢ ↑x = ↑y

Tactic:
exact (Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)

Result:
no goals

Proof state:
case right
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Surjective ⇑(map P.toInfinitesimal)

Tactic:
intro ⟨x, hx⟩

Result:
case right
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.infinitesimal.Cotangent
hx : x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨x, hx⟩

Proof state:
case right
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.infinitesimal.Cotangent
hx : x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨x, hx⟩

Tactic:
obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x

Result:
case right.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ LinearMap.ker P.infinitesimal.cotangentComplex
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨(Cotangent.map P.toInfinitesimal) x, hx⟩