-- Mathlib/Algebra/Module/PID.lean
theorem torsion_by_prime_power_decomposition (hN : Module.IsTorsion' N (Submonoid.powers p))
    [h' : Module.Finite R N] :
    ∃ (d : ℕ) (k : Fin d → ℕ), Nonempty <| N ≃ₗ[R] ⨁ i : Fin d, R ⧸ R ∙ p ^ (k i : ℕ)

Proof state:
case h.succ.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Tactic:
let s' : Fin d → N ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove

Result:
case h.succ.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ Submodule.span R {p ^ k i})

Proof state:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Submodule.map (Submodule.span R {s j}).mkQ (Submodule.span R (Set.range s)) =
    Submodule.map (Submodule.span R {s j}).mkQ ⊤
⊢ Submodule.span R (Set.range s') = ⊤

Tactic:
rw [Submodule.map_span, Submodule.map_top, range_mkQ] at hs'

Result:
case h.succ.intro.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R (⇑(Submodule.span R {s j}).mkQ '' Set.range s) = ⊤
⊢ Submodule.span R (Set.range s') = ⊤

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin 0 → N
hs : ⊥ = ⊤
this : Unique N
⊢ Nonempty (N ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ Submodule.span R {p ^ finZeroElim i})

Tactic:
haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin 0 → N
hs : ⊥ = ⊤
this✝ : Unique N
this : IsEmpty (Fin Nat.zero)
⊢ Nonempty (N ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ Submodule.span R {p ^ finZeroElim i})

Proof state:
case h.succ.intro.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N],
    IsTorsion' N ↥(Submonoid.powers p) →
      ∀ (s : Fin d → N),
        Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin (d + 1) → N
hs : Submodule.span R (Set.range s) = ⊤
this : (x : N) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R N (p ^ pOrder hN (s j))
s' : Fin d → N ⧸ Submodule.span R {s j} := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ IsTorsion' (N ⧸ Submodule.span R {s j}) ↥(Submonoid.powers p)

Tactic:
exact (mk_surjective _).forall.mpr fun x =>
  ⟨(@hN x).choose, by rw [← Quotient.mk_smul, (@hN x).choose_spec, Quotient.mk_zero]⟩

Result:
no goals

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin 0 → N
hs : ⊥ = ⊤
⊢ Nonempty (N ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ Submodule.span R {p ^ finZeroElim i})

Tactic:
haveI : Unique N :=
  ⟨⟨0⟩, fun x => by dsimp; rw [← Submodule.mem_bot R, hs]; exact Submodule.mem_top⟩

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
N : Type (max u v)
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hN : IsTorsion' N ↥(Submonoid.powers p)
s : Fin 0 → N
hs : ⊥ = ⊤
this : Unique N
⊢ Nonempty (N ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ Submodule.span R {p ^ finZeroElim i})

Proof state:
case 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
p : R
hp : Irreducible p
hN : IsTorsion' N ↥(Submonoid.powers p)
h' : Module.Finite R N
d : ℕ
s : Fin d → N
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ d k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})

Tactic:
use d

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
p : R
hp : Irreducible p
hN : IsTorsion' N ↥(Submonoid.powers p)
h' : Module.Finite R N
d : ℕ
s : Fin d → N
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})

Proof state:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
p : R
hp : Irreducible p
hN : IsTorsion' N ↥(Submonoid.powers p)
h' : Module.Finite R N
d : ℕ
s : Fin d → N
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})

Tactic:
clear h'

Result:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
N : Type (max u v)
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsDomain R
p : R
hp : Irreducible p
hN : IsTorsion' N ↥(Submonoid.powers p)
d : ℕ
s : Fin d → N
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})