Theorem: Nat.tri_add_self_lt_tri_of_lt (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
m n : Nat
⊢ m < n → m.tri + m < n.tri
Tactic:
intro h
State after:
m n : Nat
h : m < n
⊢ m.tri + m < n.tri

State before:
m n : Nat
h : m < n
⊢ m.tri + m < n.tri
Tactic:
transitivity (tri (m+1)) using LT.lt, LE.le
State after:
case left
m n : Nat
h : m < n
⊢ m.tri + m < (m + 1).tri

case right
m n : Nat
h : m < n
⊢ (m + 1).tri ≤ n.tri

State before:
case left
m n : Nat
h : m < n
⊢ m.tri + m < (m + 1).tri
Tactic:
exact Nat.lt_succ_self ..
State after:
no goals

State before:
case right
m n : Nat
h : m < n
⊢ (m + 1).tri ≤ n.tri
Tactic:
apply Nat.tri_mono
State after:
case right.a
m n : Nat
h : m < n
⊢ m + 1 ≤ n

State before:
case right.a
m n : Nat
h : m < n
⊢ m + 1 ≤ n
Tactic:
exact Nat.succ_le_of_lt h
State after:
no goals