case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b c✝ : α
hs : Intersecting s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint c c

case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
ha : b ≠ ⊥
h : ∀ (b_1 : α), b_1 ∈ s → ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c

case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint b c

case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b✝ c✝ : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
⊢ Intersecting (Insert.insert a s)
rintro b (rfl | hb) c (rfl | hc)
no goals
case inl.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b c✝ : α
hs : Intersecting s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint c c
rwa [disjoint_self]
no goals
case inl.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
ha : b ≠ ⊥
h : ∀ (b_1 : α), b_1 ∈ s → ¬Disjoint b b_1
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
exact h _ hc
no goals
case inr.inl
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
b✝ c✝ : α
hs : Intersecting s
b : α
hb : b ∈ s
c : α
ha : c ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint c b
⊢ ¬Disjoint b c
exact fun H => h _ hb H.symm
no goals
case inr.inr
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b✝ c✝ : α
hs : Intersecting s
ha : a ≠ ⊥
h : ∀ (b : α), b ∈ s → ¬Disjoint a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
⊢ ¬Disjoint b c
exact hs hb hc