Theorem: Lean4Axiomatic.Natural.trans_le_lt_lt (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:
have : n < m ∨ n ≃ m := le_split ‹n ≤ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
⊢ 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
this : n < m ∨ n ≃ m
⊢ n < k
Tactic:
match this with
| Or.inl (_ : n < m) =>
  have : n < k := lt_trans ‹n < m› ‹m < k›
  exact this
| Or.inr (_ : n ≃ m) =>
  have : n < k := trans_eqv_lt_lt ‹n ≃ m› ‹m < k›
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
h✝ : n < m
⊢ n < k
Tactic:
have : n < k := lt_trans ‹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
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : n < 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
this✝ : n < m ∨ n ≃ m
h✝ : n < m
this : n < k
⊢ n < k
Tactic:
exact this
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
x✝ : m < k
this : n < m ∨ n ≃ m
h✝ : n ≃ m
⊢ n < k
Tactic:
have : n < k := trans_eqv_lt_lt ‹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
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : n < 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
this✝ : n < m ∨ n ≃ m
h✝ : n ≃ m
this : n < k
⊢ n < k
Tactic:
exact this
State after:
no goals