no goals
α : Type u_1
β : Type u_2
γ : Type ?u.139592
ι : Type ?u.139595
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x → p x ∨ q x
tauto
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.139592
ι : Type ?u.139595
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), q x → p x ∨ q x
tauto