case mp
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u) → ∃ u, u ∈ f ∧ P u ∧ Q u

case mpr
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u, u ∈ f ∧ P u ∧ Q u) → (∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u) ↔ ∃ u, u ∈ f ∧ P u ∧ Q u
constructor
case mp.intro.intro.intro.intro.intro
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u, u ∈ f ∧ P u ∧ Q u
case mp
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ ((∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u) → ∃ u, u ∈ f ∧ P u ∧ Q u
rintro ⟨⟨u, huf, hPu⟩, v, hvf, hQv⟩
no goals
case mp.intro.intro.intro.intro.intro
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
v : Set α
hvf : v ∈ f
hQv : Q v
⊢ ∃ u, u ∈ f ∧ P u ∧ Q u
exact
  ⟨u ∩ v, inter_mem huf hvf, hP (inter_subset_left _ _) hPu, hQ (inter_subset_right _ _) hQv⟩
case mpr.intro.intro.intro
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u
case mpr
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
⊢ (∃ u, u ∈ f ∧ P u ∧ Q u) → (∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u
rintro ⟨u, huf, hPu, hQu⟩
no goals
case mpr.intro.intro.intro
α : Type u
f g : Filter α
s t : Set α
P Q : Set α → Prop
hP : Antitone P
hQ : Antitone Q
u : Set α
huf : u ∈ f
hPu : P u
hQu : Q u
⊢ (∃ u, u ∈ f ∧ P u) ∧ ∃ u, u ∈ f ∧ Q u
exact ⟨⟨u, huf, hPu⟩, u, huf, hQu⟩