Theorem: SetTheory.interpret_eqPair (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.eqPair x y z) v l ↔
    interpretTerm V v l x = pair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
unfold BoundedFormula.eqPair
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.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = 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.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    interpretTerm V v l x = pair (interpretTerm V v l y) (interpretTerm V v l z)
Tactic:
rw [eq_pair_iff]
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.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (t : V), t ∈ interpretTerm V v l x ↔ t = interpretTerm V v l y ∨ t = 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.all
        (BoundedFormula.iff (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))
          (BoundedFormula.or (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc y))
            (BoundedFormula.eq (Sum.inr (Fin.last n)) (termSucc z)))))
      v l ↔
    ∀ (t : V), t ∈ interpretTerm V v l x ↔ t = interpretTerm V v l y ∨ t = interpretTerm V v l z
Tactic:
simp
State after:
no goals