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