Theorem: Nat.add_lt_add_of_lt (Table/BuiltinExtensions.lean)

State before:
⊢ ∀ (a m n : Nat), m < n → m + a < n + a
Tactic:
intros a m n h
State after:
a m n : Nat
h : m < n
⊢ m + a < n + a

State before:
a m n : Nat
h : m < n
⊢ m + a < n + a
Tactic:
induction a with
| zero => exact h
| succ n' ih =>
 rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
 apply Nat.succ_lt_succ
 exact ih
State after:
no goals

State before:
case zero
m n : Nat
h : m < n
⊢ m + zero < n + zero
Tactic:
exact h
State after:
no goals

State before:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + succ n' < n + succ n'
Tactic:
rw [←Nat.add_one, ←Nat.add_assoc, ←Nat.add_assoc, Nat.add_one, Nat.add_one]
State after:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ succ (m + n') < succ (n + n')

State before:
case succ
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ succ (m + n') < succ (n + n')
Tactic:
apply Nat.succ_lt_succ
State after:
case succ.a
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + n' < n + n'

State before:
case succ.a
m n : Nat
h : m < n
n' : Nat
ih : m + n' < n + n'
⊢ m + n' < n + n'
Tactic:
exact ih
State after:
no goals