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

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

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

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ x ∈ r
Tactic:
constructor
State after:
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ (∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) → x ∈ r

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ r → ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r

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

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
⊢ x ∈ r → ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Tactic:
intro h
State after:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
h : x ∈ r
⊢ ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r

State before:
case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x✝ y z : V
hr : IsRelation r
x : V
h : x ∈ r
⊢ ∃ y z, x = opair y z ∧ ∃ y_1 z_1, opair z y = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r
Tactic:
obtain ⟨y, z, rfl⟩ := hr x h
State after:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z✝ : V
hr : IsRelation r
y z : V
h : opair y z ∈ r
⊢ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ ∃ y z, opair z_1 y_1 = opair y z ∧ opair z y ∈ r

State before:
case h.mpr.intro.intro
V : Type u_1
inst✝ : Zermelo V
r x y✝ z✝ : V
hr : IsRelation r
y z : V
h : opair y z ∈ r
⊢ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ ∃ y z, opair z_1 y_1 = opair y z ∧ opair z y ∈ r
Tactic:
exact ⟨y, z, rfl, z, y, rfl, h⟩
State after:
no goals