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

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

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ z✝ ∈ rcomp (rcomp t s) r ↔ z✝ ∈ rcomp t (rcomp s r)
Tactic:
simp only [mem_rcomp_iff]
State after:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ (∃ a b c,
      z✝ = opair a c ∧ (∃ a b_1 c_1, opair b c = opair a c_1 ∧ opair b_1 c_1 ∈ t ∧ opair a b_1 ∈ s) ∧ opair a b ∈ r) ↔
    ∃ a b c, z✝ = opair a c ∧ opair b c ∈ t ∧ ∃ a_1 b_1 c, opair a b = opair a_1 c ∧ opair b_1 c ∈ s ∧ opair a_1 b_1 ∈ r

State before:
case h
V : Type u_1
inst✝ : Zermelo V
r x y z t s z✝ : V
⊢ (∃ a b c,
      z✝ = opair a c ∧ (∃ a b_1 c_1, opair b c = opair a c_1 ∧ opair b_1 c_1 ∈ t ∧ opair a b_1 ∈ s) ∧ opair a b ∈ r) ↔
    ∃ a b c, z✝ = opair a c ∧ opair b c ∈ t ∧ ∃ a_1 b_1 c, opair a b = opair a_1 c ∧ opair b_1 c ∈ s ∧ opair a_1 b_1 ∈ r
Tactic:
aesop
State after:
no goals