Theorem: SetTheory.interpret_memRComp' (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x s r : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.memRComp x s r) v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r
Tactic:
unfold BoundedFormula.memRComp
State after:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x s r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.exists
              (BoundedFormula.exists
                (BoundedFormula.and
                  (BoundedFormula.and
                    (BoundedFormula.and
                      (BoundedFormula.and
                        (BoundedFormula.eqOPair (termSucc (termSucc (termSucc (termSucc (termSucc x)))))
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                        (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })))
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) })))
                    (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                      (termSucc (termSucc (termSucc (termSucc (termSucc s)))))))
                  (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                    (termSucc (termSucc (termSucc (termSucc (termSucc r))))))))))))
      v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r

State before:
V : Type u_1
inst✝ : Zermelo V
r✝ x✝ y z : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x s r : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.exists
            (BoundedFormula.exists
              (BoundedFormula.exists
                (BoundedFormula.and
                  (BoundedFormula.and
                    (BoundedFormula.and
                      (BoundedFormula.and
                        (BoundedFormula.eqOPair (termSucc (termSucc (termSucc (termSucc (termSucc x)))))
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) }))
                        (BoundedFormula.eqOPair (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                          (Sum.inr { val := n, isLt := (_ : n < n + (4 + 1)) })
                          (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })))
                      (BoundedFormula.eqOPair (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                        (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (3 + 1)) })
                        (Sum.inr { val := n + 2, isLt := (_ : n + 2 < n + 2 + (2 + 1)) })))
                    (BoundedFormula.mem (Sum.inr { val := n + 4, isLt := (_ : n + 4 < n + 4 + (0 + 1)) })
                      (termSucc (termSucc (termSucc (termSucc (termSucc s)))))))
                  (BoundedFormula.mem (Sum.inr { val := n + 3, isLt := (_ : n + 3 < n + 3 + (1 + 1)) })
                    (termSucc (termSucc (termSucc (termSucc (termSucc r))))))))))))
      v l ↔
    ∃ a b c, interpretTerm V v l x = opair a c ∧ opair b c ∈ interpretTerm V v l s ∧ opair a b ∈ interpretTerm V v l r
Tactic:
simp [and_assoc]
State after:
no goals