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

Proof state:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ x ⊗ₜ[P.infinitesimal.Ring] (D R P.infinitesimal.Ring) (P.toInfinitesimal.toRingHom a) =
    ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm (x ⊗ₜ[P.Ring] (D R P.Ring) a)

Tactic:
exact (tensorKaehlerQuotKerSqEquiv_symm_tmul_D _ _).symm

Result:
no goals

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
apply LinearMap.restrictScalars_injective P.Ring

Result:
case a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ ↑P.Ring (CotangentSpace.map P.toInfinitesimal) = ↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Proof state:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ (CotangentSpace.map P.toInfinitesimal) (x ⊗ₜ[P.Ring] (D R P.Ring) a) =
    ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm (x ⊗ₜ[P.Ring] (D R P.Ring) a)

Tactic:
simp only [map_tmul, id.map_eq_id, RingHom.id_apply, Hom.toAlgHom_apply]

Result:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ x ⊗ₜ[P.infinitesimal.Ring] (D R P.infinitesimal.Ring) (P.toInfinitesimal.toRingHom a) =
    ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm (x ⊗ₜ[P.Ring] (D R P.Ring) a)

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
have : IsScalarTower P.Ring P.infinitesimal.Ring S := .of_algebraMap_eq' rfl

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Proof state:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ (((AlgebraTensorModule.curry (↑P.Ring (CotangentSpace.map P.toInfinitesimal))) x).compDer (D R P.Ring)) a =
    (((AlgebraTensorModule.curry (↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm)) x).compDer (D R P.Ring)) a

Tactic:
dsimp

Result:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ (CotangentSpace.map P.toInfinitesimal) (x ⊗ₜ[P.Ring] (D R P.Ring) a) =
    ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm (x ⊗ₜ[P.Ring] (D R P.Ring) a)

Proof state:
case a
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
⊢ ↑P.Ring (CotangentSpace.map P.toInfinitesimal) = ↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
ext x a

Result:
case a.a.h.hf.H
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this✝ : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
this : IsScalarTower P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ (((AlgebraTensorModule.curry (↑P.Ring (CotangentSpace.map P.toInfinitesimal))) x).compDer (D R P.Ring)) a =
    (((AlgebraTensorModule.curry (↑P.Ring ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm)) x).compDer (D R P.Ring)) a

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
letI : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ _))

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : Algebra P.Ring P.infinitesimal.Ring := inferInstanceAs (Algebra P.Ring (P.Ring ⧸ P.ker ^ 2))
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑(CotangentSpace.map P.toInfinitesimal)

Tactic:
rw [this]

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Proof state:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
this : CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm
⊢ Function.Bijective ⇑↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm

Tactic:
exact(tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective

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 ⇑(CotangentSpace.map P.toInfinitesimal)

Tactic:
suffices CotangentSpace.map P.toInfinitesimal =
    (tensorKaehlerQuotKerSqEquiv _ _ _).symm.toLinearMap by
  rw [this]; exact(tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective

Result:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ CotangentSpace.map P.toInfinitesimal = ↑(tensorKaehlerQuotKerSqEquiv R P.Ring S).symm