simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₁
ha₂ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₂
⊢ False
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : g a = b₁
ha₂ : g a = b₂
⊢ False