-- 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
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)
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Tactic:
obtain ⟨j, hj⟩ := exists_isTorsionBy hN d.succ d.succ_ne_zero s hs

Result:
case h.succ.intro
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))
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Proof state:
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
x : N
⊢ ⋯.choose • Submodule.Quotient.mk x = 0

Tactic:
rw [← Quotient.mk_smul, (@hN x).choose_spec, Quotient.mk_zero]

Result:
no goals

Proof state:
case 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}
i : Fin d
fi : R ⧸ Submodule.span R {p ^ k i} →ₗ[R] N ⧸ Submodule.span R {s j} :=
  ↑f.symm ∘ₗ DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i
x : N
h0 : p ^ k i • x = 0
h1 : Submodule.Quotient.mk x = fi 1
⊢ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i) 1

Tactic:
rw [h1]

Result:
case 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}
i : Fin d
fi : R ⧸ Submodule.span R {p ^ k i} →ₗ[R] N ⧸ Submodule.span R {s j} :=
  ↑f.symm ∘ₗ DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i
x : N
h0 : p ^ k i • x = 0
h1 : Submodule.Quotient.mk x = fi 1
⊢ f (fi 1) = (DirectSum.lof R (Fin d) (fun i => R ⧸ Submodule.span R {p ^ k i}) i) 1

Proof state:
case h.succ.intro.refine_3.intro.intro.refine_2.refine_2
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
⊢ ((↑f ∘ₗ (Submodule.span R {s j}).mkQ) ∘ₗ
        DirectSum.toModule R (Fin d) N fun i =>
          liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R N ⋯.choose) ⋯) ∘ₗ
      ↑ULift.moduleEquiv =
    ↑ULift.moduleEquiv

Tactic:
suffices (f.toLinearMap.comp (R ∙ s j).mkQ).comp _ = LinearMap.id by
  rw [this, LinearMap.id_comp]

Result:
case h.succ.intro.refine_3.intro.intro.refine_2.refine_2
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
⊢ ((↑f ∘ₗ (Submodule.span R {s j}).mkQ) ∘ₗ
      DirectSum.toModule R (Fin d) N fun i => liftQSpanSingleton (p ^ k i) (LinearMap.toSpanSingleton R N ⋯.choose) ⋯) =
    LinearMap.id