Theorem: Bounded.dist1 (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 : 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
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

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

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

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

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

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

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

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

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

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

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
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
Tactic:
linarith
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 + r / 2 ≤ r

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
rr : dist w z ≤ r / 2
⊢ r / 2 + r / 2 ≤ r
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 : 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 ≤ r

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
rr : dist w z ≤ r / 2
⊢ r ≤ r
Tactic:
apply le_refl
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 : 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
⊢ ball w.swap (r / 2) ⊆ swap '' s
Tactic:
rw [ball_swap]
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
⊢ swap '' ball w (r / 2) ⊆ swap '' 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 : 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
⊢ swap '' ball w (r / 2) ⊆ swap '' s
Tactic:
exact Set.image_subset _ wrs
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 : 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 z.swap w.swap < min (r / 2) (e * r / b / 24)
Tactic:
rwa [dist_swap, dist_comm]
State after:
no goals