-- 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:
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : A →ₐ[R] B ⧸ I
⊢ ∃ f, (Ideal.Quotient.mkₐ R I).comp f = g

Tactic:
revert g

Result:
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g : A →ₐ[R] B ⧸ I), ∃ f, (Ideal.Quotient.mkₐ R I).comp f = 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 J : Ideal S),
    I ≤ J →
      (∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [_RB : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

Tactic:
intro B _ I J hIJ h₁ h₂ _ g

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
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

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

Tactic:
revert _RB

Result:
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
⊢ ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

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✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [_RB : Algebra R B], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
apply Ideal.IsNilpotent.induction_on (S := 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
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp

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 J : Ideal S),
    I ≤ J →
      (∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [_RB : Algebra R (S ⧸ I)],
            Function.Surjective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [_RB : Algebra R S], Function.Surjective (Ideal.Quotient.mkₐ R J).comp

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

Tactic:
obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)

Result:
case h₂.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 ⧸ I
e : (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp g' = (↑this.symm).comp g
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Proof state:
case h₂.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 ⧸ I
e : (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp g' = (↑this.symm).comp g
⊢ ∃ a, (Ideal.Quotient.mkₐ R J).comp a = g

Tactic:
obtain ⟨g', rfl⟩ := h₁ g'

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

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u
inst✝¹ : CommRing B
_RB : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g : A →ₐ[R] B ⧸ I), ∃ f, (Ideal.Quotient.mkₐ R I).comp f = g

Tactic:
change Function.Surjective (Ideal.Quotient.mkₐ R I).comp

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