case h
α : Type u_2
β : Type u_1
γ : Type ?u.16693
r : Rel α β
y : β
⊢ y ∈ image r Set.univ ↔ y ∈ codom r
α : Type u_2
β : Type u_1
γ : Type ?u.16693
r : Rel α β
⊢ image r Set.univ = codom r
ext y
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.16693
r : Rel α β
y : β
⊢ y ∈ image r Set.univ ↔ y ∈ codom r
simp [mem_image, codom]