-- Mathlib/Algebra/Module/DedekindDomain.lean
theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal [DecidableEq (Ideal R)]
    {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M I) :
    DirectSum.IsInternal fun p : (factors I).toFinset =>
      torsionBySet R M (p ^ (factors I).count ↑p : Ideal R)

Proof state:
case hJ
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ Irreducible p

Tactic:
exact (prime_of_mem p hp).irreducible

Result:
no goals

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤

Tactic:
rw [irreducible_pow_sup]

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ p ^ (Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) ⊓ Multiset.count p P) = ⊤

case hI
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ ⊥

case hJ
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ Irreducible p

Proof state:
case h.e'_6.h.e'_4.coprime
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ∀ i ∈ (factors I).toFinset, ∀ j ∈ (factors I).toFinset, i ≠ j → i ≠ j

Tactic:
exact fun _ _ _ _ ij => ij

Result:
no goals

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤

Tactic:
dsimp

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ p ^ Multiset.count p P ⊔ q ^ Multiset.count q P = ⊤

Proof state:
case hI
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ ⊥

Tactic:
rw [← Ideal.zero_eq_bot]

Result:
case hI
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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ 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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Tactic:
apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P)

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ (↑(factors I).toFinset).Pairwise fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0

Tactic:
rw [Multiset.count_eq_zero,
  normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
  Multiset.mem_replicate]

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)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ ¬(Multiset.count q P ≠ 0 ∧ p = normalize q)