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

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

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

Result:
case left.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : (map P.toInfinitesimal) (mk x) = 0
⊢ mk x = 0

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
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.infinitesimal.Cotangent
⊢ ∃ a, (map P.toInfinitesimal) a = x

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

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

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : (map P.toInfinitesimal) (mk x) = 0
⊢ ↑x ∈ P.ker ^ 2

Tactic:
apply_fun Cotangent.val at hx

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : ((map P.toInfinitesimal) (mk x)).val = val 0
⊢ ↑x ∈ P.ker ^ 2

Proof state:
case left.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx✝ : (map P.toInfinitesimal) (mk x) = 0
hx : ↑x ∈ P.ker ^ 2
⊢ mk x = 0

Tactic:
ext

Result:
case left.intro.e
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx✝ : (map P.toInfinitesimal) (mk x) = 0
hx : ↑x ∈ P.ker ^ 2
⊢ (mk x).val = val 0

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:
rw [injective_iff_map_eq_zero]

Result:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ∀ (a : P.Cotangent), (map P.toInfinitesimal) a = 0 → a = 0

Proof state:
case right.intro.mk.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx⟩

Tactic:
rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx

Result:
case right.intro.mk.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx✝ : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
hx : x ∈ P.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx✝⟩

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2

Tactic:
simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
  Ideal.Quotient.eq_zero_iff_mem] using hx

Result:
no goals

Proof state:
case right.intro.mk.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx✝ : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
hx : x ∈ P.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx✝⟩

Tactic:
exact ⟨.mk ⟨x, hx⟩, rfl⟩

Result:
no goals

Proof state:
case left.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : (map P.toInfinitesimal) (mk x) = 0
⊢ mk x = 0

Tactic:
have hx : x.1 ∈ P.ker ^ 2 := by
  apply_fun Cotangent.val at hx
  simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
    Extension.ker_infinitesimal] at hx
  rw [Ideal.cotangentIdeal_square] at hx
  simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
    Ideal.Quotient.eq_zero_iff_mem] using hx

Result:
case left.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx✝ : (map P.toInfinitesimal) (mk x) = 0
hx : ↑x ∈ P.ker ^ 2
⊢ mk x = 0

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ P.ker.cotangentIdeal ^ 2
⊢ ↑x ∈ P.ker ^ 2

Tactic:
rw [Ideal.cotangentIdeal_square] at hx

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ ⊥
⊢ ↑x ∈ P.ker ^ 2

Proof state:
case left
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ∀ (a : P.Cotangent), (map P.toInfinitesimal) a = 0 → a = 0

Tactic:
intro x hx

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

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : ((map P.toInfinitesimal) (mk x)).val = val 0
⊢ ↑x ∈ P.ker ^ 2

Tactic:
simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
  Extension.ker_infinitesimal] at hx

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx : P.toInfinitesimal.toRingHom ↑x ∈ P.ker.cotangentIdeal ^ 2
⊢ ↑x ∈ P.ker ^ 2

Proof state:
case left.intro.e
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : ↥P.ker
hx✝ : (map P.toInfinitesimal) (mk x) = 0
hx : ↑x ∈ P.ker ^ 2
⊢ (mk x).val = val 0

Tactic:
simpa [Ideal.toCotangent_eq_zero]

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

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
⊢ ∃ a, (map P.toInfinitesimal) a = x

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

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case right.intro.mk.intro
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Ring
hx : (Ideal.Quotient.mk (P.ker ^ 2)) x ∈ P.infinitesimal.ker
⊢ ∃ a, (map P.toInfinitesimal) a = mk ⟨(Ideal.Quotient.mk (P.ker ^ 2)) x, hx⟩