Theorem: diam_ball_eq (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
by_cases r0 : 0 = r
State after:
case pos
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : 0 = r
⊢ Metric.diam (ball c r) = 2 * r

case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
⊢ Metric.diam (ball c r) = 2 * r

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
have rp' := Ne.lt_of_le r0 rp
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : ¬0 = r
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
clear r0
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
apply le_antisymm (Metric.diam_ball rp)
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ 2 * r ≤ Metric.diam (ball c r)

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ 2 * r ≤ Metric.diam (ball c r)
Tactic:
apply le_of_forall_small_le_add rp'
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ ∀ (e : ℝ), 0 < e → e < r → 2 * r ≤ Metric.diam (ball c r) + e

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
⊢ ∀ (e : ℝ), 0 < e → e < r → 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
intro e ep er
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
⊢ 2 * r ≤ Metric.diam (ball c r) + e

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have m : ∀ t : ℝ, |t| ≤ 1 → c + t * (r - e / 2) ∈ ball c r := by
  intro t t1
  simp only [Complex.dist_eq, Metric.mem_ball, add_sub_cancel_left, AbsoluteValue.map_mul,
    Complex.abs_ofReal]
  have re : r - e / 2 ≥ 0 := by linarith [_root_.trans (half_lt_self ep) er]
  calc |t| * abs (↑r - ↑e / 2 : ℂ)
    _ = |t| * abs (↑(r - e / 2) : ℂ) := by
      simp only [Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_one]
      norm_num
    _ = |t| * (r - e / 2) := by rw [Complex.abs_ofReal, abs_of_nonneg re]
    _ ≤ 1 * (r - e / 2) := mul_le_mul_of_nonneg_right t1 re
    _ = r - e / 2 := by ring
    _ < r - 0 := (sub_lt_sub_left (by linarith) r)
    _ = r := by ring
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ 2 * r ≤ Metric.diam (ball c r) + e

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have lo :=
  Metric.dist_le_diam_of_mem Metric.isBounded_ball (m 1 (by norm_num)) (m (-1) (by norm_num))
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e
Tactic:
have e : abs (2 * ↑r - ↑e : ℂ) = 2 * r - e := by
  have re : 2 * r - e ≥ 0 := by trans r - e; linarith; simp only [sub_nonneg, er.le]
  calc abs (2 * ↑r - ↑e : ℂ)
    _ = abs (↑(2 * r - e) : ℂ) := by
      simp only [Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_one]
      norm_num
    _ = 2 * r - e := by rw [Complex.abs_ofReal, abs_of_nonneg re]
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e✝ / 2)) (c + ↑(-1) * (↑r - ↑e✝ / 2)) ≤ Metric.diam (ball c r)
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e✝ / 2)) (c + ↑(-1) * (↑r - ↑e✝ / 2)) ≤ Metric.diam (ball c r)
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
simp only [Complex.dist_eq, Complex.ofReal_one, one_mul, Complex.ofReal_neg, neg_mul, neg_sub,
  add_sub_add_left_eq_sub] at lo
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r - ↑e✝ / 2 - (↑e✝ / 2 - ↑r)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r - ↑e✝ / 2 - (↑e✝ / 2 - ↑r)) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
ring_nf at lo
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r * 2 - ↑e✝) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : Complex.abs (↑r * 2 - ↑e✝) ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
rw [mul_comm, e] at lo
State after:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : 2 * r - e✝ ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝

State before:
case neg
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝¹ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e✝ : ℝ
ep : 0 < e✝
er : e✝ < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e✝ / 2) ∈ ball c r
e : Complex.abs (2 * ↑r - ↑e✝) = 2 * r - e✝
lo : 2 * r - e✝ ≤ Metric.diam (ball c r)
⊢ 2 * r ≤ Metric.diam (ball c r) + e✝
Tactic:
linarith
State after:
no goals

State before:
case pos
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0✝ r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
r0 : 0 = r
⊢ Metric.diam (ball c r) = 2 * r
Tactic:
simp only [← r0, Metric.ball_zero, Metric.diam_empty, MulZeroClass.mul_zero]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
⊢ ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
Tactic:
intro t t1
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
⊢ c + ↑t * (↑r - ↑e / 2) ∈ ball c r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
⊢ c + ↑t * (↑r - ↑e / 2) ∈ ball c r
Tactic:
simp only [Complex.dist_eq, Metric.mem_ball, add_sub_cancel_left, AbsoluteValue.map_mul,
  Complex.abs_ofReal]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
⊢ |t| * Complex.abs (↑r - ↑e / 2) < r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
⊢ |t| * Complex.abs (↑r - ↑e / 2) < r
Tactic:
have re : r - e / 2 ≥ 0 := by linarith [_root_.trans (half_lt_self ep) er]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs (↑r - ↑e / 2) < r

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs (↑r - ↑e / 2) < r
Tactic:
calc |t| * abs (↑r - ↑e / 2 : ℂ)
  _ = |t| * abs (↑(r - e / 2) : ℂ) := by
    simp only [Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_one]
    norm_num
  _ = |t| * (r - e / 2) := by rw [Complex.abs_ofReal, abs_of_nonneg re]
  _ ≤ 1 * (r - e / 2) := mul_le_mul_of_nonneg_right t1 re
  _ = r - e / 2 := by ring
  _ < r - 0 := (sub_lt_sub_left (by linarith) r)
  _ = r := by ring
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
⊢ r - e / 2 ≥ 0
Tactic:
linarith [_root_.trans (half_lt_self ep) er]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs (↑r - ↑e / 2) = |t| * Complex.abs ↑(r - e / 2)
Tactic:
simp only [Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_one]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs (↑r - ↑e / 2) = |t| * Complex.abs (↑r - ↑e / ↑2)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs (↑r - ↑e / 2) = |t| * Complex.abs (↑r - ↑e / ↑2)
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ |t| * Complex.abs ↑(r - e / 2) = |t| * (r - e / 2)
Tactic:
rw [Complex.abs_ofReal, abs_of_nonneg re]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ 1 * (r - e / 2) = r - e / 2
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ 0 < e / 2
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
t : ℝ
t1 : |t| ≤ 1
re : r - e / 2 ≥ 0
⊢ r - 0 = r
Tactic:
ring
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ |1| ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
⊢ |(-1)| ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ Complex.abs (2 * ↑r - ↑e) = 2 * r - e
Tactic:
have re : 2 * r - e ≥ 0 := by trans r - e; linarith; simp only [sub_nonneg, er.le]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs (2 * ↑r - ↑e) = 2 * r - e

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs (2 * ↑r - ↑e) = 2 * r - e
Tactic:
calc abs (2 * ↑r - ↑e : ℂ)
  _ = abs (↑(2 * r - e) : ℂ) := by
    simp only [Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_one]
    norm_num
  _ = 2 * r - e := by rw [Complex.abs_ofReal, abs_of_nonneg re]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r - e ≥ 0
Tactic:
trans r - e
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r - e ≥ r - e

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ r - e ≥ 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ 2 * r - e ≥ r - e

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ r - e ≥ 0
Tactic:
linarith
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ r - e ≥ 0

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
⊢ r - e ≥ 0
Tactic:
simp only [sub_nonneg, er.le]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs (2 * ↑r - ↑e) = Complex.abs ↑(2 * r - e)
Tactic:
simp only [Complex.ofReal_sub, Complex.ofReal_mul, Complex.ofReal_one]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs (2 * ↑r - ↑e) = Complex.abs (↑2 * ↑r - ↑e)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs (2 * ↑r - ↑e) = Complex.abs (↑2 * ↑r - ↑e)
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e✝ : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
rp' : 0 < r
e : ℝ
ep : 0 < e
er : e < r
m : ∀ (t : ℝ), |t| ≤ 1 → c + ↑t * (↑r - ↑e / 2) ∈ ball c r
lo : dist (c + ↑1 * (↑r - ↑e / 2)) (c + ↑(-1) * (↑r - ↑e / 2)) ≤ Metric.diam (ball c r)
re : 2 * r - e ≥ 0
⊢ Complex.abs ↑(2 * r - e) = 2 * r - e
Tactic:
rw [Complex.abs_ofReal, abs_of_nonneg re]
State after:
no goals