-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
b : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤
x : R
hx : x ∈ I ^ n
⊢ Eq.{u_1 + 1} (α := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              ⋯ :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ⋯ :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              ⋯ :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        b) →
    Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx) = b
have refine_3 : ∀ (y : R) (hy : y ∈ I ^ n),
  Eq.{u_1 + 1} (α := ↥(map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              sorry :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx)))
      ((fun (c : ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤) ↦
          (Subtype.mk (p := fun (x : R ⧸ I ^ (n + 1)) ↦
              Membership.mem (γ := Submodule R (R ⧸ I ^ (n + 1)))
                (Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n))) x)
              (((HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤).mapQ (I ^ (n + 1)) (Submodule.subtype (I ^ n)) sorry :
                  (a : ↥(I ^ n) ⧸ I • ⊤) → R ⧸ I ^ (n + 1))
                c)
              sorry :
            ↥(Submodule.restrictScalars R (map (F := R →+* R ⧸ I ^ (n + 1)) (Quotient.mk (I ^ (n + 1))) (I ^ n)))))
        (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy))) →
    Eq (α := ↥(I ^ n) ⧸ HSMul.hSMul (β := Submodule R ↥(I ^ n)) I ⊤)
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) x hx))
      (Submodule.Quotient.mk (Subtype.mk (p := fun (x : R) ↦ x ∈ I ^ n) y hy))
Tactic: obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b
Cleared hypotheses: b