case h
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s ↔ x ∈ diagonal α ∩ s ×ˢ s
α : Type u_1
s✝ t s : Set α
⊢ (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s
ext x
case h.mp
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s → x ∈ diagonal α ∩ s ×ˢ s

case h.mpr
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ diagonal α ∩ s ×ˢ s → x ∈ (fun x => (x, x)) '' s
case h
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s ↔ x ∈ diagonal α ∩ s ×ˢ s
constructor
case h.mp.intro.intro
α : Type u_1
s✝ t s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (x, x)) x ∈ diagonal α ∩ s ×ˢ s
case h.mp
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s → x ∈ diagonal α ∩ s ×ˢ s
rintro ⟨x, hx, rfl⟩
no goals
case h.mp.intro.intro
α : Type u_1
s✝ t s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (x, x)) x ∈ diagonal α ∩ s ×ˢ s
exact ⟨rfl, hx, hx⟩
case h.mpr.mk
α : Type u_1
s✝ t s : Set α
x y : α
⊢ (x, y) ∈ diagonal α ∩ s ×ˢ s → (x, y) ∈ (fun x => (x, x)) '' s
case h.mpr
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ diagonal α ∩ s ×ˢ s → x ∈ (fun x => (x, x)) '' s
obtain ⟨x, y⟩ := x
case h.mpr.mk.intro
α : Type u_1
s✝ t s : Set α
x : α
h2x : (x, x) ∈ s ×ˢ s
⊢ (x, x) ∈ (fun x => (x, x)) '' s
case h.mpr.mk
α : Type u_1
s✝ t s : Set α
x y : α
⊢ (x, y) ∈ diagonal α ∩ s ×ˢ s → (x, y) ∈ (fun x => (x, x)) '' s
rintro ⟨rfl : x = y, h2x⟩
no goals
case h.mpr.mk.intro
α : Type u_1
s✝ t s : Set α
x : α
h2x : (x, x) ∈ s ×ˢ s
⊢ (x, x) ∈ (fun x => (x, x)) '' s
exact mem_image_of_mem _ h2x.1