-- Mathlib/RingTheory/Smooth/Basic.lean
theorem of_split [FormallySmooth R P] (g : A →ₐ[R] P ⧸ (RingHom.ker f.toRingHom) ^ 2)
    (hg : f.kerSquareLift.comp g = AlgHom.id R A) : FormallySmooth R A

Proof state:
case a.h
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯
⊢ (↑(i.comp f.kerSquareLift)).comp (Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2)) =
    (↑((Ideal.Quotient.mkₐ R I).comp l)).comp (Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2))

Tactic:
ext x

Result:
case a.h.a
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯
x : P
⊢ ((↑(i.comp f.kerSquareLift)).comp (Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2))) x =
    ((↑((Ideal.Quotient.mkₐ R I).comp l)).comp (Ideal.Quotient.mk (RingHom.ker f.toRingHom ^ 2))) x

Proof state:
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
x : P
hx : f x = 0
⊢ x ∈ Ideal.comap (lift I ⋯ (i.comp f)) I

Tactic:
have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x :)

Result:
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
x : P
hx : f x = 0
this : (Ideal.Quotient.mk I) ((lift I ⋯ (i.comp f)) x) = i (f x)
⊢ x ∈ Ideal.comap (lift I ⋯ (i.comp f)) I

Proof state:
case comp_surjective
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = i

Tactic:
let l : P ⧸ (RingHom.ker f.toRingHom) ^ 2 →ₐ[R] C := by
  refine Ideal.Quotient.liftₐ _ (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) ?_
  have : RingHom.ker f ≤ I.comap (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) := by
    rintro x (hx : f x = 0)
    have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x :)
    rwa [hx, map_zero, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero] at this
  intro x hx
  have := (Ideal.pow_right_mono this 2).trans (Ideal.le_comap_pow _ 2) hx
  rwa [hI] at this

Result:
case comp_surjective
R : Type u
inst✝⁷ : CommRing R
P A : Type u
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
f : P →ₐ[R] A
inst✝² : FormallySmooth R P
g : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
C : Type u
inst✝¹ : CommRing C
inst✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
i : A →ₐ[R] C ⧸ I
l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = i