internlm/Lean-Github huggingface dataset:
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have m : Set.MapsTo (fun t ↦ f (t, w.snd)) (ball z.fst (r / 2))
    (ball (f (z.fst, w.snd)) (3 * b)) := by
  intro t ts; simp only [dist_eq_norm, Metric.mem_ball]; apply lt_of_le_of_lt (norm_sub_le _ _)
  have f0 : ‖f (t, w.snd)‖ ≤ b := by
    apply_rules [rs, Set.mk_mem_prod, Metric.ball_subset_ball ur, fb, wz.right]
  have f1 : ‖f (z.fst, w.snd)‖ ≤ b := by
    apply_rules [rs, Set.mk_mem_prod, Metric.ball_subset_ball ur, fb, Metric.mem_ball_self up,
      wz.right]
  calc ‖f (t, w.snd)‖ + ‖f (z.fst, w.snd)‖
    _ ≤ b + b := by linarith
    _ = 2 * b := by ring
    _ < 3 * b := mul_lt_mul_of_pos_right (by norm_num) bp
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have L := Complex.dist_le_div_mul_dist_of_mapsTo_ball d m wf
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f (w.1, w.2)) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f (w.1, w.2)) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
simp only [Prod.mk.eta] at L
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
refine _root_.trans L (_root_.trans ?_ ue)
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ 3 * b / (r / 2) * dist w.1 z.1 ≤ 6 * b / r * u
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
⊢ 3 * b / (r / 2) * dist w.1 z.1 ≤ 6 * b / r * u
Tactic:
simp only [Metric.mem_ball] at wz
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ 3 * b / (r / 2) * dist w.1 z.1 ≤ 6 * b / r * u
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ 3 * b / (r / 2) * dist w.1 z.1 ≤ 6 * b / r * u
Tactic:
rw [div_eq_mul_inv _ (2 : ℝ), div_mul_eq_div_div]
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ 3 * b / r / 2⁻¹ * dist w.1 z.1 ≤ 6 * b / r * u
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ 3 * b / r / 2⁻¹ * dist w.1 z.1 ≤ 6 * b / r * u
Tactic:
ring_nf
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ b * r⁻¹ * dist w.1 z.1 * 6 ≤ b * r⁻¹ * u * 6
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
d : DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
wf : w.1 ∈ ball z.1 (r / 2)
m : Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
L : dist (f w) (f (z.1, w.2)) ≤ 3 * b / (r / 2) * dist w.1 z.1
wz : dist w.1 z.1 < u ∧ dist w.2 z.2 < u
⊢ b * r⁻¹ * dist w.1 z.1 * 6 ≤ b * r⁻¹ * u * 6
Tactic:
bound
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < u
Tactic:
rw [← hu]
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < min (r / 2) (e * r / b / 24)
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < min (r / 2) (e * r / b / 24)
Tactic:
simp only [gt_iff_lt, lt_min_iff]
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < r / 2 ∧ 0 < e * r / b / 24
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < r / 2 ∧ 0 < e * r / b / 24
Tactic:
exact ⟨by bound, by bound⟩
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < r / 2
Tactic:
bound
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
⊢ 0 < e * r / b / 24
Tactic:
bound
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
⊢ u ≤ r / 2
Tactic:
rw [← hu]
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
⊢ min (r / 2) (e * r / b / 24) ≤ r / 2
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
⊢ min (r / 2) (e * r / b / 24) ≤ r / 2
Tactic:
exact min_le_left _ _
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ 6 * b / r * u ≤ e / 4
Tactic:
rw [← hu]
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ 6 * b / r * min (r / 2) (e * r / b / 24) ≤ e / 4
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ 6 * b / r * min (r / 2) (e * r / b / 24) ≤ e / 4
Tactic:
calc 6 * b / r * min (r / 2) (e * r / b / 24)
  _ ≤ 6 * b / r * (e * r / b / 24) := by bound
  _ = b / b * (r / r) * (e / 4) := by ring
  _ = e / 4 := by field_simp [bp.ne', rp.ne']
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ 6 * b / r * min (r / 2) (e * r / b / 24) ≤ 6 * b / r * (e * r / b / 24)
Tactic:
bound
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ 6 * b / r * (e * r / b / 24) = b / b * (r / r) * (e / 4)
Tactic:
ring
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
⊢ b / b * (r / r) * (e / 4) = e / 4
Tactic:
field_simp [bp.ne', rp.ne']
Proof state after:
no goals
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ DifferentiableOn ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2))
Tactic:
intro t ts
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ DifferentiableWithinAt ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2)) t
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ DifferentiableWithinAt ℂ (fun t => f (t, w.2)) (ball z.1 (r / 2)) t
Tactic:
refine (h.fa0 t w.snd ?_).differentiableWithinAt
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ (t, w.2) ∈ s
Theorem: Bounded.dist0
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z.1 (r / 2) ×ˢ ball z.2 (r / 2) ⊆ s
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
wz : w.1 ∈ ball z.1 u ∧ w.2 ∈ ball z.2 u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ (t, w.2) ∈ s
Tactic:
exact rs (Set.mk_mem_prod ts (Metric.ball_subset_ball ur wz.right))
Proof state after:
no goals