-- 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
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
h : x - y ∈ P
a₁ :
  (↑(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 + 1))) x)
          ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y))) ⋯) :
      S ⧸ P ^ e) =
    (↑(HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e))
            ⋯)
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
            ⋯)) :
      S ⧸ P ^ e)
a₂ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y)) =
    (↑(HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e))
            ⋯)
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
            ⋯)) :
      S ⧸ P ^ e)
a₃ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y)) =
    (↑(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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e))
            ⋯) :
        S ⧸ P ^ e) -
      (↑(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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
            ⋯) :
        S ⧸ P ^ e)
a₄ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y)) =
    HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e) -
      (↑(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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
            ⋯) :
        S ⧸ P ^ e)
⊢ (↑((p.powQuotSuccInclusion P i :
            (a : ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))) → ↥(map (Quotient.mk (P ^ e)) (P ^ i)))
          (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 + 1))) x)
            ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y))) ⋯)) :
      S ⧸ P ^ e) =
    (↑(HSub.hSub (α := ↥(map (F := S →+* S ⧸ P ^ e) (Quotient.mk (P ^ e)) (P ^ i)))
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e))
            ⋯)
          (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)
            (HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
              ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e))
            ⋯)) :
      S ⧸ P ^ e)
have a₅ : (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * (x - y)) =
  HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
      ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) x : S ⧸ P ^ e) -
    HMul.hMul (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) a : S ⧸ P ^ e)
      ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) y : S ⧸ P ^ e)
Tactic: rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Submodule.coe_sub, Subtype.coe_mk,
      Subtype.coe_mk, map_mul, map_sub, mul_sub]