Theorem: Lean4Axiomatic.Natural.trans_le_eqv_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_eqv_subst ‹m ≃ k› ‹n ≤ m›
State after:
no goals