case intro
α : Type u_2
β : Type u_1
f : α → β
x : α
⊢ {x_1 | Rel (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}
α : Type u_2
β : Type u_1
f : α → β
⊢ classes (ker f) ⊆ Set.range fun y => {x | f x = y}
rintro s ⟨x, rfl⟩
case intro
α : Type u_2
β : Type u_1
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | Rel (ker f) x_1 x}
case intro
α : Type u_2
β : Type u_1
f : α → β
x : α
⊢ {x_1 | Rel (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}
rw [Set.mem_range]
no goals
case intro
α : Type u_2
β : Type u_1
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | Rel (ker f) x_1 x}
exact ⟨f x, rfl⟩