awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
b : M
zero : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑0 : R) b = HSMul.hSMul (α := ℕ) 0 b
succ :
  ∀ (n : ℕ) (ih : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b),
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(n + 1) : R) b = (n + 1) • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b

Tactic:
induction n with
  | zero => rw [Nat.cast_zero, zero_smul, zero_smul]
  | succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

Premises used: Nat.cast_succ, one_smul, zero_smul, add_smul, Nat.zero, Nat.cast_zero, Nat.succ
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
inst_3 : n.AtLeastTwo
b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (OfNat.ofNat n) b = HSMul.hSMul (α := ℕ) (OfNat.ofNat n) b

Tactic:
Nat.cast_smul_eq_nsmul ..

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
inst : AddCommMonoid M
h : Module ℕ M
n : ℕ
x : M
⊢ SMul.smul n x = n • x

Tactic:
Nat.cast_smul_eq_nsmul ..

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Module ℕ M
n : ℕ
⊢ ∀ (x : M), SMul.smul n x = n • x

Tactic:
nat_smul_eq_nsmul P n

Premises used: nat_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : Module ℕ M
n : ℕ
⊢ ∀ (m : M), n • m = n • m

Tactic:
convert! nat_smul_eq_nsmul P n

Premises used: nat_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Subsingleton.{max (u_3 + 1) 1} (Module ℕ M)

Tactic:
AddCommMonoid.uniqueNatModule.instSubsingleton

Premises used: Unique.instSubsingleton
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
y : M
⊢ HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)

Tactic:
simp only [zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : R
y : M
n : ℕ
ih : (n • x) • y = n • x • y
⊢ ((n + 1) • x) • y = (n + 1) • x • y

Tactic:
simp only [add_smul, one_smul, ih]

Premises used: one_smul, add_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
x : R
y : M
zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
succ : ∀ (n : ℕ) (ih : (n • x) • y = n • x • y), ((n + 1) • x) • y = (n + 1) • x • y
⊢ (n • x) • y = n • x • y

Tactic:
induction n with
    | zero => simp only [zero_smul]
    | succ n ih => simp only [add_smul, one_smul, ih]

Premises used: one_smul, zero_smul, add_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : Semiring R
inst_5 : Semiring S
inst_6 : Module R M
inst_7 : Module S M₂
x : ℕ
a : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑x : R) a) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑x : S) ((f : (a : M) → M₂) a : M₂)

Tactic:
simp only [Nat.cast_smul_eq_nsmul, map_nsmul]

Premises used: Nat.cast_smul_eq_nsmul, map_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_5
inst : NonAssocSemiring R
m : ℕ
rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
rw₁ rw₂ : Eq.{u_5 + 1} (α := R) (↑m : R) (↑m : R)
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)

Tactic:
rw [nsmul_eq_mul, mul_one]

Premises used: nsmul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_5
inst : NonAssocRing R
m : ℤ
rw : HMul.hMul (α := R) (↑m : R) 1 = (↑m : R)
rw₁ rw₂ : Eq.{u_5 + 1} (α := R) (↑m : R) (↑m : R)
⊢ HSMul.hSMul (β := R) m 1 = (↑m : R)

Tactic:
rw [zsmul_eq_mul, mul_one]

Premises used: zsmul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
b : M
a : ℕ
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(ofNat a) : R) b = ofNat a • b

Tactic:
simp [Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
b : M
a : ℕ
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑-[a+1] : R) b = -[a+1] • b

Tactic:
simp [add_smul, Nat.cast_smul_eq_nsmul]

Premises used: add_smul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
b : M
ofNat : ∀ (a : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑(Int.ofNat a) : R) b = Int.ofNat a • b
negSucc : ∀ (a : ℕ), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑-[a+1] : R) b = -[a+1] • b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑n : R) b = n • b

Tactic:
cases n with
  | ofNat => simp [Nat.cast_smul_eq_nsmul]
  | negSucc => simp [add_smul, Nat.cast_smul_eq_nsmul]

Premises used: Int.ofNat, add_smul, Nat.cast_smul_eq_nsmul, Int.negSucc
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
inst : AddCommGroup M
h : Module ℤ M
n : ℤ
x : M
⊢ SMul.smul n x = n • x

Tactic:
Int.cast_smul_eq_zsmul ..

Premises used: Int.cast_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Module ℤ M
n : ℤ
⊢ ∀ (x : M), SMul.smul n x = n • x

Tactic:
int_smul_eq_zsmul P n

Premises used: int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Module ℤ M
n : ℤ
⊢ ∀ (m : M), n • m = n • m

Tactic:
convert! int_smul_eq_zsmul P n

Premises used: int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : Ring R
inst_5 : Ring S
inst_6 : Module R M
inst_7 : Module S M₂
x : ℤ
a : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑x : R) a) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑x : S) ((f : (a : M) → M₂) a : M₂)

Tactic:
simp only [Int.cast_smul_eq_zsmul, map_zsmul]

Premises used: Int.cast_smul_eq_zsmul, map_zsmul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R_1 : Type u_1
S : Type u_2
M_1 : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
y : M
a : ℕ
⊢ (Int.ofNat a • x) • y = Int.ofNat a • x • y

Tactic:
simp [mul_smul, Nat.cast_smul_eq_nsmul]

Premises used: Nat.cast_smul_eq_nsmul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R_1 : Type u_1
S : Type u_2
M_1 : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
y : M
a : ℕ
⊢ (Int.negSucc a • x) • y = Int.negSucc a • x • y

Tactic:
simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

Premises used: add_smul, Nat.cast_smul_eq_nsmul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R_1 : Type u_1
S : Type u_2
M_1 : Type u_3
M₂ : Type u_4
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℤ
x : R
y : M
ofNat : ∀ (a : ℕ), (Int.ofNat a • x) • y = Int.ofNat a • x • y
negSucc : ∀ (a : ℕ), (Int.negSucc a • x) • y = Int.negSucc a • x • y
⊢ (n • x) • y = n • x • y

Tactic:
cases n with
    | ofNat => simp [mul_smul, Nat.cast_smul_eq_nsmul]
    | negSucc => simp [mul_smul, add_smul, Nat.cast_smul_eq_nsmul]

Premises used: add_smul, Nat.cast_smul_eq_nsmul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
⊢ CharZero R

Tactic:
⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩

Premises used: CharZero.mk, Nat.cast_injective
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
refine : ∀ (m n : ℕ) (h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)), Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)
⊢ CharZero R

Tactic:
refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩
-- Module: Mathlib.Algebra.Module.NatInt
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoidWithOne M
inst_2 : CharZero M
inst_3 : Module R M
m n : ℕ
h : Eq.{u_1 + 1} (α := R) (↑m : R) (↑n : R)
rw : HSMul.hSMul (β := M) m 1 = (↑n : M)
rw₁ : HSMul.hSMul (β := M) m 1 = HSMul.hSMul (β := M) n 1
rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul (β := M) n 1
rw₃ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑m : R) 1 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1
rw₄ rw₅ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) (↑n : R) 1
⊢ Eq.{u_3 + 1} (α := M) (↑m : M) (↑n : M)

Tactic:
rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]

Premises used: Nat.cast_smul_eq_nsmul, nsmul_one
-- 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
a : R
h : Irreducible a
⊢ IsSemisimpleModule.{u, v} R ↥(torsionBy R M a)

Tactic:
haveI := PrincipalIdealRing.isMaximal_of_irreducible h
  letI := Ideal.Quotient.field (R ∙ a)
  (isSemisimpleModule_iff ..).mpr (submodule_torsionBy_orderIso a).complementedLattice

Premises used: Iff.mpr, Submodule.torsionBy, Membership.mem, OrderIso.complementedLattice, Subtype, isSemisimpleModule_iff, Submodule.submodule_torsionBy_orderIso
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBySet R M
      (↑((↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R)

Tactic:
isInternal_prime_power_torsion hM

Premises used: Submodule.isInternal_prime_power_torsion
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
h :
  ∀ (x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))),
    Eq (α := Submodule R M)
      (torsionBy R M
        (IsPrincipal.generator (↑x : Ideal R) ^
          Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
      (torsionBySet R M
        (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
⊢ DirectSum.IsInternal (S := Submodule R M) fun (p : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))) ↦
    torsionBy R M
      (IsPrincipal.generator (↑p : Ideal R) ^ Multiset.count (↑p : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤)))

Tactic:
convert! isInternal_prime_power_torsion hM

Premises used: Submodule.isInternal_prime_power_torsion
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
x : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
h :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(R ∙
            IsPrincipal.generator (↑x : Ideal R) ^
              Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₁ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(Ideal.span
            {IsPrincipal.generator (↑x : Ideal R) ^
                Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))}) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₂ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑(HPow.hPow (α := Ideal R) (Ideal.span {IsPrincipal.generator (↑x : Ideal R)})
            (Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤)))) :
        Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
h₃ h₄ :
  Eq (α := Submodule R M)
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))
⊢ Eq (α := Submodule R M)
    (torsionBy R M
      (IsPrincipal.generator (↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))))
    (torsionBySet R M
      (↑((↑x : Ideal R) ^ Multiset.count (↑x : Ideal R) (factors (annihilator.{u, v} (M := M) ⊤))) : Set R))

Tactic:
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.span_singleton_pow,
    Ideal.span_singleton_generator]

Premises used: Ideal.submodule_span_eq, Ideal.span_singleton_generator, Submodule.torsionBySet_span_singleton_eq, Ideal.span_singleton_pow
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∃ (ι : Type u) (x : Fintype ι) (x : DecidableEq ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (i : ι) ↦ torsionBy R M (p i ^ e i)

Tactic:
⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩

Premises used: Submodule.isInternal_prime_power_torsion_of_pid, Exists.intro
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
refine_1 : Fintype ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
refine_2 :
  ∀ (i : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))),
    Irreducible (IsPrincipal.generator (↑i : Ideal R))
⊢ ∃ (ι : Type u) (x : Fintype ι) (x : DecidableEq ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (i : ι) ↦ torsionBy R M (p i ^ e i)

Tactic:
refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
⊢ Fintype ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))

Tactic:
exact Finset.fintypeCoeSort _

Premises used: Finset.fintypeCoeSort
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) p
⊢ Prime p

Tactic:
have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) p
hP : Prime p
⊢ p.IsPrime

Tactic:
haveI := Ideal.isPrime_of_prime hP
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) p
hP : Prime p
this : p.IsPrime
⊢ Irreducible
    (IsPrincipal.generator
      (↑(Subtype.mk (p := fun (x : Ideal R) ↦
            Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) x) p
            hp) :
        Ideal R))

Tactic:
(IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

Premises used: Prime.irreducible, Submodule.IsPrincipal.prime_generator_of_isPrime, Prime.ne_zero
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) p
hP : Prime p
this : p.IsPrime
⊢ Irreducible
    (IsPrincipal.generator
      (↑(Subtype.mk (p := fun (x : Ideal R) ↦
            Membership.mem (γ := Finset (Ideal R)) (Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤))) x) p
            hp) :
        Ideal R))

Tactic:
exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

Premises used: Prime.irreducible, Submodule.IsPrincipal.prime_generator_of_isPrime, Prime.ne_zero
-- 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
inst_5 : Module.Finite R M
hM : Module.IsTorsion R M
refine_1 : Fintype ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))
refine_2 refine_2₁ :
  ∀ (i : ↥(Multiset.toFinset (factors (annihilator.{u, v} (M := M) ⊤)))),
    Irreducible (IsPrincipal.generator (↑i : Ideal R))
⊢ ∃ (ι : Type u) (x : Fintype ι) (x : DecidableEq ι) (p : ι → R) (_ : ∀ (i : ι), Irreducible (p i)) (e : ι → ℕ),
    DirectSum.IsInternal (S := Submodule R M) fun (i : ι) ↦ torsionBy R M (p i ^ e i)

Tactic:
classical
  refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
  · exact Finset.fintypeCoeSort _
  · rintro ⟨p, hp⟩
    have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
    haveI := Ideal.isPrime_of_prime hP
    exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

Premises used: Finset.fintypeCoeSort
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
dsimp : Eq (α := Ideal R) (torsionOf R M x) (Ideal.span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯})
⊢ Eq (α := Ideal R) (torsionOf R M x) (Ideal.span {p ^ pOrder hM x})

Tactic:
dsimp only [pOrder]

Premises used: Submodule.pOrder
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
rw :
  Associates.mk (generator (torsionOf R M x)) =
    HPow.hPow (α := Associates R) (Associates.mk p) (Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯)
⊢ Eq (α := Ideal R) (torsionOf R M x) (Ideal.span {p ^ Nat.find (p := fun (n : ℕ) ↦ p ^ n • x = 0) ⋯})

Tactic:
rw [← (torsionOf R M x).span_singleton_generator, Ideal.span_singleton_eq_span_singleton, ←
    Associates.mk_eq_mk_iff_associated, Associates.mk_pow]

Premises used: Associates.mk_eq_mk_iff_associated, Ideal.span_singleton_eq_span_singleton, Ideal.span_singleton_generator, Associates.mk_pow, Ideal.torsionOf
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
h :
  ∀ (n : ℕ),
    p ^ n • x = 0 ↔ Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
⊢ Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n

Tactic:
ext n
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
n : ℕ
h : p ^ n • x = 0 ↔ Membership.mem (γ := Ideal R) (torsionOf R M x) (p ^ n)
⊢ p ^ n • x = 0 ↔ Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n

Tactic:
rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]

Premises used: Associates.mk_pow, Associates.mk_dvd_mk, Submodule.IsPrincipal.mem_iff_generator_dvd
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
n : ℕ
⊢ p ^ n • x = 0 ↔ Membership.mem (γ := Ideal R) (torsionOf R M x) (p ^ n)

Tactic:
rfl
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
⊢ Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n

Tactic:
have prop :
    (fun n : ℕ => p ^ n • x = 0) = fun n : ℕ =>
      (Associates.mk <| generator <| torsionOf R M x) ∣ Associates.mk p ^ n := by
    ext n; rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]; rfl
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
prop :
  Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
⊢ ∃ (n : ℕ), p ^ n • x = 0

Tactic:
have := (isTorsion'_powers_iff p).mp hM x
-- 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
p : R
hp : Irreducible p
hM : IsTorsion'.{v, u} M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
prop :
  Eq (α := (n : ℕ) → Prop) (fun (n : ℕ) ↦ p ^ n • x = 0) fun (n : ℕ) ↦
    Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n
this : ∃ (n : ℕ), p ^ n • x = 0
⊢ ∃ (n : ℕ), Associates.mk (generator (torsionOf R M x)) ∣ HPow.hPow (α := Associates R) (Associates.mk p) n

Tactic:
rw [prop] at this