Theorem: unevenSeries_uniform_bound (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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
rcases (((isCompact_sphere _ _).prod (isCompact_closedBall _ _)).bddAbove_image
  fc.norm).exists_ge 0 with ⟨b, bp, fb⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ y ∈ (fun x => ‖f x‖) '' sphere c0 (r0 / 2) ×ˢ closedBall c1 s, y ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ y ∈ (fun x => ‖f x‖) '' sphere c0 (r0 / 2) ×ˢ closedBall c1 s, y ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
simp only [Set.forall_mem_image] at fb
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∃ c a, c > 0 ∧ a > 0 ∧ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
Tactic:
use b + 1, (r0 / 2)⁻¹, lt_of_le_of_lt bp (lt_add_one _), inv_pos.mpr (half_pos u.r0p)
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
intro n z1 z1s
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have r0hp : r0 / 2 > 0 := by linarith [u.r0p]
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have r0hr1 : r0 / 2 ≤ r1 := _root_.trans (by linarith [u.r0p]) u.r01
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
set g := fun z0 ↦ f (z0, z1)
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have gc : ContinuousOn g (sphere c0 (r0 / 2)) :=
  ContinuousOn.comp fc (ContinuousOn.prod continuousOn_id continuousOn_const) fun z0 z0s ↦
    Set.mk_mem_prod z0s z1s
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have gb : ∀ z0, z0 ∈ sphere c0 (r0 / 2) → ‖g z0‖ ≤ b := fun z0 z0s ↦ fb (Set.mk_mem_prod z0s z1s)
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have cb := cauchy1_bound' r0hp b gc gb n
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
gc : ContinuousOn g (sphere c0 (r0 / 2))
gb : ∀ z0 ∈ sphere c0 (r0 / 2), ‖g z0‖ ≤ b
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
clear bp gc gb
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
have e : (2 * π * I : ℂ)⁻¹ • (∮ z0 in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) =
    unevenTerm' u (r0 / 2) z1 n := rfl
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e✝ : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
e : ((2 * ↑π * I)⁻¹ • ∮ (z0 : ℂ) in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) = unevenTerm' u (r0 / 2) z1 n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e✝ : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r0 / 2), (z - c0)⁻¹ ^ n • (z - c0)⁻¹ • g z‖ ≤ b * (r0 / 2)⁻¹ ^ n
e : ((2 * ↑π * I)⁻¹ • ∮ (z0 : ℂ) in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) = unevenTerm' u (r0 / 2) z1 n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
rw [e] at cb
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e✝ : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
e : ((2 * ↑π * I)⁻¹ • ∮ (z0 : ℂ) in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) = unevenTerm' u (r0 / 2) z1 n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e✝ : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
g : ℂ → E := fun z0 => f (z0, z1)
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
e : ((2 * ↑π * I)⁻¹ • ∮ (z0 : ℂ) in C(c0, r0 / 2), (z0 - c0)⁻¹ ^ n • (z0 - c0)⁻¹ • g z0) = unevenTerm' u (r0 / 2) z1 n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
clear e g
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm' u (r0 / 2) z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
rw [unevenTerm_eq u r0hp r0hr1 (Metric.closedBall_subset_closedBall sr.le z1s)] at cb
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenSeries u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
rw [unevenSeries_norm u]
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenTerm u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ ‖unevenTerm u z1 n‖ ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
Tactic:
apply _root_.trans cb
State after:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ b * (r0 / 2)⁻¹ ^ n ≤ (b + 1) * (r0 / 2)⁻¹ ^ n

State before:
case right
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b✝ e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
r0hr1 : r0 / 2 ≤ r1
cb : ‖unevenTerm u z1 n‖ ≤ b * (r0 / 2)⁻¹ ^ n
⊢ b * (r0 / 2)⁻¹ ^ n ≤ (b + 1) * (r0 / 2)⁻¹ ^ n
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
suffices fa' : AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s) by exact fa'.continuousOn
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
refine u.a.mono (Set.prod_mono ?_ ?_)
State after:
case refine_1
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0

case refine_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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ closedBall c1 s ⊆ ball c1 r1

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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fa' : AnalyticOn ℂ f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
⊢ ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
Tactic:
exact fa'.continuousOn
State after:
no goals

State before:
case refine_1
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0
Tactic:
have rh : r0 / 2 < r0 := by linarith [u.r0p]
State after:
case refine_1
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
rh : r0 / 2 < r0
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0

State before:
case refine_1
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
rh : r0 / 2 < r0
⊢ sphere c0 (r0 / 2) ⊆ ball c0 r0
Tactic:
exact _root_.trans Metric.sphere_subset_closedBall (Metric.closedBall_subset_ball rh)
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ r0 / 2 < r0
Tactic:
linarith [u.r0p]
State after:
no goals

State before:
case refine_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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ closedBall c1 s ⊆ ball c1 r1
Tactic:
exact Metric.closedBall_subset_ball (by linarith [u.r1p])
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
⊢ s < r1
Tactic:
linarith [u.r1p]
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
⊢ r0 / 2 > 0
Tactic:
linarith [u.r0p]
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 : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
fc : ContinuousOn f (sphere c0 (r0 / 2) ×ˢ closedBall c1 s)
b : ℝ
bp : 0 ≤ b
fb : ∀ ⦃x : ℂ × ℂ⦄, x ∈ sphere c0 (r0 / 2) ×ˢ closedBall c1 s → ‖f x‖ ≤ b
n : ℕ
z1 : ℂ
z1s : z1 ∈ closedBall c1 s
r0hp : r0 / 2 > 0
⊢ r0 / 2 ≤ r0
Tactic:
linarith [u.r0p]
State after:
no goals