Theorem: LO.FirstOrder.Arith.Hierarchy.of_zero (Logic/FirstOrder/Arith/Hierarchy.lean)

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' s p
Tactic:
rcases Nat.eq_or_lt_of_le (Nat.zero_le s) with (rfl | pos)
State after:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' 0 p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
pos : 0 < s
⊢ Hierarchy b' s p

State before:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
p : Semiformula L μ n
hp : Hierarchy b 0 p
⊢ Hierarchy b' 0 p
Tactic:
exact zero_iff.mp hp
State after:
no goals

State before:
case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
b b' : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy b 0 p
pos : 0 < s
⊢ Hierarchy b' s p
Tactic:
exact strict_mono hp b' pos
State after:
no goals