-- Mathlib/RingTheory/Smooth/Basic.lean
theorem exists_lift {B : Type u} [CommRing B] [_RB : Algebra R B]
    [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) :
    ∃ f : A →ₐ[R] B, (Ideal.Quotient.mkₐ R I).comp f = g

Proof state:
case h₂.intro.intro
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g') =
    (↑this.symm).comp g
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
replace e := congr_arg this.toAlgHom.comp e

Result:
case h₂.intro.intro
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) =
    (↑this).comp ((↑this.symm).comp g)
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Proof state:
case h₁
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
intro B _ I hI _

Result:
case h₁
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
_RB✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Proof state:
case h₂.intro.intro
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) =
    (↑this).comp ((↑this.symm).comp g)
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
conv_rhs at e =>
  rw [← AlgHom.comp_assoc, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_eq_coe,
    AlgEquiv.comp_symm, AlgHom.id_comp]

Result:
case h₂.intro.intro
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) = g
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Proof state:
case h₁
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
_RB✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
exact FormallySmooth.comp_surjective I hI

Result:
no goals

Proof state:
case h₂
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
let this : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
  {
    (DoubleQuot.quotQuotEquivQuotSup I J).trans
      (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
    commutes' := fun x => rfl }

Result:
case h₂
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Proof state:
case h₂.intro.intro
R : Type u
inst✝⁵ : CommSemiring R
A : Type u
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B✝ : Type u
inst✝² : CommRing B✝
inst✝¹ : FormallySmooth R A
I✝ : Ideal B✝
hI : IsNilpotent I✝
B : Type u
inst✝ : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ : ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp
h₂ : ∀ [_RB : Algebra R (B ⧸ I)], Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp
_RB✝ : Algebra R B
g : A →ₐ[R] B ⧸ J
this : ((B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J) ≃ₐ[R] B ⧸ J :=
  let __src := (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this).comp ((Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp ((Ideal.Quotient.mkₐ R I).comp g')) = g
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
exact ⟨g', e⟩

Result:
no goals