case a
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
this : Directed (fun x x_1 => x ≥ x_1) fun s => 𝓟 ↑s
U : Set α
⊢ U ∈ FilterBasis.filter B ↔ U ∈ ⨅ (s : ↑B.sets), 𝓟 ↑s
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
this : Directed (fun x x_1 => x ≥ x_1) fun s => 𝓟 ↑s
⊢ FilterBasis.filter B = ⨅ (s : ↑B.sets), 𝓟 ↑s
ext U
no goals
case a
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
this : Directed (fun x x_1 => x ≥ x_1) fun s => 𝓟 ↑s
U : Set α
⊢ U ∈ FilterBasis.filter B ↔ U ∈ ⨅ (s : ↑B.sets), 𝓟 ↑s
simp [mem_filter_iff, mem_iInf_of_directed this]
case mk.mk
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in }) ((fun s => 𝓟 ↑s) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in }) ((fun s => 𝓟 ↑s) z)
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
⊢ Directed (fun x x_1 => x ≥ x_1) fun s => 𝓟 ↑s
rintro ⟨U, U_in⟩ ⟨V, V_in⟩
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in }) ((fun s => 𝓟 ↑s) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in }) ((fun s => 𝓟 ↑s) z)
case mk.mk
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in }) ((fun s => 𝓟 ↑s) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in }) ((fun s => 𝓟 ↑s) z)
rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in })
      ((fun s => 𝓟 ↑s) { val := W, property := W_in }) ∧
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in })
      ((fun s => 𝓟 ↑s) { val := W, property := W_in })
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in }) ((fun s => 𝓟 ↑s) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in }) ((fun s => 𝓟 ↑s) z)
use ⟨W, W_in⟩
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := U, property := U_in })
      ((fun s => 𝓟 ↑s) { val := W, property := W_in }) ∧
    (fun x x_1 => x ≥ x_1) ((fun s => 𝓟 ↑s) { val := V, property := V_in })
      ((fun s => 𝓟 ↑s) { val := W, property := W_in })
simp only [ge_iff_le, le_principal_iff, mem_principal, Subtype.coe_mk]
no goals
case mk.mk.intro.intro
α : Type u_1
β : Type ?u.4090
γ : Type ?u.4093
ι : Sort ?u.4096
ι' : Sort ?u.4099
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V
exact subset_inter_iff.mp W_sub