awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ C / (C / ε) = ε

Tactic:
div_div_cancel₀ C₀.lt.ne'

Premises used: GT.gt.lt, LT.lt.ne', div_div_cancel₀
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ ε

Tactic:
calc
    ‖deriv f c‖ ≤ C / (C / ε) :=
      norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.diffContOnCl fun z _ => hC z
    _ = ε := div_div_cancel₀ C₀.lt.ne'

Premises used: Differentiable.diffContOnCl, deriv, GT.gt.lt, HDiv.hDiv, LT.lt.ne', div_div_cancel₀, Complex.norm_deriv_le_of_forall_mem_sphere_norm_le, div_pos
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
this : g 0 = g 1
⊢ f z = f w

Tactic:
simpa [g]
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
suffices : g 0 = g 1
⊢ f z = f w

Tactic:
suffices g 0 = g 1 by simpa [g]
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
hf₁ : Differentiable ℂ g
hb₁ : Bornology.IsBounded (range g)
⊢ g 0 = g 1

Tactic:
apply liouville_theorem_aux

Premises used: Complex.liouville_theorem_aux
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
⊢ Differentiable ℂ g

Tactic:
hf.comp ((differentiable_id.smul_const (w - z)).add_const z)

Premises used: HSub.hSub, Differentiable.add_const, Differentiable.comp, Differentiable.smul_const
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
⊢ Bornology.IsBounded (range g)

Tactic:
hb.subset (range_comp_subset_range _ _)

Premises used: Set.range_comp_subset_range, Bornology.IsBounded.subset
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
⊢ Differentiable ℂ g

Tactic:
exacts [hf.comp ((differentiable_id.smul_const (w - z)).add_const z),
    hb.subset (range_comp_subset_range _ _)]

Premises used: Set.range_comp_subset_range, HSub.hSub, Bornology.IsBounded.subset, Differentiable.add_const, Differentiable.comp, Differentiable.smul_const
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
⊢ ∃ (c : F), ∀ (z : E), f z = c

Tactic:
⟨f 0, fun _ => hf.apply_eq_apply_of_bounded hb _ _⟩

Premises used: Differentiable.apply_eq_apply_of_bounded, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
⊢ ∃ (c : F), f = const E c

Tactic:
(hf.exists_const_forall_eq_of_bounded hb).imp fun _ => funext

Premises used: Exists.imp, funext, Differentiable.exists_const_forall_eq_of_bounded
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
obtain : ∀ (s : Set E) (hs : s ∈ cocompact E) (hs_bdd : Bornology.IsBounded (f '' s)), Bornology.IsBounded (range f)
⊢ Bornology.IsBounded (range f)

Tactic:
obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb

Premises used: Metric.exists_isBounded_image_of_tendsto
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
obtain : ∀ (t : Set E) (ht : IsCompact t) (hts : tᶜ ⊆ s), Bornology.IsBounded (range f)
⊢ Bornology.IsBounded (range f)

Tactic:
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs

Premises used: Iff.mp, Filter.mem_cocompact
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
apply : range f ⊆ f '' t ∪ f '' s
⊢ Bornology.IsBounded (range f)

Tactic:
apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset

Premises used: IsCompact.isBounded, Bornology.IsBounded.subset, IsCompact.image, Differentiable.continuous, Bornology.IsBounded.union
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ t ∪ tᶜ ⊆ t ∪ s

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ range f ⊆ f '' t ∪ f '' s

Tactic:
simpa [Set.image_union, Set.image_univ] using Set.image_mono <| calc
      Set.univ = t ∪ tᶜ := t.union_compl_self.symm
      _        ⊆ t ∪ s  := by gcongr

Premises used: Set.image_univ, Set.univ, Set.image_mono, Set.union_compl_self, Eq.symm, Set.image_union
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ Bornology.IsBounded (range f)

Tactic:
have h_bdd : Bornology.IsBounded (Set.range f) := by
    obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb
    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
    apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset
    simpa [Set.image_union, Set.image_univ] using Set.image_mono <| calc
      Set.univ = t ∪ tᶜ := t.union_compl_self.symm
      _        ⊆ t ∪ s  := by gcongr
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
obtain : ∀ (c' : F) (hc' : f = const E c'), f = const E c
⊢ f = const E c

Tactic:
obtain ⟨c', hc'⟩ := hf.exists_eq_const_of_bounded h_bdd

Premises used: Differentiable.exists_eq_const_of_bounded
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c'

Tactic:
hc'
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
h : c = c'
⊢ f = const E c

Tactic:
convert! hc'
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ Tendsto f (cocompact E) (𝓝 c')

Tactic:
simpa [hc'] using tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ c = c'

Tactic:
exact tendsto_nhds_unique hb (by simpa [hc'] using tendsto_const_nhds)

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
x : E
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ f x = c

Tactic:
congr($(hf.eq_const_of_tendsto_cocompact hb) x)

Premises used: id, congrFun, Differentiable.eq_const_of_tendsto_cocompact
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
r : ℝ
f : ℂ → E
inst_2 : CompleteSpace E
hU : IsOpen U
hf : DifferentiableOn ℂ f U
hr : 0 < r
hzr : closedBall z r ⊆ U
⊢ cderiv r f z = deriv f z

Tactic:
two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable hU hzr hf (mem_ball_self hr)

Premises used: Complex.cderiv, Metric.mem_ball_self, Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
⊢ (sphere z r).Nonempty

Tactic:
NormedSpace.sphere_nonempty.mpr hr.le

Premises used: Iff.mpr, LT.lt.le, NormedSpace.sphere_nonempty
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
obtain : ∀ (w : ℂ) (hw : w ∈ sphere z r), 0 ≤ M
⊢ 0 ≤ M

Tactic:
obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le

Premises used: Iff.mpr, LT.lt.le, Set.Nonempty, NormedSpace.sphere_nonempty, Metric.sphere
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ 0 ≤ M

Tactic:
(norm_nonneg _).trans (hf w hw)

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ 0 ≤ M

Tactic:
exact (norm_nonneg _).trans (hf w hw)

Premises used: LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
⊢ 0 ≤ M

Tactic:
have hM : 0 ≤ M := by
    obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
    exact (norm_nonneg _).trans (hf w hw)
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ ‖w - z‖ = r

Tactic:
simp only [mem_sphere_iff_norm] at hw hf

Premises used: mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
hw₁ : ‖w - z‖ = r
⊢ ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M

Tactic:
simp only [mem_sphere_iff_norm] at hw hf

Premises used: mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hM : 0 ≤ M
w : ℂ
hw : ‖w - z‖ = r
hf : ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M
simp : ‖f w‖ / HPow.hPow (β := ℕ) r 2 ≤ M / HPow.hPow (β := ℕ) r 2
⊢ ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2

Tactic:
simp only [norm_smul, inv_mul_eq_div, hw, norm_inv, norm_pow]

Premises used: norm_smul, norm_pow, inv_mul_eq_div, norm_inv
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hM : 0 ≤ M
w : ℂ
hw : ‖w - z‖ = r
hf : ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M
⊢ ‖f w‖ / HPow.hPow (β := ℕ) r 2 ≤ M / HPow.hPow (β := ℕ) r 2

Tactic:
div_le_div₀ hM (hf w hw) (sq_pos_of_pos hr) le_rfl

Premises used: div_le_div₀, le_rfl, sq_pos_of_pos
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hM : 0 ≤ M
w : ℂ
hw : ‖w - z‖ = r
hf : ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M
⊢ ‖f w‖ / HPow.hPow (β := ℕ) r 2 ≤ M / HPow.hPow (β := ℕ) r 2

Tactic:
exact div_le_div₀ hM (hf w hw) (sq_pos_of_pos hr) le_rfl

Premises used: div_le_div₀, le_rfl, sq_pos_of_pos
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2

Tactic:
have h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2 := by
    intro w hw
    simp only [mem_sphere_iff_norm] at hw hf
    simp only [norm_smul, inv_mul_eq_div, hw, norm_inv, norm_pow]
    exact div_le_div₀ hM (hf w hw) (sq_pos_of_pos hr) le_rfl
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
⊢ norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)

Tactic:
have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
simp :
  ‖(2 * (↑π : ℂ) * I)⁻¹‖ * norm.{u_1} (E := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w) ≤ M / r
⊢ ‖cderiv r f z‖ ≤ M / r

Tactic:
simp only [cderiv, norm_smul]

Premises used: norm_smul, Complex.cderiv
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ * norm.{u_1} (E := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w) ≤ M / r

Tactic:
(mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq ?_)

Premises used: le_rfl, mul_le_mul, LE.le.trans, le_of_eq, norm_nonneg
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
refine : ‖(2 * (↑π : ℂ) * I)⁻¹‖ * (2 * π * r * (M / HPow.hPow (β := ℕ) r 2)) = M / r
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ * norm.{u_1} (E := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w) ≤ M / r

Tactic:
refine (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq ?_)

Premises used: le_rfl, mul_le_mul, LE.le.trans, le_of_eq, norm_nonneg
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ * (2 * π * r * (M / HPow.hPow (β := ℕ) r 2)) = M / r

Tactic:
simp [field, abs_of_nonneg Real.pi_pos.le]

Premises used: Real.pi_pos, LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)

Tactic:
((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_

Premises used: Continuous.continuousOn, continuous_const, continuous_id', Continuous.pow, ContinuousOn.inv₀, OfNat.ofNat, Continuous.sub, LT.lt.ne
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
refine : ∀ (w : ℂ) (hw : w ∈ sphere z r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)

Tactic:
refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_

Premises used: Continuous.continuousOn, continuous_const, continuous_id', Continuous.pow, ContinuousOn.inv₀, OfNat.ofNat, Continuous.sub, LT.lt.ne
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : HPow.hPow (β := ℕ) (w - z) 2 = 0
rwa : ∀ (hw : ‖w - z‖ = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
rwa₁ : ∀ (hw : norm (E := ℂ) 0 = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hw : 0 = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
⊢ 0 = r

Tactic:
rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw

Premises used: norm_zero, mem_sphere_iff_norm, Iff.mp, sq_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)

Tactic:
have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) := by
    refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_
    rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
simp_rw :
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
        (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z

Tactic:
simp_rw [cderiv, ← smul_sub]

Premises used: Complex.cderiv, smul_sub
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
e_a :
  ∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w =
    HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
      (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
        (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
⊢ ∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w =
    HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
      (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)

Tactic:
simpa only [Pi.sub_apply, smul_sub] using
    circleIntegral.integral_sub ((h1.smul hf).circleIntegrable hr.le)
      ((h1.smul hg).circleIntegrable hr.le)

Premises used: ContinuousOn.circleIntegrable, LT.lt.le, circleIntegral.integral_sub, smul_sub, ContinuousOn.smul, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.LocallyUniformLimit
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ (sphere z r).Nonempty

Tactic:
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le