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

State before:
x : ℝ
⊢ 0 ≤ x → x ≤ 1 / 2 → 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
intro xp xh
State after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 / (1 - x) ≤ 1 + 2 * x

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
have x1 : 1 - x > 0 := by linarith
State after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 / (1 - x) ≤ 1 + 2 * x

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 / (1 - x) ≤ 1 + 2 * x
Tactic:
rw [div_le_iff x1]
State after:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 ≤ (1 + 2 * x) * (1 - x)

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 ≤ (1 + 2 * x) * (1 - x)
Tactic:
calc (1 + 2*x) * (1 - x) = 1 + x * (1 - 2*x) := by ring
  _ ≥ 1 + x * (1 - 2 * (1/2)) := by bound
  _ = 1 := by ring
State after:
no goals

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
⊢ 1 - x > 0
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ (1 + 2 * x) * (1 - x) = 1 + x * (1 - 2 * x)
Tactic:
ring
State after:
no goals

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 + x * (1 - 2 * x) ≥ 1 + x * (1 - 2 * (1 / 2))
Tactic:
bound
State after:
no goals

State before:
x : ℝ
xp : 0 ≤ x
xh : x ≤ 1 / 2
x1 : 1 - x > 0
⊢ 1 + x * (1 - 2 * (1 / 2)) = 1
Tactic:
ring
State after:
no goals