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

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
this : ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
⊢ Hierarchy Γ' s' p
Tactic:
simpa [show s + (s' - s.succ) + 1 = s' from by simpa [Nat.succ_add] using Nat.add_sub_of_le h] using this (s' - s.succ)
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
Tactic:
intro d
State after:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
d : ℕ
⊢ Hierarchy Γ' (s + d + 1) p

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
d : ℕ
⊢ Hierarchy Γ' (s + d + 1) p
Tactic:
induction' d with s ih
State after:
case zero
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ Hierarchy Γ' (s + 0 + 1) p

case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s✝ : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s✝ p
Γ' : Polarity
s' : ℕ
h : s✝ < s'
s : ℕ
ih : Hierarchy Γ' (s✝ + s + 1) p
⊢ Hierarchy Γ' (s✝ + (s + 1) + 1) p

State before:
case zero
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
⊢ Hierarchy Γ' (s + 0 + 1) p
Tactic:
simpa using hp.accum Γ'
State after:
no goals

State before:
case succ
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s✝ : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s✝ p
Γ' : Polarity
s' : ℕ
h : s✝ < s'
s : ℕ
ih : Hierarchy Γ' (s✝ + s + 1) p
⊢ Hierarchy Γ' (s✝ + (s + 1) + 1) p
Tactic:
simpa only [Nat.add_succ, add_zero] using ih.accum _
State after:
no goals

State before:
L : Language
inst✝ : L.LT
μ : Type v
n : ℕ
Γ : Polarity
s : ℕ
p : Semiformula L μ n
hp : Hierarchy Γ s p
Γ' : Polarity
s' : ℕ
h : s < s'
this : ∀ (d : ℕ), Hierarchy Γ' (s + d + 1) p
⊢ s + (s' - s.succ) + 1 = s'
Tactic:
simpa [Nat.succ_add] using Nat.add_sub_of_le h
State after:
no goals