internlm/Lean-Github huggingface dataset:
Theorem: diam_ball_eq
Proof 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
Proof 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✝
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof 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
Theorem: diam_ball_eq
Proof 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]
Proof 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
Theorem: diam_ball_eq
Proof 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]
Proof 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
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof 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)
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof 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
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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
Proof 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
Theorem: diam_ball_eq
Proof 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
Proof 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
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof 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)
Theorem: diam_ball_eq
Proof 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
Proof state after:
no goals
Theorem: diam_ball_eq
Proof 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]
Proof state after:
no goals
Theorem: diam_closedBall_eq
Proof 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 (closedBall c r) = 2 * r
Tactic:
apply le_antisymm (Metric.diam_closedBall rp)
Proof 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
⊢ 2 * r ≤ Metric.diam (closedBall c r)
Theorem: diam_closedBall_eq
Proof 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
⊢ 2 * r ≤ Metric.diam (closedBall c r)
Tactic:
trans Metric.diam (ball c r)
Proof 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
⊢ 2 * r ≤ Metric.diam (ball c r)

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) ≤ Metric.diam (closedBall c r)
Theorem: diam_closedBall_eq
Proof 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
⊢ 2 * r ≤ Metric.diam (ball c r)

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) ≤ Metric.diam (closedBall c r)
Tactic:
rw [diam_ball_eq rp]
Proof 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
⊢ Metric.diam (ball c r) ≤ Metric.diam (closedBall c r)
Theorem: diam_closedBall_eq
Proof 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) ≤ Metric.diam (closedBall c r)
Tactic:
exact Metric.diam_mono Metric.ball_subset_closedBall Metric.isBounded_closedBall
Proof state after:
no goals
Theorem: le_of_ball_subset_closedBall
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
⊢ ball z0 r0 ⊆ closedBall z1 r1 → r0 ≤ r1
Tactic:
intro s
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
⊢ r0 ≤ r1
Theorem: le_of_ball_subset_closedBall
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
⊢ r0 ≤ r1
Tactic:
have m := Metric.diam_mono s Metric.isBounded_closedBall
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : Metric.diam (ball z0 r0) ≤ Metric.diam (closedBall z1 r1)
⊢ r0 ≤ r1
Theorem: le_of_ball_subset_closedBall
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : Metric.diam (ball z0 r0) ≤ Metric.diam (closedBall z1 r1)
⊢ r0 ≤ r1
Tactic:
rw [diam_ball_eq r0p, diam_closedBall_eq r1p] at m
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : 2 * r0 ≤ 2 * r1
⊢ r0 ≤ r1
Theorem: le_of_ball_subset_closedBall
Proof 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 : ℝ
z0 z1 : ℂ
r0 r1 : ℝ
r0p : r0 ≥ 0
r1p : r1 ≥ 0
s : ball z0 r0 ⊆ closedBall z1 r1
m : 2 * r0 ≤ 2 * r1
⊢ r0 ≤ r1
Tactic:
linarith
Proof state after:
no goals
Theorem: to_uneven
Proof 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have r4p : r / 4 > 0 := by linarith
Proof 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Theorem: to_uneven
Proof 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
rcases on_subdisk h rp r4p with ⟨c0', r0, r0p, m, a⟩
Proof state after:
case intro.intro.intro.intro
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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
m : c0' ∈ closedBall c0 (r / 4)
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1