-- Mathlib/Algebra/Module/PID.lean
theorem Submodule.exists_isInternal_prime_power_torsion_of_pid [Module.Finite R M]
    (hM : Module.IsTorsion R M) :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i)
        (e : ι → ℕ), DirectSum.IsInternal fun i => torsionBy R M <| p i ^ e i

Proof state:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
this : p.IsPrime
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Tactic:
exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

Result:
no goals

Proof state:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Tactic:
have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)

Result:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Proof state:
case refine_1
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ Fintype { x // x ∈ (factors ⊤.annihilator).toFinset }

Tactic:
exact Finset.fintypeCoeSort _

Result:
no goals

Proof state:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Tactic:
haveI := Ideal.isPrime_of_prime hP

Result:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
this : p.IsPrime
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∃ ι x x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i => torsionBy R M (p i ^ e i)

Tactic:
refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩

Result:
case refine_1
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ Fintype { x // x ∈ (factors ⊤.annihilator).toFinset }

case refine_2
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∀ (i : { x // x ∈ (factors ⊤.annihilator).toFinset }), Irreducible (IsPrincipal.generator ↑i)

Proof state:
case refine_2
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∀ (i : { x // x ∈ (factors ⊤.annihilator).toFinset }), Irreducible (IsPrincipal.generator ↑i)

Tactic:
rintro ⟨p, hp⟩

Result:
case refine_2.mk
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)