Theorem: Lean4Axiomatic.Natural.trans_eqv_le_le (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:
exact le_subst_eqv (Rel.symm ‹n ≃ m›) ‹m ≤ k›
State after:
no goals