-- Mathlib/RingTheory/Smooth/Basic.lean
theorem liftOfSurjective_apply [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C)
    (hg : Function.Surjective g) (hg' : IsNilpotent <| RingHom.ker (g : B →+* C)) (x : A) :
    g (FormallySmooth.liftOfSurjective f g hg hg' x) = f x

Proof state:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.Quotient.mk (RingHom.ker ↑g))
      ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective

Result:
case a.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x))) =
    (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.Quotient.mk (RingHom.ker ↑g))
        ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x))

Proof state:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f) x

Tactic:
erw [← FormallySmooth.mk_lift _ hg'
  ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f)]

Result:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.Quotient.mk (RingHom.ker ↑g))
      ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)

Proof state:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Tactic:
change _ = ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f) x

Result:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f) x

Proof state:
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ g ((liftOfSurjective f g hg hg') x) = f x

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective

Result:
case a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Proof state:
case a.a
R : Type u
inst✝⁷ : CommSemiring R
A : Type u
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
B : Type u
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker ↑g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x))) =
    (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.Quotient.mk (RingHom.ker ↑g))
        ((lift (RingHom.ker ↑g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x))

Tactic:
simp only [liftOfSurjective, AlgEquiv.apply_symm_apply, AlgEquiv.toAlgHom_eq_coe,
  Ideal.quotientKerAlgEquivOfSurjective_apply, RingHom.kerLift_mk, RingHom.coe_coe]

Result:
no goals