case h.mk
α : Type u_1
s t : Set α
x y : α
⊢ ((x, y) ∈ range fun x => (x, x)) ↔ (x, y) ∈ diagonal α
α : Type u_1
s t : Set α
⊢ (range fun x => (x, x)) = diagonal α
ext ⟨x, y⟩
no goals
case h.mk
α : Type u_1
s t : Set α
x y : α
⊢ ((x, y) ∈ range fun x => (x, x)) ↔ (x, y) ∈ diagonal α
simp [diagonal, eq_comm]