-- Mathlib/Algebra/Module/PID.lean
theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoid.powers p))
    [h' : Module.Finite R N] :
    ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty <| N ≃ₗ[R] ⨁ i : Fin d, R ⧸ R ∙ p ^ (k i : ℕ)

Proof state:
case h.succ.intro.refine_3.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (N ⧸ Submodule.span R {s j}) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i}
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Tactic:
have : ∀ i : Fin d,
    ∃ x : N, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = DirectSum.lof R _ _ i 1 := by
  intro i
  let fi := f.symm.toLinearMap.comp (DirectSum.lof _ _ _ i)
  obtain ⟨x, h0, h1⟩ := exists_smul_eq_zero_and_mk_eq hp hN hj fi; refine ⟨x, h0, ?_⟩; rw [h1]
  simp only [fi, LinearMap.coe_comp, f.symm.coe_toLinearMap, f.apply_symm_apply,
    Function.comp_apply]

Result:
case h.succ.intro.refine_3.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (N ⧸ Submodule.span R {s j}) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i}
this :
  ∀ (i : Fin d),
    ∃ x,
      p ^ k i • x = 0 ∧
        f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i) 1
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Proof state:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R (⇑(Submodule.span R {s j}).mkQ '' Set.range s) = ⊤
⊢ Submodule.span R (Set.range s') = ⊤

Tactic:
simp only [mkQ_apply] at hs'

Result:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R ((fun a => Submodule.Quotient.mk a) '' Set.range s) = ⊤
⊢ Submodule.span R (Set.range s') = ⊤

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (N ⧸ Submodule.span R {s j}) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i}
⊢ ∀ (i : Fin d),
    ∃ x,
      p ^ k i • x = 0 ∧
        f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i) 1

Tactic:
intro i

Result:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (N ⧸ Submodule.span R {s j}) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i}
i : Fin d
⊢ ∃ x,
    p ^ k i • x = 0 ∧
      f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i) 1

Proof state:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R ((fun a => Submodule.Quotient.mk a) '' Set.range s) = ⊤
⊢ Submodule.span R (Set.range (Submodule.Quotient.mk ∘ s ∘ j.succAbove)) = ⊤

Tactic:
rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove]

Result:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R ((fun a => Submodule.Quotient.mk a) '' Set.range s) = ⊤
⊢ Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ) = ⊤