awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ ∃ (k : Fin (d + 1) → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))

Tactic:
⟨?_, ⟨?_⟩⟩

Premises used: Nonempty.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h : Fin (d + 1) → ℕ
h₁ :
  M ≃ₗ[R]
    ⨁ (i : Fin (d + 1)),
      HasQuotient.Quotient R (B := Submodule R R)
        (R ∙
          HPow.hPow (β := ℕ) p
            ((fun (i : Option (Fin d)) ↦
                (Option.rec (motive := fun (x : Option (Fin d)) ↦ ℕ) (pOrder hM (s j)) k i : ℕ))
              ((finSuccEquiv d : (a : Fin (d + 1)) → Option (Fin d)) i)))
⊢ ∃ (k : Fin (d + 1) → ℕ),
    Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))

Tactic:
refine ⟨?_, ⟨?_⟩⟩
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
⊢ Fin (d + 1) → ℕ

Tactic:
exact fun a => (fun i => (Option.rec (pOrder hM (s j)) k i : ℕ)) (finSuccEquiv d a)

Premises used: Option.rec, finSuccEquiv, DFunLike.coe
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this_1 : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f :
  LinearEquiv.{u, u, v, u} (RingHom.id R) (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
this :
  ∀ (i : Fin d),
    ∃ (x : M),
      p ^ k i • x = 0 ∧
        Eq.{u + 1} (α := ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          ((f : (a : M ⧸ R ∙ s j) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) (Submodule.Quotient.mk x) :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
          (((DirectSum.lof R (Fin d) (fun (i : Fin d) ↦ HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) i :
                  HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i) →ₗ[R]
                    ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i)) :
                (a : R ⧸ R ∙ p ^ k i) → ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
              1 :
            ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
h : R ∙ s j = ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker
h₁ :
  Eq (α := Submodule R M) (R ∙ s j)
    (LinearMap.ker (M₂ := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (mkQ (R ∙ s j)))
h₂ h₃ : Eq (α := Submodule R M) (R ∙ s j) (R ∙ s j)
⊢ LinearMap.range (M := ↥(R ∙ s j)) (Submodule.subtype (R ∙ s j)) =
    ((↑f : M ⧸ R ∙ s j →ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i) ∘ₗ mkQ (R ∙ s j)).ker

Tactic:
rw [range_subtype, LinearEquiv.ker_comp, ker_mkQ]

Premises used: LinearEquiv.ker_comp, Submodule.ker_mkQ, Submodule.range_subtype
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
x : M
rw :
  Eq (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
    (Submodule.Quotient.mk (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯ • x)) 0
rw₁ : Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) (Submodule.Quotient.mk 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) 0 0
⊢ HSMul.hSMul (β := HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))
      (Exists.choose (p := fun (a : ↥(Submonoid.powers p)) ↦ a • x = 0) ⋯) (Submodule.Quotient.mk x) =
    0

Tactic:
rw [← Quotient.mk_smul, (@hM x).choose_spec, Quotient.mk_zero]

Premises used: Exists.choose_spec, Submodule.Quotient.mk_smul, Submodule.Quotient.mk_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ IsTorsion'.{v, u} (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)) ↥(Submonoid.powers p)

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

Premises used: Iff.mpr, Function.Surjective.forall, Submodule.Quotient.mk_surjective
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.map (mkQ (R ∙ s j)) (Submodule.span R (Set.range s))) (Submodule.map (mkQ (R ∙ s j)) ⊤)

Tactic:
have hs' := congr_arg (Submodule.map <| mkQ <| R ∙ s j) hs
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.map (mkQ (R ∙ s j)) (Submodule.span R (Set.range s))) (Submodule.map (mkQ (R ∙ s j)) ⊤)
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((⇑(mkQ (R ∙ s j)) : (a : M) → M ⧸ R ∙ s j) '' Set.range s)) ⊤

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

Premises used: Submodule.map_top, Submodule.range_mkQ, Submodule.map_span
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((⇑(mkQ (R ∙ s j)) : (a : M) → M ⧸ R ∙ s j) '' Set.range s)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤

Tactic:
simp only [mkQ_apply] at hs'

Premises used: Submodule.mkQ_apply
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤
h :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Set.range (Submodule.Quotient.mk ∘ s ∘ j.succAbove))) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j))) (Submodule.span R (Set.range s')) ⊤

Tactic:
simp only [s']
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤
h :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Set.range (Submodule.Quotient.mk ∘ s ∘ j.succAbove))) ⊤

Tactic:
rw [← Function.comp_assoc, Set.range_comp (_ ∘ s), Fin.range_succAbove]

Premises used: Set.range_comp, Function.comp, Fin.range_succAbove, Function.comp_assoc
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) '' Set.range s)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ)) ⊤

Tactic:
rw [← Set.range_comp, ← Set.insert_image_compl_eq_range _ j, Function.comp_apply,
        (Quotient.mk_eq_zero _).mpr (Submodule.mem_span_singleton_self _),
        Submodule.span_insert_zero] at hs'

Premises used: Iff.mpr, Set.range_comp, Submodule.mem_span_singleton_self, Function.comp_apply, Set.insert_image_compl_eq_range, Submodule.Quotient.mk_eq_zero, Submodule.span_insert_zero
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ)) ⊤

Tactic:
hs'

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Module.PID
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst_5 : AddCommGroup M] [inst_6 : Module R M] (hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p))
    (s : Fin d → M) (hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤),
    ∃ (k : Fin d → ℕ), Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p ^ k i))
M : Type v
inst_3 : AddCommGroup M
inst_4 : Module R M
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Eq (α := Submodule R M) (Submodule.span R (Set.range s)) ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j) := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' :
  Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R ((fun (a : M) ↦ Submodule.Quotient.mk a) ∘ s '' {j}ᶜ)) ⊤
⊢ Eq (α := Submodule R (HasQuotient.Quotient M (B := Submodule R M) (R ∙ s j)))
    (Submodule.span R (Submodule.Quotient.mk ∘ s '' {j}ᶜ)) ⊤

Tactic:
exact hs'
-- 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
obtain :
  ∀ (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)),
    ∃ (ι : 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))
⊢ ∃ (ι : 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:
obtain ⟨I, fI, _, p, hp, e, h⟩ := Submodule.exists_isInternal_prime_power_torsion_of_pid hM

Premises used: Submodule.exists_isInternal_prime_power_torsion_of_pid
-- 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)
⊢ ∀ (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)))

Tactic:
fun i =>
      torsion_by_prime_power_decomposition.{u, v} (hp i)
        ((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)

Premises used: Iff.mpr, Submodule.isTorsion'_powers_iff, HPow.hPow, Exists.intro, Submodule.smul_torsionBy, Module.torsion_by_prime_power_decomposition
-- 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)
⊢ ∀ (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)))

Tactic:
exact fun i =>
      torsion_by_prime_power_decomposition.{u, v} (hp i)
        ((isTorsion'_powers_iff <| p i).mpr fun x => ⟨e i, smul_torsionBy _ _⟩)