case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
h : Intersecting s
⊢ s ≠ {⊥}

case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
⊢ Intersecting s ↔ (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
refine' ⟨fun h => ⟨fun a ha b hb _ => h ha hb, _⟩, fun h a ha b hb hab => _⟩
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
⊢ False
have := h.1.eq ha hb (Classical.not_not.2 hab)
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Disjoint a b
this : a = b
⊢ False
rw [this, disjoint_self] at hab
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : b = ⊥
this : a = b
⊢ False
rw [hab] at hb
no goals
case refine'_2
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a✝ b✝ c : α
h : (Set.Pairwise s fun a b => ¬Disjoint a b) ∧ s ≠ {⊥}
a : α
ha : a ∈ s
b : α
hb : ⊥ ∈ s
hab : b = ⊥
this : a = b
⊢ False
exact
  h.2
    (eq_singleton_iff_unique_mem.2
      ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
t : Set α
a b c : α
h : Intersecting {⊥}
⊢ False
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s t : Set α
a b c : α
h : Intersecting s
⊢ s ≠ {⊥}
rintro rfl
no goals
case refine'_1
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
t : Set α
a b c : α
h : Intersecting {⊥}
⊢ False
exact intersecting_singleton.1 h rfl