Theorem: le_of_forall_small_le_add (Ray/Misc/Bounds.lean)

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ a ≤ b
Tactic:
apply le_of_forall_pos_lt_add
State after:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ ∀ (ε : ℝ), 0 < ε → a < b + ε

State before:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
⊢ ∀ (ε : ℝ), 0 < ε → a < b + ε
Tactic:
intro e ep
State after:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
⊢ a < b + e

State before:
case h
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
⊢ a < b + e
Tactic:
by_cases et : e ≥ t
State after:
case pos
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ a < b + e

case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : ¬e ≥ t
⊢ a < b + e

State before:
case pos
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ a < b + e
Tactic:
specialize h (t/2) (by bound) (by bound)
State after:
case pos
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ a < b + e

State before:
case pos
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ a < b + e
Tactic:
calc a ≤ b + t/2 := h
  _ ≤ b + e/2 := by bound
  _ < b + e := by bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ 0 < t / 2
Tactic:
bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e ≥ t
⊢ t / 2 < t
Tactic:
bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ b + t / 2 ≤ b + e / 2
Tactic:
bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
e : ℝ
ep : 0 < e
et : e ≥ t
h : a ≤ b + t / 2
⊢ b + e / 2 < b + e
Tactic:
bound
State after:
no goals

State before:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : ¬e ≥ t
⊢ a < b + e
Tactic:
simp only [ge_iff_le, not_le] at et
State after:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ a < b + e

State before:
case neg
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ a < b + e
Tactic:
calc a ≤ b + e/2 := h (e/2) (by bound) (by linarith)
  _ < b + e := by bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ 0 < e / 2
Tactic:
bound
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ e / 2 < t
Tactic:
linarith
State after:
no goals

State before:
a b t : ℝ
tp : 0 < t
h : ∀ (e : ℝ), 0 < e → e < t → a ≤ b + e
e : ℝ
ep : 0 < e
et : e < t
⊢ b + e / 2 < b + e
Tactic:
bound
State after:
no goals