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

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

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ preimage (inverse r) x ↔ y ∈ image 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 y z = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair z y ∈ 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 y z = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair z y ∈ r
Tactic:
aesop
State after:
no goals