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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
⊢ Hierarchy Γ s' p
Tactic:
rcases Nat.lt_or_eq_of_le h with (lt | rfl)
State after:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
lt : s < s'
⊢ Hierarchy Γ s' p

case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s
⊢ Hierarchy Γ s p

State before:
case inl
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s s' : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s'
lt : s < s'
⊢ Hierarchy Γ s' p
Tactic:
exact hp.strict_mono Γ lt
State after:
no goals

State before:
case inr
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
h : s ≤ s
⊢ Hierarchy Γ s p
Tactic:
assumption
State after:
no goals