Theorem: test_try_elab (Ray/Tactic/BoundTests.lean)

State before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs w + e
Tactic:
calc abs (f z) = abs (f w - (f w - f z)) := by ring_nf
  _ ≤ abs (f w) + abs (f w - f z) := by bound
  _ ≤ c * abs w + e := by bound [h w wr, sc wz]
State after:
no goals

State before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) = Complex.abs (f w - (f w - f z))
Tactic:
ring_nf
State after:
no goals

State before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f w - (f w - f z)) ≤ Complex.abs (f w) + Complex.abs (f w - f z)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
z w : ℂ
s r c e : ℝ
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
wz : Complex.abs (w - z) < s
wr : Complex.abs w < r
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f w) + Complex.abs (f w - f z) ≤ c * Complex.abs w + e
Tactic:
bound [h w wr, sc wz]
State after:
no goals