Theorem: Lean4Axiomatic.Natural.lt_trans (Lean4Axiomatic/Natural/Order.lean)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
⊢ n < m → m < k → n < k
Tactic:
intro (_ : n < m) (_ : m < k)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ n < k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ n < k
Tactic:
apply lt_step_le.mpr
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ step n ≤ k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n < m
x✝ : m < k
⊢ step n ≤ k
Tactic:
calc
  step n ≤ _ := lt_step_le.mp ‹n < m›
  m      ≤ _ := le_from_lt lt_step
  step m ≤ _ := lt_step_le.mp ‹m < k›
  k      ≤ _ := Rel.refl
State after:
no goals