-- Mathlib/Algebra/Module/PID.lean
theorem equiv_directSum_of_isTorsion [h' : Module.Finite R N] (hN : Module.IsTorsion R N) :
    ∃ (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
      Nonempty <| N ≃ₗ[R] ⨁ i : ι, R ⧸ R ∙ p i ^ e i

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
obtain ⟨I, fI, _, p, hp, e, h⟩ := Submodule.exists_isInternal_prime_power_torsion_of_pid hN

Result:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
i : (x : I) × Fin ⋯.choose
⊢ span R {p i.fst ^ ⋯.choose i.snd} =
    span R
      {(fun x =>
              match x with
              | ⟨i, snd⟩ => p i)
            i ^
          (fun x =>
              match x with
              | ⟨i, j⟩ => ⋯.choose j)
            i}

Tactic:
obtain ⟨i, j⟩ := i

Result:
case intro.intro.intro.intro.intro.intro.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
i : I
j : Fin ⋯.choose
⊢ span R {p ⟨i, j⟩.fst ^ ⋯.choose ⟨i, j⟩.snd} =
    span R
      {(fun x =>
              match x with
              | ⟨i, snd⟩ => p i)
            ⟨i, j⟩ ^
          (fun x =>
              match x with
              | ⟨i, j⟩ => ⋯.choose j)
            ⟨i, j⟩}

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
classical
refine
  ⟨Σ i, Fin (this i).choose, inferInstance, fun ⟨i, _⟩ => p i, fun ⟨i, _⟩ => hp i, fun ⟨i, j⟩ =>
    (this i).choose_spec.choose j,
    ⟨(LinearEquiv.ofBijective (DirectSum.coeLinearMap _) h).symm.trans <|
        (DFinsupp.mapRange.linearEquiv fun i => (this i).choose_spec.choose_spec.some).trans <|
          (DirectSum.sigmaLcurryEquiv R).symm.trans
            (DFinsupp.mapRange.linearEquiv fun i => quotEquivOfEq _ _ ?_)⟩⟩
obtain ⟨i, j⟩ := i
simp only

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this : Fintype I
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
have :
  ∀ i,
    ∃ (d : ℕ) (k : Fin d → ℕ),
      Nonempty <| torsionBy R N (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ p i ^ k j := by
  haveI := fun i => isNoetherian_submodule' (torsionBy R N <| p i ^ e i)
  exact fun i =>
    torsion_by_prime_power_decomposition.{u, v} (hp i)
      ((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)

Result:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
refine
  ⟨Σ i, Fin (this i).choose, inferInstance, fun ⟨i, _⟩ => p i, fun ⟨i, _⟩ => hp i, fun ⟨i, j⟩ =>
    (this i).choose_spec.choose j,
    ⟨(LinearEquiv.ofBijective (DirectSum.coeLinearMap _) h).symm.trans <|
        (DFinsupp.mapRange.linearEquiv fun i => (this i).choose_spec.choose_spec.some).trans <|
          (DirectSum.sigmaLcurryEquiv R).symm.trans
            (DFinsupp.mapRange.linearEquiv fun i => quotEquivOfEq _ _ ?_)⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
h' : Module.Finite R N
hN : IsTorsion R N
I : Type u
fI : Fintype I
w✝ : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)
this✝ : Fintype I
this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})
i : (x : I) × Fin ⋯.choose
⊢ span R {p i.fst ^ ⋯.choose i.snd} =
    span R
      {(fun x =>
              match x with
              | ⟨i, snd⟩ => p i)
            i ^
          (fun x =>
              match x with
              | ⟨i, j⟩ => ⋯.choose j)
            i}