Theorem: SetTheory.interpret_eqOPair (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.eqOPair x y z) v l ↔
    interpretTerm V v l x = opair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
unfold BoundedFormula.eqOPair opair
State after:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.eqSingleton (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc y)) (termSucc (termSucc z))))
            (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    interpretTerm V v l x = pair {interpretTerm V v l y} (pair (interpretTerm V v l y) (interpretTerm V v l z))

State before:
V : Type u_1
inst✝ : Zermelo V
x✝ y✝ z✝ : V
α : Type
n : Nat
v : α → V
l : Fin n → V
x y z : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.exists
        (BoundedFormula.exists
          (BoundedFormula.and
            (BoundedFormula.and
              (BoundedFormula.eqSingleton (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) }) (termSucc (termSucc y)))
              (BoundedFormula.eqPair (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })
                (termSucc (termSucc y)) (termSucc (termSucc z))))
            (BoundedFormula.eqPair (termSucc (termSucc x)) (Sum.inr { val := n, isLt := (_ : n < n + (1 + 1)) })
              (Sum.inr { val := n + 1, isLt := (_ : n + 1 < n + 1 + (0 + 1)) })))))
      v l ↔
    interpretTerm V v l x = pair {interpretTerm V v l y} (pair (interpretTerm V v l y) (interpretTerm V v l z))
Tactic:
aesop
State after:
no goals