-- Mathlib/Algebra/Module/DedekindDomain.lean
theorem isInternal_prime_power_torsion [DecidableEq (Ideal R)] [Module.Finite R M]
    (hM : Module.IsTorsion R M) :
    DirectSum.IsInternal fun p : (factors (⊤ : Submodule R M).annihilator).toFinset =>
      torsionBySet R M (p ^ (factors (⊤ : Submodule R M).annihilator).count ↑p : Ideal R)

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
have hM' := Module.isTorsionBySet_annihilator_top R M

Result:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ ⊤.annihilator ≠ ⊥

Tactic:
rw [← Set.nonempty_iff_ne_empty] at hI

Result:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
⊢ ⊤.annihilator ≠ ⊥

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
refine isInternal_prime_power_torsion_of_is_torsion_by_ideal ?_ hM'

Result:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ ⊤.annihilator ≠ ⊥

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM

Result:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : ↑⊤.annihilator ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
⊢ ⊤.annihilator ≠ ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Result:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
⊢ ∃ x ∈ ⊤.annihilator, x ≠ 0

Proof state:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
⊢ ∃ x ∈ ⊤.annihilator, x ≠ 0

Tactic:
obtain ⟨x, H, hx⟩ := hI

Result:
case intro.intro
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
x : R
H : x ∈ ↑⊤.annihilator
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x ∈ ⊤.annihilator, x ≠ 0

Proof state:
case intro.intro
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDedekindDomain R
inst✝¹ : DecidableEq (Ideal R)
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
x : R
H : x ∈ ↑⊤.annihilator
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x ∈ ⊤.annihilator, x ≠ 0

Tactic:
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩

Result:
no goals