α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ Disjoint s {a}
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ offDiag (insert a s) = offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}
rw [insert_eq, union_comm, offDiag_union, offDiag_singleton, union_empty, union_right_comm]
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 ∈ {a}
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ Disjoint s {a}
rw [disjoint_left]
α : Type u_1
s t : Set α
x : α × α
b : α
hb : b ∈ s
ha : ¬b ∈ s
⊢ False
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 ∈ {a}
rintro b hb (rfl : b = a)
no goals
α : Type u_1
s t : Set α
x : α × α
b : α
hb : b ∈ s
ha : ¬b ∈ s
⊢ False
exact ha hb