-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.Extension.formallySmooth_iff_split_injection
    (P : Algebra.Extension.{u} R S) [FormallySmooth R P.Ring] :
    Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Proof state:
case e
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ ({ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun (r • m)).val =
    ((RingHom.id P.Ring) r • { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun m).val

Tactic:
simp

Result:
case e
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ Cotangent.val (r • m) = r • Cotangent.val m

Proof state:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_

Result:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Proof state:
case mp
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
intro ⟨l, hl⟩

Result:
case mp
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[P.Ring] (RingHom.ker (algebraMap P.Ring S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id
⊢ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Proof state:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
constructor

Result:
case mp
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

case mpr
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id

Proof state:
case mpr
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : P.CotangentSpace →ₗ[S] P.Cotangent
hl : l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id

Tactic:
exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
  LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Result:
no goals

Proof state:
case mp
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[P.Ring] (RingHom.ker (algebraMap P.Ring S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id
⊢ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
  LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Result:
no goals

Proof state:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
let e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  { __ := AddEquiv.refl _, map_smul' r m := by ext1; simp; rfl }

Result:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id) ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Proof state:
case e
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ Cotangent.val (r • m) = r • Cotangent.val m

Tactic:
rfl

Result:
no goals

Proof state:
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun (r • m) =
    (RingHom.id P.Ring) r • { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun m

Tactic:
ext1

Result:
case e
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ ({ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun (r • m)).val =
    ((RingHom.id P.Ring) r • { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun m).val

Proof state:
case mpr
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id

Tactic:
intro ⟨l, hl⟩

Result:
case mpr
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Extension R S
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
l : P.CotangentSpace →ₗ[S] P.Cotangent
hl : l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring S = LinearMap.id