-- 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 : Fin d → ℕ),
      Nonempty
        (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
          (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))
i :
  (x : I) ×
    Fin
      (⋯.choose (p := fun (d : ℕ) ↦
        ∃ (k : Fin d → ℕ),
          Nonempty
            (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
              (⨁ (j : 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) ↦
            Fin
              (⋯.choose (p := fun (d : ℕ) ↦
                ∃ (k : Fin d → ℕ),
                  Nonempty
                    (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                      (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))
        (Exists.choose (p :=
            fun
              (k :
                Fin
                    (Exists.choose (p := fun (d : ℕ) ↦
                      ∃ (k : Fin d → ℕ),
                        Nonempty
                          (LinearEquiv.{u, u, v, u} (RingHom.id R)
                            (↥(torsionBy R M
                                (p
                                    (i.fst (β := fun (x : I) ↦
                                      Fin
                                        (⋯.choose (p := fun (d : ℕ) ↦
                                          ∃ (k : Fin d → ℕ),
                                            Nonempty
                                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                (⨁ (j : Fin d),
                                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                                  e
                                    (i.fst (β := fun (x : I) ↦
                                      Fin
                                        (⋯.choose (p := fun (d : ℕ) ↦
                                          ∃ (k : Fin d → ℕ),
                                            Nonempty
                                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                (⨁ (j : Fin d),
                                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                            (⨁ (j : Fin d),
                              HasQuotient.Quotient R (B := Submodule R R)
                                (R ∙
                                  p
                                      (i.fst (β := fun (x : I) ↦
                                        Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : 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) ↦
                          Fin
                            (⋯.choose (p := fun (d : ℕ) ↦
                              ∃ (k : Fin d → ℕ),
                                Nonempty
                                  (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                    (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                      e
                        (i.fst (β := fun (x : I) ↦
                          Fin
                            (⋯.choose (p := fun (d : ℕ) ↦
                              ∃ (k : Fin d → ℕ),
                                Nonempty
                                  (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                    (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                (⨁ (j :
                  Fin
                    (Exists.choose (p := fun (d : ℕ) ↦
                      ∃ (k : Fin d → ℕ),
                        Nonempty
                          (LinearEquiv.{u, u, v, u} (RingHom.id R)
                            (↥(torsionBy R M
                                (p
                                    (i.fst (β := fun (x : I) ↦
                                      Fin
                                        (⋯.choose (p := fun (d : ℕ) ↦
                                          ∃ (k : Fin d → ℕ),
                                            Nonempty
                                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                (⨁ (j : Fin d),
                                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                                  e
                                    (i.fst (β := fun (x : I) ↦
                                      Fin
                                        (⋯.choose (p := fun (d : ℕ) ↦
                                          ∃ (k : Fin d → ℕ),
                                            Nonempty
                                              (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                (⨁ (j : Fin d),
                                                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))))))
                            (⨁ (j : Fin d),
                              HasQuotient.Quotient R (B := Submodule R R)
                                (R ∙
                                  p
                                      (i.fst (β := fun (x : I) ↦
                                        Fin
                                          (⋯.choose (p := fun (d : ℕ) ↦
                                            ∃ (k : Fin d → ℕ),
                                              Nonempty
                                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                                  (⨁ (j : 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) ↦
                            Fin
                              (⋯.choose (p := fun (d : ℕ) ↦
                                ∃ (k : Fin d → ℕ),
                                  Nonempty
                                    (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                                      (⨁ (j : Fin d),
                                        HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) ^
                        k j))))
            ⋯
            (i.snd (β := fun (x : I) ↦
              Fin
                (⋯.choose (p := fun (d : ℕ) ↦
                  ∃ (k : Fin d → ℕ),
                    Nonempty
                      (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p x ^ e x)))
                        (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p x ^ k j))))))) :
          ℕ))
    (R ∙
      HPow.hPow (α := R) (β := ℕ)
        ((fun
              (x :
                (i : I) ×
                  Fin
                    (⋯.choose (p := fun (d : ℕ) ↦
                      ∃ (k : Fin d → ℕ),
                        Nonempty
                          (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                            (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))))) ↦
            (match (motive :=
                (i : I) ×
                    Fin
                      (⋯.choose (p := fun (d : ℕ) ↦
                        ∃ (k : Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                              (⨁ (j : 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) ×
                  Fin
                    (⋯.choose (p := fun (d : ℕ) ↦
                      ∃ (k : Fin d → ℕ),
                        Nonempty
                          (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                            (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j)))))) ↦
            (match (motive :=
                (i : I) ×
                    Fin
                      (⋯.choose (p := fun (d : ℕ) ↦
                        ∃ (k : Fin d → ℕ),
                          Nonempty
                            (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                              (⨁ (j : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ k j))))) →
                  ℕ)
                x with
              | ⟨i, j⟩ =>
                ⋯.choose (p :=
                  fun
                    (k :
                      Fin
                          (⋯.choose (p := fun (d : ℕ) ↦
                            ∃ (k : Fin d → ℕ),
                              Nonempty
                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                  (⨁ (j : 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 :
                        Fin
                          (⋯.choose (p := fun (d : ℕ) ↦
                            ∃ (k : Fin d → ℕ),
                              Nonempty
                                (LinearEquiv.{u, u, v, u} (RingHom.id R) (↥(torsionBy R M (p i ^ e i)))
                                  (⨁ (j : 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))

Tactic:
simp only