case a
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
⊢ replicate n x ∩ s = replicate (min n (count x s)) x
ext y
case a
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
case a
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)
rw [count_inter, count_replicate, count_replicate]
case pos
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0

case neg
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
case a
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
by_cases h : y = x
no goals
case pos
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
simp only [h, if_true]
no goals
case neg
α : Type u_1
β : Type ?u.422106
γ : Type ?u.422109
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬y = x
⊢ min (if y = x then n else 0) (count y s) = if y = x then min n (count x s) else 0
simp only [h, if_false, zero_min]