-- 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:
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
this : RingHom.ker f ≤ Ideal.comap (lift I ⋯ (i.comp f)) I
⊢ ∀ a ∈ RingHom.ker f.toRingHom ^ 2, (lift I ⋯ (i.comp f)) a = 0

Tactic:
intro x hx

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
this : RingHom.ker f ≤ Ideal.comap (lift I ⋯ (i.comp f)) I
x : P
hx : x ∈ RingHom.ker f.toRingHom ^ 2
⊢ (lift I ⋯ (i.comp f)) x = 0

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
this : RingHom.ker f ≤ Ideal.comap (lift I ⋯ (i.comp f)) I
x : P
hx : x ∈ RingHom.ker f.toRingHom ^ 2
⊢ (lift I ⋯ (i.comp f)) x = 0

Tactic:
have := (Ideal.pow_right_mono this 2).trans (Ideal.le_comap_pow _ 2) hx

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
this✝ : RingHom.ker f ≤ Ideal.comap (lift I ⋯ (i.comp f)) I
x : P
hx : x ∈ RingHom.ker f.toRingHom ^ 2
this : x ∈ Ideal.comap (lift I ⋯ (i.comp f)) (I ^ 2)
⊢ (lift I ⋯ (i.comp f)) x = 0

Proof state:
case 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)) ⋯
⊢ ↑(i.comp f.kerSquareLift) = ↑((Ideal.Quotient.mkₐ R I).comp l)

Tactic:
apply Ideal.Quotient.ringHom_ext

Result:
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))

Proof state:
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

Tactic:
exact (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x).symm

Result:
no goals

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
⊢ P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C

Tactic:
refine Ideal.Quotient.liftₐ _ (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) ?_

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
⊢ ∀ a ∈ RingHom.ker f.toRingHom ^ 2, (lift I ⋯ (i.comp f)) a = 0

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
l : P ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] C :=
  Ideal.Quotient.liftₐ (RingHom.ker f.toRingHom ^ 2) (lift I ⋯ (i.comp f)) ⋯
this : i.comp f.kerSquareLift = (Ideal.Quotient.mkₐ R I).comp l
⊢ (Ideal.Quotient.mkₐ R I).comp (l.comp g) = i

Tactic:
rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]

Result:
no goals

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
⊢ ∀ a ∈ RingHom.ker f.toRingHom ^ 2, (lift I ⋯ (i.comp f)) a = 0

Tactic:
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

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
this : RingHom.ker f ≤ Ideal.comap (lift I ⋯ (i.comp f)) I
⊢ ∀ a ∈ RingHom.ker f.toRingHom ^ 2, (lift I ⋯ (i.comp f)) a = 0