Theorem: Nat.add_lt_of_le_lt (Jordan/PermMaximal.lean)

State before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < c + d
Tactic:
apply Nat.lt_of_lt_of_le
State after:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < ?m

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ?m ≤ c + d

case m
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ

State before:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + b < ?m

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ?m ≤ c + d

case m
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ
Tactic:
apply Nat.add_lt_add_left _ a
State after:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ

a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < ?m.126

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + ?m.126 ≤ c + d

State before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ ℕ

a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < ?m.126

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + ?m.126 ≤ c + d
Tactic:
use d
State after:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < d

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d

State before:
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ b < d

case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Tactic:
exact hbd
State after:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d

State before:
case a
a b c d : ℕ
hab : a ≤ c
hbd : b < d
⊢ a + d ≤ c + d
Tactic:
apply Nat.add_le_add_right hab d
State after:
no goals