Theorem: SetTheory.image_inverse (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ image (inverse r) x = preimage r x
Tactic:
ext y
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ image (inverse r) x ↔ y ∈ preimage r x

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ image (inverse r) x ↔ y ∈ preimage r x
Tactic:
simp only [mem_image_iff, mem_preimage_iff, mem_inverse_iff]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair y z ∈ r

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair y z ∈ r
Tactic:
aesop
State after:
no goals