-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
i : Fin d
h :
  Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (Submodule.Quotient.mk
          ((DirectSum.toModule R (Fin d) (M := fun (i : Fin d) ↦
                HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) M fun (i : Fin d) ↦
                liftQSpanSingleton (p ^ k i)
                  (LinearMap.toSpanSingleton R M
                    (⋯.choose (p := fun (x : M) ↦
                      p ^ k i • x = 0 ∧
                        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          (((DirectSum.lof R (Fin d)
                                    (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                              1 :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))))
                  ⋯ :
              (a : ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) → M)
            (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                  (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                (Submodule.Quotient.mk 1) :
              ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    ((LinearMap.id : (a : ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
              HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
            (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
          (Submodule.Quotient.mk 1)) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h₁ :
  Eq (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (Submodule.Quotient.mk
          ((DirectSum.toModule R (Fin d) (M := fun (i : Fin d) ↦
                HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) M fun (i : Fin d) ↦
                liftQSpanSingleton (p ^ k i)
                  (LinearMap.toSpanSingleton R M
                    (⋯.choose (p := fun (x : M) ↦
                      p ^ k i • x = 0 ∧
                        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          (((DirectSum.lof R (Fin d)
                                    (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                              1 :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))))
                  ⋯ :
              (a : ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) → M)
            (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                  (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                (Submodule.Quotient.mk 1) :
              ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
              ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
          (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (Submodule.Quotient.mk 1) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    (((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (Submodule.Quotient.mk
          ((DirectSum.toModule R (Fin d) (M := fun (i : Fin d) ↦
                HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) M fun (i : Fin d) ↦
                liftQSpanSingleton (p ^ k i)
                  (LinearMap.toSpanSingleton R M
                    (⋯.choose (p := fun (x : M) ↦
                      p ^ k i • x = 0 ∧
                        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                          (((DirectSum.lof R (Fin d)
                                    (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                              1 :
                            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))))
                  ⋯ :
              (a : ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) → M)
            (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                  (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                (Submodule.Quotient.mk 1) :
              ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
    ((LinearMap.id : (a : ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
        (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
              HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
            (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
          (Submodule.Quotient.mk 1)) :
      ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
have h₂ : Eq (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
  ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
      (Submodule.Quotient.mk
        ((liftQSpanSingleton (p ^ k i)
              (LinearMap.toSpanSingleton R M
                (sorry.choose (p := fun (x : M) ↦
                  p ^ k i • x = 0 ∧
                    Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                      ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
                        ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
                      (((DirectSum.lof R (Fin d)
                                (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                              HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                                ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                            (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
                          1 :
                        ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)))))
              sorry :
            (a : R ⧸ R ∙ p ^ k i) → M)
          (Submodule.Quotient.mk 1))) :
    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
  (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
        (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
      (Submodule.Quotient.mk 1) :
    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
Tactic: rw [LinearEquiv.coe_toLinearMap, LinearMap.id_apply, DirectSum.toModule_lof,
            liftQSpanSingleton_apply, LinearMap.toSpanSingleton_apply_one, Ideal.Quotient.mk_eq_mk,
            map_one (Ideal.Quotient.mk _), (this i).choose_spec.right]