Theorem: Lean4Axiomatic.Natural.le_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)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
⊢ m ≤ k → n ≤ k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
⊢ m ≤ k → n ≤ k
Tactic:
have ⟨d, (_ : n + d ≃ m)⟩ := le_defn.mp ‹n ≤ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ k → n ≤ k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ k → n ≤ k
Tactic:
apply ind_on (motive := λ k => m ≤ k → n ≤ k) k
State after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ m ≤ 0 → n ≤ 0
Tactic:
case zero =>
  intro (_ : m ≤ 0)
  have ⟨e, (_ : m + e ≃ 0)⟩ := le_defn.mp ‹m ≤ 0›
  show n ≤ 0
  apply le_defn.mpr
  exists d + e
  show n + (d + e) ≃ 0
  calc
    n + (d + e) ≃ _ := Rel.symm AA.assoc
    (n + d) + e ≃ _ := AA.substL ‹n + d ≃ m›
    m + e       ≃ _ := ‹m + e ≃ 0›
    0           ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
Tactic:
case step =>
  intro k (ih : m ≤ k → n ≤ k) (_ : m ≤ step k)
  show n ≤ step k
  match le_step_split ‹m ≤ step k› with
  | Or.inl (_ : m ≤ k) =>
    exact le_step (ih ‹m ≤ k›)
  | Or.inr (_ : m ≃ step k) =>
    exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
x✝ : m ≤ 0
⊢ n ≤ 0
Tactic:
have ⟨e, (_ : m + e ≃ 0)⟩ := le_defn.mp ‹m ≤ 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n ≤ 0

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n ≤ 0
Tactic:
apply le_defn.mpr
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ ∃ k, n + k ≃ 0

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ ∃ k, n + k ≃ 0
Tactic:
exists d + e
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n + (d + e) ≃ 0

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
x✝ : m ≤ 0
e : ℕ
h✝ : m + e ≃ 0
⊢ n + (d + e) ≃ 0
Tactic:
calc
  n + (d + e) ≃ _ := Rel.symm AA.assoc
  (n + d) + e ≃ _ := AA.substL ‹n + d ≃ m›
  m + e       ≃ _ := ‹m + e ≃ 0›
  0           ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
x✝ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
⊢ ∀ (m_1 : ℕ), (m ≤ m_1 → n ≤ m_1) → m ≤ step m_1 → n ≤ step m_1
Tactic:
intro k (ih : m ≤ k → n ≤ k) (_ : m ≤ step k)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
⊢ n ≤ step k

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
⊢ n ≤ step k
Tactic:
match le_step_split ‹m ≤ step k› with
| Or.inl (_ : m ≤ k) =>
  exact le_step (ih ‹m ≤ k›)
| Or.inr (_ : m ≃ step k) =>
  exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
h✝ : m ≤ k
⊢ n ≤ step k
Tactic:
exact le_step (ih ‹m ≤ k›)
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝¹ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
h✝ : m ≃ step k
⊢ n ≤ step k
Tactic:
exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
State after:
no goals