-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
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)
rw :
  (↑(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) (-z)) ⋯) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
rw₁ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))
rw₂ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y + z) : S ⧸ P ^ e)
rw₃ :
  (Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) =
    HSub.hSub (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (HAdd.hAdd (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
        ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) z : S ⧸ P ^ e))
rw₄ :
  Eq (α := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (-z) : S ⧸ P ^ e)
    (-(Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) z : S ⧸ P ^ e)
rw₅ rw₆ :
  Eq (α := S ⧸ P ^ e) (-(Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) z : S ⧸ P ^ e)
    (-(Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) z : 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) (-z)) ⋯)) :
      S ⧸ P ^ e) =
    HSub.hSub (α := S ⧸ P ^ e) (β := S ⧸ P ^ e) ((Quotient.mk (P ^ e) : (a : S) → S ⧸ P ^ e) (a * y) : S ⧸ P ^ e)
      (Submodule.Quotient.mk (a * y + z))

Tactic:
rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
      sub_add_cancel_left, map_neg]

Premises used: Subtype.coe_mk, Ideal.powQuotSuccInclusion_apply_coe, map_add, sub_add_cancel_left, map_neg, Ideal.Quotient.mk_eq_mk