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

State before:
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x ↔ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
constructor
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x → ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x

case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ (∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x) → Inductive x

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ Inductive x → ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
intro h
State after:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
h : Inductive x
⊢ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x

State before:
case mp
V : Type u_1
inst✝ : Zermelo V
x : V
h : Inductive x
⊢ ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
Tactic:
exact ⟨h.empty_mem, h.succ_mem⟩
State after:
no goals

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
⊢ (∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x) → Inductive x
Tactic:
intro h
State after:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
h : ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
⊢ Inductive x

State before:
case mpr
V : Type u_1
inst✝ : Zermelo V
x : V
h : ∅ ∈ x ∧ ∀ (y : V), y ∈ x → succ y ∈ x
⊢ Inductive x
Tactic:
exact ⟨h.1, h.2⟩
State after:
no goals