no goals
α : Type u_1
β : Type ?u.13543
ι : Type ?u.13546
ι' : Type ?u.13549
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f✝ : ι → α
i : ι
f : Bool → α
⊢ true ≠ false
simp only [Ne.def, not_false_iff]