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

Proof state:
case intro.intro.intro.intro.intro.intro.mk.ofRepr.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
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
f : N ⧸ torsion R N →ₗ[R] N
hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
refine
  ⟨n, I, fI, p, hp, e,
    ⟨(lequivProdOfRightSplitExact (torsion R N).injective_subtype ?_ hf).symm.trans <|
        (h.prod g).trans <| LinearEquiv.prodComm.{u, u} R _ (Fin n →₀ R) ⟩⟩

Result:
case intro.intro.intro.intro.intro.intro.mk.ofRepr.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
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
f : N ⧸ torsion R N →ₗ[R] N
hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id
⊢ LinearMap.range (torsion R N).subtype = LinearMap.ker (torsion R N).mkQ

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
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ :=
  equiv_directSum_of_isTorsion.{u, v} (@torsion_isTorsion R N _ _ _)

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
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Proof state:
case intro.intro.intro.intro.intro.intro.mk.ofRepr
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
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
haveI : Module.Projective R (N ⧸ torsion R N) := Module.Projective.of_basis ⟨g⟩

Result:
case intro.intro.intro.intro.intro.intro.mk.ofRepr
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
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span 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
this : IsNoetherian R ↥(torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
haveI := Module.Finite.of_surjective _ (torsion R N).mkQ_surjective

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
this✝ : IsNoetherian R ↥(torsion R N)
this : Module.Finite R (N ⧸ torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Proof state:
case intro.intro.intro.intro.intro.intro.mk.ofRepr.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
this✝¹ : IsNoetherian R ↥(torsion R N)
this✝ : Module.Finite R (N ⧸ torsion R N)
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R N) ≃ₗ[R] ⨁ (i : I), R ⧸ span R {p i ^ e i}
n : ℕ
g : (N ⧸ torsion R N) ≃ₗ[R] Fin n →₀ R
this : Projective R (N ⧸ torsion R N)
f : N ⧸ torsion R N →ₗ[R] N
hf : (torsion R N).mkQ ∘ₗ f = LinearMap.id
⊢ LinearMap.range (torsion R N).subtype = LinearMap.ker (torsion R N).mkQ

Tactic:
rw [range_subtype, ker_mkQ]

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
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})

Tactic:
haveI := isNoetherian_submodule' (torsion R N)

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
this : IsNoetherian R ↥(torsion R N)
⊢ ∃ n ι x p,
    ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ span R {p i ^ e i})