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)
⊢ 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
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ (fun t => f (t, w.2)) t ∈ ball (f (z.1, w.2)) (3 * b)
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)
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]
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2) - f (z.1, w.2)‖ < 3 * b
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)
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 _ _)
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)
t : ℂ
ts : t ∈ ball z.1 (r / 2)
⊢ ‖f (t, w.2)‖ + ‖f (z.1, w.2)‖ < 3 * b
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)
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]
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)
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
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)
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]
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)
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
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)
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
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
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]
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
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]
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
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
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
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
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
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
Proof state after:
no goals
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
have wrs : ball w (r / 2) ⊆ s := by
  refine _root_.trans ?_ rs; apply Metric.ball_subset_ball'
  have rr := _root_.trans wz.le (min_le_left _ _)
  trans r / 2 + r / 2; linarith; ring_nf; apply le_refl
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
have rs' : ball (swap w) (r / 2) ⊆ swap '' s := by rw [ball_swap]; exact Set.image_subset _ wrs
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
have wz' : dist (swap z) (swap w) < min (r / 2) (e * r / b / 24) := by rwa [dist_swap, 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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
have fb' : ∀ z, z ∈ swap '' s → ‖(f ∘ swap) z‖ ≤ b := fun z zs ↦ fb z.swap (swap_mem'.mp zs)
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
have d' := Bounded.dist0 h.flip bp ep rp rs' wz' fb'
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
d' : dist ((f ∘ swap) z.swap) ((f ∘ swap) (w.swap.1, z.swap.2)) ≤ e / 4
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
d' : dist ((f ∘ swap) z.swap) ((f ∘ swap) (w.swap.1, z.swap.2)) ≤ e / 4
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
simp only [Function.comp_apply, Prod.swap_swap, Prod.fst_swap, Prod.snd_swap,
  Prod.swap_prod_mk] at d'
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
d' : dist (f z) (f (z.1, w.2)) ≤ e / 4
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
wrs : ball w (r / 2) ⊆ s
rs' : ball w.swap (r / 2) ⊆ swap '' s
wz' : dist z.swap w.swap < min (r / 2) (e * r / b / 24)
fb' : ∀ z ∈ swap '' s, ‖(f ∘ swap) z‖ ≤ b
d' : dist (f z) (f (z.1, w.2)) ≤ e / 4
⊢ dist (f (z.1, w.2)) (f z) ≤ e / 4
Tactic:
rwa [dist_comm]
Proof state after:
no goals
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ ball w (r / 2) ⊆ s
Tactic:
refine _root_.trans ?_ rs
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ ball w (r / 2) ⊆ ball z r
Theorem: Bounded.dist1
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ ball w (r / 2) ⊆ ball z r
Tactic:
apply Metric.ball_subset_ball'
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ r / 2 + dist w z ≤ r
Theorem: Bounded.dist1
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
⊢ r / 2 + dist w z ≤ r
Tactic:
have rr := _root_.trans wz.le (min_le_left _ _)
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + dist w z ≤ r
Theorem: Bounded.dist1
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 s
z w : ℂ × ℂ
b e r : ℝ
bp : 0 < b
ep : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + dist w z ≤ r
Tactic:
trans r / 2 + r / 2
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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + dist w z ≤ r / 2 + r / 2

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : 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 : e > 0
rp : r > 0
rs : ball z r ⊆ s
wz : dist w z < min (r / 2) (e * r / b / 24)
fb : ∀ z ∈ s, ‖f z‖ ≤ b
rr : dist w z ≤ r / 2
⊢ r / 2 + r / 2 ≤ r