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

State before:
t : Th
Δ : Ctx
⊢ Monotone (lindenbaumSequence t Δ)
Tactic:
intros a b
State after:
t : Th
Δ : Ctx
a b : Lex (ℕ × ℕ)
⊢ a ≤ b → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ b

State before:
t : Th
Δ : Ctx
a b : Lex (ℕ × ℕ)
⊢ a ≤ b → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ b
Tactic:
exact lindenbaumSequenceMonotone' b a
State after:
no goals