Theorem: lindenbaumStageMonotone (Fine/SystemB/Lindenbaum.lean)

State before:
t : Th
Δ : Ctx
i : ℕ
⊢ Monotone fun j => lindenbaumSequence t Δ (i, j)
Tactic:
intros a b h₁
State after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ (fun j => lindenbaumSequence t Δ (i, j)) a ≤ (fun j => lindenbaumSequence t Δ (i, j)) b

State before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ (fun j => lindenbaumSequence t Δ (i, j)) a ≤ (fun j => lindenbaumSequence t Δ (i, j)) b
Tactic:
change lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
State after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)

State before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Tactic:
have l₂ := (Prod.Lex.le_iff (i, a) (i,b)).mpr $ Or.inr ⟨rfl,h₁⟩
State after:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
l₂ : ↑toLex (i, a) ≤ ↑toLex (i, b)
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)

State before:
t : Th
Δ : Ctx
i a b : ℕ
h₁ : a ≤ b
l₂ : ↑toLex (i, a) ≤ ↑toLex (i, b)
⊢ lindenbaumSequence t Δ (i, a) ≤ lindenbaumSequence t Δ (i, b)
Tactic:
exact lindenbaumSequenceMonotone' (i,b) (i,a) l₂
State after:
no goals