Theorem: LO.FirstOrder.Completeness.chain_monotone (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[u]
Tactic:
suffices ∀ d, ⛓️[s] ⊆ ⛓️[s + d] by
  simpa[Nat.add_sub_of_le h] using this (u - s)
State after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]
Tactic:
intro d
State after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
⊢ ⛓️[s] ⊆ ⛓️[s + d]

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
⊢ ⛓️[s] ⊆ ⛓️[s + d]
Tactic:
induction' d with d ih
State after:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[s + 0]

case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
ih : ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[s + (d + 1)]

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
this : ∀ (d : ℕ), ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[u]
Tactic:
simpa[Nat.add_sub_of_le h] using this (u - s)
State after:
no goals

State before:
case zero
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
⊢ ⛓️[s] ⊆ ⛓️[s + 0]
Tactic:
simp
State after:
no goals

State before:
case succ
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
s u : ℕ
h : s ≤ u
d : ℕ
ih : ⛓️[s] ⊆ ⛓️[s + d]
⊢ ⛓️[s] ⊆ ⛓️[s + (d + 1)]
Tactic:
simpa only [Nat.add_succ] using subset_trans ih <| ReduxNat.antimonotone (chain_spec nwf (s + d))
State after:
no goals