no goals
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
classical
  exact
    Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
      (by simpa only [Multiset.map_id', Finset.mem_def] using div)
      (by
        intro a
        simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
        change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
        apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
        apply Multiset.nodup_iff_count_le_one.mp
        exact s.nodup)
no goals
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      intro a
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
      change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
      apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
      apply Multiset.nodup_iff_count_le_one.mp
      exact s.nodup)
no goals
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → Prime a
simpa only [Multiset.map_id', Finset.mem_def] using h
no goals
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → a ∣ n
simpa only [Multiset.map_id', Finset.mem_def] using div
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
intro a
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (Eq a) s.val) ≤ 1
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (Eq a) s.val) ≤ 1
change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.count a s.val ≤ 1
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
case a
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.Nodup s.val
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.count a s.val ≤ 1
apply Multiset.nodup_iff_count_le_one.mp
no goals
case a
α : Type u_1
β : Type ?u.20971
γ : Type ?u.20974
δ : Type ?u.20977
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.Nodup s.val
exact s.nodup