-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Basic (goal)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst_3 : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b :
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i))
val : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : Membership.mem (γ := Submodule S S) (span {a}) (a * y)
hx_1 :
  Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i))
    (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z))
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ ∃ (a_1 : S ⧸ P),
    Eq (α :=
      HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
        Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
        (LinearMap.range (p.powQuotSuccInclusion P i)))
      ((p.quotientToQuotientRangePowQuotSucc P a_mem :
            (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
          a_1 :
        HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
          Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (LinearMap.range (p.powQuotSuccInclusion P i)))
      (Quot.mk
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
          (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
            Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
            (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z)) hx_1) :
        Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
            ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))
have refine : Eq (α :=
  HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
    Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
    (LinearMap.range (p.powQuotSuccInclusion P i)))
  ((p.quotientToQuotientRangePowQuotSucc P a_mem :
        (a : S ⧸ P) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range)
      (Submodule.Quotient.mk y) :
    HasQuotient.Quotient ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) (B :=
      Submodule.{u, v} (R ⧸ p) ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (LinearMap.range (p.powQuotSuccInclusion P i)))
  (Quot.mk
      (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
        ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop)
      (Subtype.mk (p := fun (x : S ⧸ P ^ e) ↦
        Membership.mem (γ := Ideal (S ⧸ P ^ e)) (map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)) x)
        (Quot.mk (⇑(Submodule.quotientRel (P ^ e)) : S → S → Prop) (a * y + z)) hx_1) :
    Quot (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
      (⇑(p.powQuotSuccInclusion P i).range.quotientRel :
        ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)) → Prop))
Tactic: refine ⟨Submodule.Quotient.mk y, ?_⟩