α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
⊢ IsUpperSet s
rintro a b hab ha
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ Insert.insert b s

α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ Intersecting (Insert.insert b s)
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
rw [h (Insert.insert b s) _ (subset_insert _ _)]
no goals
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ Intersecting (Insert.insert b s)
exact
  hs.insert (mt (eq_bot_mono hab) <| hs.ne_bot ha) fun c hc hbc => hs ha hc <| hbc.mono_left hab
no goals
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
hs : Intersecting s
h : ∀ (t : Set α), Intersecting t → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ Insert.insert b s
exact mem_insert _ _