-- Mathlib/RingTheory/Smooth/Basic.lean
theorem iff_split_surjection [FormallySmooth R P] :
    FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Proof state:
case mp.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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
x : A
this :
  ↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift.toRingHom))
        ((lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) x)) =
    ↑(Ideal.quotientKerAlgEquivOfSurjective surj) (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm x)
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    (AlgHom.id R A) x

Tactic:
erw [AlgEquiv.apply_symm_apply] at this

Result:
case mp.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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
x : A
this :
  ↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift.toRingHom))
        ((lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) x)) =
    x
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    (AlgHom.id R A) 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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
⊢ FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
constructor

Result:
case mp
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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
⊢ FormallySmooth R A → ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

case mpr
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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
⊢ (∃ g, f.kerSquareLift.comp g = AlgHom.id R A) → FormallySmooth R A

Proof state:
case mp
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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
have surj : Function.Surjective f.kerSquareLift := fun x =>
  ⟨Submodule.Quotient.mk (hf x).choose, (hf x).choose_spec⟩

Result:
case mp
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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Proof state:
case mp
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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
⊢ f.kerSquareLift.comp
      (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) =
    AlgHom.id R A

Tactic:
ext x

Result:
case mp.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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
x : A
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    (AlgHom.id R A) x

Proof state:
case mp.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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
x : A
this :
  ↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift.toRingHom))
        ((lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) x)) =
    x
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    (AlgHom.id R A) x

Tactic:
conv_rhs => rw [← this, AlgHom.id_apply]

Result:
case mp.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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
x : A
this :
  ↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift.toRingHom))
        ((lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) x)) =
    x
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    ↑(Ideal.quotientKerAlgEquivOfSurjective surj)
      ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift.toRingHom))
        ((lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm) x))