-- 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)) =
    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))

Tactic:
rfl

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
hf : Function.Surjective ⇑f
inst✝ : FormallySmooth R P
a✝ : FormallySmooth R A
surj : Function.Surjective ⇑f.kerSquareLift
⊢ RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0

Tactic:
rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square, Ideal.zero_eq_bot]

Result:
no goals

Proof state:
case mpr.intro
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 : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
⊢ FormallySmooth R A

Tactic:
exact FormallySmooth.of_split f g hg

Result:
no goals

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
⊢ (f.kerSquareLift.comp
        (lift (RingHom.ker f.kerSquareLift.toRingHom) ⋯ ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm))
      x =
    (AlgHom.id R A) x

Tactic:
have :=
  (Ideal.quotientKerAlgEquivOfSurjective surj).toAlgHom.congr_arg
    (FormallySmooth.mk_lift _ ⟨2, sqz⟩
      (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom 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
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

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
⊢ FormallySmooth R A → ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
intro

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
⊢ ∃ 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
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0 := by
  rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square, Ideal.zero_eq_bot]

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
sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0
⊢ ∃ 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
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
refine
  ⟨FormallySmooth.lift _ ⟨2, sqz⟩ (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom,
    ?_⟩

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

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

Tactic:
rintro ⟨g, hg⟩

Result:
case mpr.intro
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 : A →ₐ[R] P ⧸ RingHom.ker f.toRingHom ^ 2
hg : f.kerSquareLift.comp g = AlgHom.id R A
⊢ FormallySmooth R A