case h
α : Type u_2
β : Type u_1
γ : Type ?u.1450
r : Rel α β
x : β
⊢ x ∈ dom (inv r) ↔ x ∈ codom r
α : Type u_2
β : Type u_1
γ : Type ?u.1450
r : Rel α β
⊢ dom (inv r) = codom r
ext x
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.1450
r : Rel α β
x : β
⊢ x ∈ dom (inv r) ↔ x ∈ codom r
rfl