-- 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:
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})

Tactic:
haveI := fI

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
⊢ ∃ ι 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.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⟩}

Tactic:
simp only

Result:
no goals

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
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), IsNoetherian R ↥(torsionBy R N (p i ^ e i))
⊢ ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})

Tactic:
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:
no goals

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
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
⊢ ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})

Tactic:
haveI := fun i => isNoetherian_submodule' (torsionBy R N <| p i ^ e i)

Result:
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), IsNoetherian R ↥(torsionBy R N (p i ^ e i))
⊢ ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})