-- Module: Mathlib.RingTheory.Ideal.Quotient.Operations
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
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)) ⋯ :
                    (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)))))
          (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))
⊢ 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

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b

Premises used: Submodule.Quotient.mk_surjective, rfl