Theorem: SetTheory.interpret_isInductive (SetTheory/Nat.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V (BoundedFormula.isInductive x) v l ↔ Inductive (interpretTerm V v l x)
Tactic:
unfold BoundedFormula.isInductive
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    Inductive (interpretTerm V v l x)

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    Inductive (interpretTerm V v l x)
Tactic:
rw [inductive_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    ∅ ∈ interpretTerm V v l x ∧ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x

State before:
V : Type u_1
inst✝ : Zermelo V
α : Type
n : Nat
v : α → V
l : Fin n → V
x : α ⊕ Fin n
⊢ Interpret V
      (BoundedFormula.and
        (BoundedFormula.exists
          (BoundedFormula.and (BoundedFormula.eqEmpty (Sum.inr (Fin.last n)))
            (BoundedFormula.mem (Sum.inr (Fin.last n)) (termSucc x))))
        (BoundedFormula.succClosed x))
      v l ↔
    ∅ ∈ interpretTerm V v l x ∧ ∀ (y : V), y ∈ interpretTerm V v l x → succ y ∈ interpretTerm V v l x
Tactic:
simp
State after:
no goals