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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈ rcomp s r ↔ ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
unfold rcomp
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈
      sep (BoundedFormula.memRComp (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then s else r)
        (prod (dom r) (ran s)) ↔
    ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ x ∈
      sep (BoundedFormula.memRComp (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then s else r)
        (prod (dom r) (ran s)) ↔
    ∃ a b c, x = opair a c ∧ opair b c ∈ s ∧ opair a b ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memRComp', interpret_inr, interpret_inl, ite_true, ite_false,
  and_iff_right_iff_imp, forall_exists_index, and_imp]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ prod (dom r) (ran s)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z s : V
⊢ ∀ (x_1 x_2 x_3 : V), x = opair x_1 x_3 → opair x_2 x_3 ∈ s → opair x_1 x_2 ∈ r → x ∈ prod (dom r) (ran s)
Tactic:
rintro a b c rfl hs hr
State after:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ opair a c ∈ prod (dom r) (ran s)

State before:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ opair a c ∈ prod (dom r) (ran s)
Tactic:
rw [mem_prod_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ a_1, a_1 ∈ dom r ∧ ∃ b, b ∈ ran s ∧ opair a c = opair a_1 b

State before:
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ a_1, a_1 ∈ dom r ∧ ∃ b, b ∈ ran s ∧ opair a c = opair a_1 b
Tactic:
refine ⟨a, ?_, c, ?_, rfl⟩
State after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ a ∈ dom r

case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ c ∈ ran s

State before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ a ∈ dom r
Tactic:
rw [mem_dom_iff]
State after:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair a z ∈ r

State before:
case refine_1
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair a z ∈ r
Tactic:
exact ⟨b, hr⟩
State after:
no goals

State before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ c ∈ ran s
Tactic:
rw [mem_ran_iff]
State after:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair z c ∈ s

State before:
case refine_2
V : Type u_1
inst✝ : Zermelo V
r y z s a b c : V
hs : opair b c ∈ s
hr : opair a b ∈ r
⊢ ∃ z, opair z c ∈ s
Tactic:
exact ⟨b, hs⟩
State after:
no goals