-- 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:
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)

Tactic:
exact fun H => pq <| H.2.trans <| normalize_eq q

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
this : Multiset.count p (normalizedFactors ?m.8521) = 0
⊢ p ^ (Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) ⊓ Multiset.count p P) = ⊤

Tactic:
rw [this, zero_min, pow_zero, Ideal.one_eq_top]

Result:
no goals

Proof state:
case h.e'_6.h.e'_4
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, i ^ Multiset.count i P = I

Tactic:
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_prime_pow_eq_prod, ← Finset.prod_multiset_count,
  ← associated_iff_eq]

Result:
case h.e'_6.h.e'_4
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
⊢ Associated (factors I).prod I

case h.e'_6.h.e'_4.prime
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, Prime i

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

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
⊢ Module.IsTorsionBySet R M ↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P)

Tactic:
convert hM

Result:
case h.e'_6.h.e'_4
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, i ^ Multiset.count i P = I

Proof state:
case h.e'_6.h.e'_4
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
⊢ Associated (factors I).prod I

Tactic:
exact factors_prod hI

Result:
no goals

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 ≠ 0

Tactic:
apply pow_ne_zero

Result:
case hI.h
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 ≠ 0

Proof state:
case h.e'_6.h.e'_4.prime
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, Prime i

Tactic:
exact prime_of_mem

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
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Tactic:
let P := factors I

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
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Proof state:
case hI.h
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 ≠ 0

Tactic:
exact (prime_of_mem q hq).ne_zero

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
⊢ (↑(factors I).toFinset).Pairwise fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤

Tactic:
intro p hp q hq pq

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
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤