-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.FormallySmooth.iff_injective_and_split :
    Algebra.FormallySmooth R S ↔ Function.Injective (kerCotangentToTensor R P S) ∧
      ∃ l, (KaehlerDifferential.mapBaseChange R P S) ∘ₗ l = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R P S) ∧ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Tactic:
rw [Algebra.FormallySmooth.iff_split_injection hf]

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    Function.Injective ⇑(kerCotangentToTensor R P S) ∧ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (Surjective ⇑(mapBaseChange R P S) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    Function.Injective ⇑(kerCotangentToTensor R P S) ∧ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Tactic:
refine Iff.trans (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae'
  (g := (KaehlerDifferential.mapBaseChange R P S).restrictScalars P)).out 1 0)
  (and_congr Iff.rfl ?_)

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, ↑P (mapBaseChange R P S) ∘ₗ l = LinearMap.id) ↔ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, ↑P (mapBaseChange R P S) ∘ₗ l = LinearMap.id) ↔ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Tactic:
rw [(LinearMap.extendScalarsOfSurjectiveEquiv hf).surjective.exists]

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, ↑P (mapBaseChange R P S) ∘ₗ l = LinearMap.id) ↔
    ∃ x, mapBaseChange R P S ∘ₗ (LinearMap.extendScalarsOfSurjectiveEquiv hf) x = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, ↑P (mapBaseChange R P S) ∘ₗ l = LinearMap.id) ↔
    ∃ x, mapBaseChange R P S ∘ₗ (LinearMap.extendScalarsOfSurjectiveEquiv hf) x = LinearMap.id

Tactic:
simp only [LinearMap.ext_iff, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, LinearMap.extendScalarsOfSurjective_apply, LinearMap.id_coe, id_eq]

Result:
no goals

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    Function.Injective ⇑(kerCotangentToTensor R P S) ∧ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id

Tactic:
refine (and_iff_right (KaehlerDifferential.mapBaseChange_surjective R _ _ hf)).symm.trans ?_

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ (Surjective ⇑(mapBaseChange R P S) ∧ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    Function.Injective ⇑(kerCotangentToTensor R P S) ∧ ∃ l, mapBaseChange R P S ∘ₗ l = LinearMap.id