internlm/Lean-Github huggingface dataset:
Theorem: to_uneven
Proof state before:
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
Tactic:
simp only [Metric.mem_closedBall] at m
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have sub : closedBall c0' (r / 2) ⊆ closedBall c0 r := by
  apply Metric.closedBall_subset_closedBall'
  calc
    r / 2 + dist c0' c0 ≤ r / 2 + r / 4 := by linarith
    _ = 3 / 4 * r := by ring
    _ ≤ 1 * r := by linarith
    _ = r := by ring
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have r01 : min r0 (r / 2) ≤ r / 2 := by bound
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have c0m : c0 ∈ ball c0' (r / 2) := by
  simp only [Metric.mem_ball]; rw [dist_comm]; apply lt_of_le_of_lt m; bound
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have h' : Har f (closedBall (c0', c1) (r / 2)) := by
  refine Har.mono ?_ h; simp only [← closedBall_prod_same]; apply Set.prod_mono
  assumption; apply Metric.closedBall_subset_closedBall; linarith
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
have a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2)) := by
  apply a.mono; apply Set.prod_mono
  apply Metric.ball_subset_ball'
  simp only [dist_self, add_zero, min_le_iff, le_refl, true_or_iff]
  apply Metric.ball_subset_ball; linarith
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ ∃ 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:
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ ∃ c0' r0 r1, ball c0' r1 ⊆ closedBall c0 r ∧ c0 ∈ ball c0' r1 ∧ Uneven f c0' c1 r0 r1
Tactic:
use c0', min r0 (r / 2), r / 2, _root_.trans Metric.ball_subset_closedBall sub, c0m
Proof state after:
case right
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ Uneven f c0' c1 (min r0 (r / 2)) (r / 2)
Theorem: to_uneven
Proof state before:
case right
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ Uneven f c0' c1 (min r0 (r / 2)) (r / 2)
Tactic:
exact
  { r0p := by bound
    r1p := by bound
    r01
    h := h'
    a := a' }
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
⊢ r / 4 > 0
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ closedBall c0' (r / 2) ⊆ closedBall c0 r
Tactic:
apply Metric.closedBall_subset_closedBall'
Proof state after:
case h
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ r / 2 + dist c0' c0 ≤ r
Theorem: to_uneven
Proof state before:
case h
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ r / 2 + dist c0' c0 ≤ r
Tactic:
calc
  r / 2 + dist c0' c0 ≤ r / 2 + r / 4 := by linarith
  _ = 3 / 4 * r := by ring
  _ ≤ 1 * r := by linarith
  _ = r := by ring
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ r / 2 + dist c0' c0 ≤ r / 2 + r / 4
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ r / 2 + r / 4 = 3 / 4 * r
Tactic:
ring
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ 3 / 4 * r ≤ 1 * r
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
⊢ 1 * r = r
Tactic:
ring
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
⊢ min r0 (r / 2) ≤ r / 2
Tactic:
bound
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ c0 ∈ ball c0' (r / 2)
Tactic:
simp only [Metric.mem_ball]
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ dist c0 c0' < r / 2
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ dist c0 c0' < r / 2
Tactic:
rw [dist_comm]
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ dist c0' c0 < r / 2
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ dist c0' c0 < r / 2
Tactic:
apply lt_of_le_of_lt 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 : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ r / 4 < r / 2
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
⊢ r / 4 < r / 2
Tactic:
bound
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
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ Har f (closedBall (c0', c1) (r / 2))
Tactic:
refine Har.mono ?_ h
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall (c0', c1) (r / 2) ⊆ closedBall (c0, c1) r
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall (c0', c1) (r / 2) ⊆ closedBall (c0, c1) r
Tactic:
simp only [← closedBall_prod_same]
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c0' (r / 2) ×ˢ closedBall c1 (r / 2) ⊆ closedBall c0 r ×ˢ closedBall c1 r
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 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c0' (r / 2) ×ˢ closedBall c1 (r / 2) ⊆ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
apply Set.prod_mono
Proof state after:
case hs
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c0' (r / 2) ⊆ closedBall c0 r

case ht
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c1 (r / 2) ⊆ closedBall c1 r
Theorem: to_uneven
Proof state before:
case hs
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c0' (r / 2) ⊆ closedBall c0 r

case ht
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c1 (r / 2) ⊆ closedBall c1 r
Tactic:
assumption
Proof state after:
case ht
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
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c1 (r / 2) ⊆ closedBall c1 r