Theorem: Bounded.dist0 (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✝ : ℝ
h : Har f s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : 0 < e
rp : 0 < r
rs : ball z (r / 2) ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
generalize hu : min (r / 2) (e * r / b / 24) = u
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
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
u : ℝ
hu : min (r / 2) (e * r / b / 24) = u
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [hu] at wz
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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have up : 0 < u := by
  rw [← hu]; simp only [gt_iff_lt, lt_min_iff]
  exact ⟨by bound, by bound⟩
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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have ur : u ≤ r / 2 := by rw [← hu]; exact min_le_left _ _
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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have ue : 6 * b / r * u ≤ e / 4 := by
  rw [← hu]
  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']
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
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [ball_prod_same'] at rs
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 : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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 : dist w z < u
hu : min (r / 2) (e * r / b / 24) = u
up : 0 < u
ur : u ≤ r / 2
ue : 6 * b / r * u ≤ e / 4
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
rw [← Metric.mem_ball, ball_prod_same', Set.mem_prod] at wz
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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have d : DifferentiableOn ℂ (fun t ↦ f (t, w.snd)) (ball z.fst (r / 2)) := by
  intro t ts; refine (h.fa0 t w.snd ?_).differentiableWithinAt
  exact rs (Set.mk_mem_prod ts (Metric.ball_subset_ball ur wz.right))
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))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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))
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4
Tactic:
have wf : w.fst ∈ ball z.fst (r / 2) := Metric.ball_subset_ball ur wz.left
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)
⊢ dist (f w) (f (z.1, w.2)) ≤ e / 4

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
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

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
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

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
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

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)
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

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
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

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]
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

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
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

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
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✝ : ℝ
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]
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)

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]
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

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⟩
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✝ : ℝ
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
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✝ : ℝ
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
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✝ : ℝ
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]
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

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 _ _
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✝ : ℝ
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]
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

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']
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✝ : ℝ
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
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✝ : ℝ
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
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✝ : ℝ
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']
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✝ : ℝ
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
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

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
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

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))
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✝ : ℝ
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)
⊢ Set.MapsTo (fun t => f (t, w.2)) (ball z.1 (r / 2)) (ball (f (z.1, w.2)) (3 * b))
Tactic:
intro t ts
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ (fun t => f (t, w.2)) t ∈ ball (f (z.1, w.2)) (3 * b)

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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ (fun t => f (t, w.2)) t ∈ ball (f (z.1, w.2)) (3 * b)
Tactic:
simp only [dist_eq_norm, Metric.mem_ball]
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2) - f (z.1, w.2)‖ < 3 * b

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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2) - f (z.1, w.2)‖ < 3 * b
Tactic:
apply lt_of_le_of_lt (norm_sub_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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b

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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b
Tactic:
have f0 : ‖f (t, w.snd)‖ ≤ b := by
  apply_rules [rs, Set.mk_mem_prod, Metric.ball_subset_ball ur, fb, wz.right]
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b

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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b
Tactic:
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]
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
f1 : ‖f (z.1, w.2)‖ ≤ b
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b

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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
f1 : ‖f (z.1, w.2)‖ ≤ b
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b
Tactic:
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
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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2)‖ ≤ b
Tactic:
apply_rules [rs, Set.mk_mem_prod, Metric.ball_subset_ball ur, fb, wz.right]
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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
⊢ ‖f (z.1, w.2)‖ ≤ b
Tactic:
apply_rules [rs, Set.mk_mem_prod, Metric.ball_subset_ball ur, fb, Metric.mem_ball_self up,
  wz.right]
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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
f1 : ‖f (z.1, w.2)‖ ≤ b
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ ≤ b + b
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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
f1 : ‖f (z.1, w.2)‖ ≤ b
⊢ b + b = 2 * b
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✝ : ℝ
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
f0 : ‖f (t, w.2)‖ ≤ b
f1 : ‖f (z.1, w.2)‖ ≤ b
⊢ 2 < 3
Tactic:
norm_num
State after:
no goals