-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
h' : Module.Finite R M
hM : IsTorsion R M
I : Type u
fI : Fintype I
w : DecidableEq I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : DirectSum.IsInternal (S := Submodule R M) fun (i : I) ↦ torsionBy R M (p i ^ e i)
this :
  ∀ (i : I),
    ∃ (d : ℕ) (k : _root_.Fin d → ℕ),
      Nonempty
        (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
          (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))
Fin :
  ∀
    (i :
      (x : I) ×
        _root_.Fin
          (⋯.choose (p := fun (d : ℕ) ↦
            ∃ (k : _root_.Fin d → ℕ),
              Nonempty
                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                  (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j)))))),
    Eq (α := Submodule R R)
      (R ∙
        HPow.hPow (β := ℕ)
          (p
            (i.fst (β := fun (x : I) ↦
              _root_.Fin
                (⋯.choose (p := fun (d : ℕ) ↦
                  ∃ (k : _root_.Fin d → ℕ),
                    Nonempty
                      (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                        (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))
          (Exists.choose (p :=
              fun
                (k :
                  _root_.Fin
                      (Exists.choose (p := fun (d : ℕ) ↦
                        ∃ (k : _root_.Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R)
                              (↥(torsionBy R M
                                  (p
                                      (i.fst (β := fun (x : I) ↦
                                        _root_.Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : _root_.Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : _root_.Fin d),
                                                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                                    e
                                      (i.fst (β := fun (x : I) ↦
                                        _root_.Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : _root_.Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : _root_.Fin d),
                                                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                              (⨁ (j : _root_.Fin d),
                                HasQuotient.Quotient R (B := Submodule R R)
                                  (R ∙
                                    p
                                        (i.fst (β := fun (x : I) ↦
                                          _root_.Fin
                                            (⋯.choose (p := fun (d : ℕ) ↦
                                              ∃ (k : _root_.Fin d → ℕ),
                                                Nonempty
                                                  (LinearEquiv.{u, u, v, u} (RingHom.id R)
                                                    (↥(torsionBy R M (p x ^ e x)))
                                                    (⨁ (j : _root_.Fin d),
                                                      HasQuotient.Quotient R (B := Submodule R R)
                                                        (R ∙ p x ^ k j))))))) ^
                                      k j))))
                        ⋯) →
                    ℕ) ↦
              Nonempty
                (LinearEquiv.{u, u, v, u} (RingHom.id R)
                  (↥(torsionBy R M
                      (p
                          (i.fst (β := fun (x : I) ↦
                            _root_.Fin
                              (⋯.choose (p := fun (d : ℕ) ↦
                                ∃ (k : _root_.Fin d → ℕ),
                                  Nonempty
                                    (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                      (⨁ (j : _root_.Fin d),
                                        HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                        e
                          (i.fst (β := fun (x : I) ↦
                            _root_.Fin
                              (⋯.choose (p := fun (d : ℕ) ↦
                                ∃ (k : _root_.Fin d → ℕ),
                                  Nonempty
                                    (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                      (⨁ (j : _root_.Fin d),
                                        HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                  (⨁ (j :
                    _root_.Fin
                      (Exists.choose (p := fun (d : ℕ) ↦
                        ∃ (k : _root_.Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R)
                              (↥(torsionBy R M
                                  (p
                                      (i.fst (β := fun (x : I) ↦
                                        _root_.Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : _root_.Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : _root_.Fin d),
                                                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                                    e
                                      (i.fst (β := fun (x : I) ↦
                                        _root_.Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : _root_.Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : _root_.Fin d),
                                                    HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                              (⨁ (j : _root_.Fin d),
                                HasQuotient.Quotient R (B := Submodule R R)
                                  (R ∙
                                    p
                                        (i.fst (β := fun (x : I) ↦
                                          _root_.Fin
                                            (⋯.choose (p := fun (d : ℕ) ↦
                                              ∃ (k : _root_.Fin d → ℕ),
                                                Nonempty
                                                  (LinearEquiv.{u, u, v, u} (RingHom.id R)
                                                    (↥(torsionBy R M (p x ^ e x)))
                                                    (⨁ (j : _root_.Fin d),
                                                      HasQuotient.Quotient R (B := Submodule R R)
                                                        (R ∙ p x ^ k j))))))) ^
                                      k j))))
                        ⋯)),
                    HasQuotient.Quotient R (B := Submodule R R)
                      (R ∙
                        p
                            (i.fst (β := fun (x : I) ↦
                              _root_.Fin
                                (⋯.choose (p := fun (d : ℕ) ↦
                                  ∃ (k : _root_.Fin d → ℕ),
                                    Nonempty
                                      (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                        (⨁ (j : _root_.Fin d),
                                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                          k j))))
              ⋯
              (i.snd (β := fun (x : I) ↦
                _root_.Fin
                  (⋯.choose (p := fun (d : ℕ) ↦
                    ∃ (k : _root_.Fin d → ℕ),
                      Nonempty
                        (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                          (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) :
            ℕ))
      (R ∙
        HPow.hPow (α := R) (β := ℕ)
          ((fun
                (x :
                  (i : I) ×
                    _root_.Fin
                      (⋯.choose (p := fun (d : ℕ) ↦
                        ∃ (k : _root_.Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                              (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))))) ↦
              (match (motive :=
                  (i : I) ×
                      _root_.Fin
                        (⋯.choose (p := fun (d : ℕ) ↦
                          ∃ (k : _root_.Fin d → ℕ),
                            Nonempty
                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j))))) →
                    R)
                  x with
                | ⟨i, snd⟩ => p i :
                R))
            i)
          ((fun
                (x :
                  (i : I) ×
                    _root_.Fin
                      (⋯.choose (p := fun (d : ℕ) ↦
                        ∃ (k : _root_.Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                              (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))))) ↦
              (match (motive :=
                  (i : I) ×
                      _root_.Fin
                        (⋯.choose (p := fun (d : ℕ) ↦
                          ∃ (k : _root_.Fin d → ℕ),
                            Nonempty
                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                (⨁ (j : _root_.Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j))))) →
                    ℕ)
                  x with
                | ⟨i, j⟩ =>
                  ⋯.choose (p :=
                    fun
                      (k :
                        _root_.Fin
                            (⋯.choose (p := fun (d : ℕ) ↦
                              ∃ (k : _root_.Fin d → ℕ),
                                Nonempty
                                  (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                    (⨁ (j : _root_.Fin d),
                                      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j))))) →
                          ℕ) ↦
                    Nonempty
                      (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                        (⨁ (j :
                          _root_.Fin
                            (⋯.choose (p := fun (d : ℕ) ↦
                              ∃ (k : _root_.Fin d → ℕ),
                                Nonempty
                                  (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                    (⨁ (j : _root_.Fin d),
                                      HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))))),
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j))))
                    j :
                ℕ))
            i))
⊢ ∃ (ι : Type u) (x : Fintype ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (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 _ _ ?_)⟩⟩
  simp only