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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ inverse r ↔ ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
unfold inverse
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memInverse (Sum.inr 0) (Sum.inl ())) (fun x => r) (prod (ran r) (dom r)) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memInverse (Sum.inr 0) (Sum.inl ())) (fun x => r) (prod (ran r) (dom r)) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memInverse']
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) ↔
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
constructor
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) →
    ∃ y z, x = opair y z ∧ opair z y ∈ r

case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (∃ y z, x = opair y z ∧ opair z y ∈ r) →
    x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())) →
    ∃ y z, x = opair y z ∧ opair z y ∈ r
Tactic:
aesop
State after:
no goals

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (∃ y z, x = opair y z ∧ opair z y ∈ r) →
    x ∈ prod (ran r) (dom r) ∧
      ∃ y z,
        interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inr 0) = opair y z ∧
          opair z y ∈ interpretTerm V (fun x => r) (fun x_1 => x) (Sum.inl ())
Tactic:
rintro ⟨a, b, rfl, ha⟩
State after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r) ∧
    ∃ y z,
      interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
        opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())

State before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r) ∧
    ∃ y z,
      interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
        opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
Tactic:
refine ⟨?_, by aesop⟩
State after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r)

State before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ opair a b ∈ prod (ran r) (dom r)
Tactic:
rw [mem_prod_iff]
State after:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ a_1, a_1 ∈ ran r ∧ ∃ b_1, b_1 ∈ dom r ∧ opair a b = opair a_1 b_1

State before:
case mpr.intro.intro.intro
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ a_1, a_1 ∈ ran r ∧ ∃ b_1, b_1 ∈ dom r ∧ opair a b = opair a_1 b_1
Tactic:
refine ⟨a, ?_, b, ?_, rfl⟩
State after:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ a ∈ ran r

case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ b ∈ dom r

State before:
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ y z,
    interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inr 0) = opair y z ∧
      opair z y ∈ interpretTerm V (fun x => r) (fun x => opair a b) (Sum.inl ())
Tactic:
aesop
State after:
no goals

State before:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ a ∈ ran r
Tactic:
rw [mem_ran_iff]
State after:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair z a ∈ r

State before:
case mpr.intro.intro.intro.refine_1
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair z a ∈ r
Tactic:
exact ⟨b, ha⟩
State after:
no goals

State before:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ b ∈ dom r
Tactic:
rw [mem_dom_iff]
State after:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair b z ∈ r

State before:
case mpr.intro.intro.intro.refine_2
V : Type u_1
inst✝ : Zermelo V
r y z a b : V
ha : opair b a ∈ r
⊢ ∃ z, opair b z ∈ r
Tactic:
exact ⟨a, ha⟩
State after:
no goals