-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
z : M
hz : IsTorsionBy R M (p ^ pOrder hM z)
k : ℕ
f :
  LinearMap.{u, u, u, v} (RingHom.id R) (HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k))
    (HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
f1 :
  ∃ (a : M),
    Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
      ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
this :
  Membership.mem (γ := Submodule R M) (R ∙ z)
    (p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)))
a : R
ha :
  p ^ k •
      f1.choose (p := fun (a : M) ↦
        Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
          ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) =
    p ^ k • a • z
rw :
  HSub.hSub (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
      (Submodule.Quotient.mk
        (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1))))
      (Submodule.Quotient.mk (a • z)) =
    (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
rw₁ :
  Submodule.Quotient.mk
        (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1))) -
      HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) a (Submodule.Quotient.mk z) =
    (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
rw₂ :
  Submodule.Quotient.mk
        (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1))) -
      HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) a 0 =
    (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
rw₃ :
  HSub.hSub (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
      (Submodule.Quotient.mk
        (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1))))
      0 =
    (f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1
⊢ Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
    (Submodule.Quotient.mk
      (f1.choose (p := fun (a : M) ↦
          Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
            ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)) -
        a • z))
    ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
have rw₄ : Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z))
  (Submodule.Quotient.mk
    (f1.choose (p := fun (a : M) ↦
      Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ z)) (Submodule.Quotient.mk a)
        ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1))))
  ((f : (a : R ⧸ R ∙ p ^ k) → M ⧸ R ∙ z) 1)
Tactic: rw [mk_sub, mk_smul, (Quotient.mk_eq_zero _).mpr <| Submodule.mem_span_singleton_self _,
    smul_zero, sub_zero, f1.choose_spec]