Theorem: LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero (Logic/FirstOrder/Arith/StrictHierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p ↔ DeltaZero p
Tactic:
constructor
State after:
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p

case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ DeltaZero p → StrictHierarchy Γ 0 p

State before:
case mp
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ StrictHierarchy Γ 0 p → DeltaZero p
Tactic:
rintro ⟨h⟩
State after:
case mp.zero
L : Language
inst✝ : L.LT
μ : Type u_1
n✝ : ℕ
Γ : Polarity
p : Semiformula L μ n✝
n : ℕ
h : DeltaZero p
⊢ DeltaZero p

State before:
case mp.zero
L : Language
inst✝ : L.LT
μ : Type u_1
n✝ : ℕ
Γ : Polarity
p : Semiformula L μ n✝
n : ℕ
h : DeltaZero p
⊢ DeltaZero p
Tactic:
exact h
State after:
no goals

State before:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
⊢ DeltaZero p → StrictHierarchy Γ 0 p
Tactic:
intro h
State after:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
h : DeltaZero p
⊢ StrictHierarchy Γ 0 p

State before:
case mpr
L : Language
inst✝ : L.LT
μ : Type u_1
n : ℕ
Γ : Polarity
p : Semiformula L μ n
h : DeltaZero p
⊢ StrictHierarchy Γ 0 p
Tactic:
exact zero h
State after:
no goals