Theorem: HW2.problem_4 (BrownCs22/Homework/Hw2sols.lean)

State before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
⊢ a ≤ b
Tactic:
have hab2 : 2*a ≤ a + b ∨ a + b ≤ 2*b := h (a + b)
State after:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
hab2 : 2 * a ≤ a + b ∨ a + b ≤ 2 * b
⊢ a ≤ b

State before:
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
hab2 : 2 * a ≤ a + b ∨ a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
eliminate hab2 with h1 h2
State after:
case inl
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h1 : 2 * a ≤ a + b
⊢ a ≤ b

case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b

State before:
case inl
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h1 : 2 * a ≤ a + b
⊢ a ≤ b

case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
linarith
State after:
case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b

State before:
case inr
a b : ℤ
h : ∀ (x : ℤ), 2 * a ≤ x ∨ x ≤ 2 * b
h2 : a + b ≤ 2 * b
⊢ a ≤ b
Tactic:
linarith
State after:
no goals