awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
w : ℂ
h : c = w → DifferentiableAt ℂ f c
⊢ Eq (α := UniformSpace.Completion E) (dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c w)
    (((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w)

Tactic:
rw [e.dslope_comp, Function.comp_apply]

Premises used: ContinuousLinearMap.dslope_comp, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ DifferentiableAt ℂ f c

Tactic:
hd.differentiableAt <| ball_mem_nhds _ h_R₁

Premises used: DifferentiableOn.differentiableAt, Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ DifferentiableAt ℂ f c

Tactic:
exact hd.differentiableAt <| ball_mem_nhds _ h_R₁

Premises used: DifferentiableOn.differentiableAt, Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c

Tactic:
have hg' : g = e ∘ dslope f c := by
    ext w
    simp only [g]
    rw [e.dslope_comp, Function.comp_apply]
    rintro rfl
    exact hd.differentiableAt <| ball_mem_nhds _ h_R₁
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z_1 : ℂ
hz_1 : z_1 ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
z : ℂ
hz : z ∈ ball c R₁
w : ℂ
hw : w ∈ ball c R₁
⊢ Membership.mem (γ := Set (UniformSpace.Completion E))
    (closedBall (((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c) R₂)
    (((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) w)

Tactic:
simpa [e] using h_maps hw
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
⊢ ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁

Tactic:
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
    norm_dslope_le_div_of_mapsTo_ball (e.differentiable.comp_differentiableOn hd)
      (fun w hw ↦ by simpa [e] using h_maps hw) hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z_1 : ℂ
hz_1 : z_1 ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ (norm ∘ g) z ≤ (norm ∘ g) z₀

Tactic:
simpa [h_eq, hg', e] using g_le_div z hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
⊢ IsMaxOn (norm ∘ g) (ball c R₁) z₀

Tactic:
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
    isMaxOn_iff.mpr fun z hz => by simpa [h_eq, hg', e] using g_le_div z hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
⊢ DifferentiableOn ℂ g (ball c R₁)

Tactic:
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
    (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr
      (e.differentiable.comp_differentiableOn hd)
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ ‖dslope f c z‖ = ‖dslope f c z₀‖

Tactic:
simpa [hg', e] using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
      isOpen_ball g_diff h_z₀ g_max hz

Premises used: convex_ball, Complex.norm_eqOn_of_isPreconnected_of_isMaxOn, Metric.isOpen_ball, Convex.isPreconnected
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ ‖dslope f c z‖ = ‖dslope f c z₀‖

Tactic:
have heq : ‖dslope f c z‖ = ‖dslope f c z₀‖ := by
    simpa [hg', e] using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
      isOpen_ball g_diff h_z₀ g_max hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
⊢ ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖

Tactic:
simpa [hg', e, ← UniformSpace.Completion.coe_add]
      using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
        isOpen_ball (g_diff.add_const (g z₀)) h_z₀ g_max.norm_add_self hz

Premises used: IsMaxOn.norm_add_self, DifferentiableOn.add_const, convex_ball, Complex.norm_eqOn_of_isPreconnected_of_isMaxOn, Metric.isOpen_ball, Convex.isPreconnected, UniformSpace.Completion.coe_add
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
⊢ ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖

Tactic:
have heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖ := by
    simpa [hg', e, ← UniformSpace.Completion.coe_add]
      using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
        isOpen_ball (g_diff.add_const (g z₀)) h_z₀ g_max.norm_add_self hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
⊢ ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z‖ + ‖dslope f c z₀‖

Tactic:
simp only [heq, SameRay.rfl.norm_add, heq_add]

Premises used: SameRay.norm_add, SameRay.rfl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
⊢ dslope f c z = dslope f c z₀

Tactic:
have : dslope f c z = dslope f c z₀ := eq_of_norm_eq_of_norm_add_eq heq <| by
    simp only [heq, SameRay.rfl.norm_add, heq_add]
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
this : dslope f c z = dslope f c z₀
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z

Tactic:
simp [← this]
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : ∃ z₀ ∈ ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁
⊢ ∃ (C : E), ‖C‖ = R₂ / R₁ ∧ EqOn f (fun (z : ℂ) ↦ f c + (z - c) • C) (ball c R₁)

Tactic:
let ⟨z₀, h_z₀, h_eq⟩ := h_z₀
  ⟨dslope f c z₀, h_eq, affine_of_mapsTo_ball_of_norm_dslope_eq_div hd h_maps h_z₀ h_eq⟩

Premises used: Norm.norm, HSub.hSub, Exists, HDiv.hDiv, Metric.ball, Set.EqOn, And, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, dslope, _private.0.Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'.match_1, Eq, Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div
-- Module: Mathlib.Analysis.Complex.Spectrum
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℂ A
a : A
⊢ SpectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔ ∀ x ∈ spectrum ℂ a, x = (↑x.re : ℂ)

Tactic:
simp [spectrumRestricts_iff, Set.LeftInvOn, Function.LeftInverse, eq_comm]

Premises used: spectrumRestricts_iff, Set.LeftInvOn, Function.LeftInverse, eq_comm
-- Module: Mathlib.Analysis.Complex.Spectrum
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : IsScalarTower ℂ A A
inst_3 : SMulCommClass ℂ A A
a : A
rw :
  SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
    ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
rw₁ :
  SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
    ∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)
rw₂ rw₃ :
  (∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)) ↔
    ∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)
⊢ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔ ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]

Premises used: SpectrumRestricts.real_iff, quasispectrumRestricts_iff_spectrumRestricts_inr, Unitization.quasispectrum_eq_spectrum_inr', Complex
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ HSub.hSub (α := ℂ) 2⁻¹ 1 = -1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
rw : 2⁻¹ * z ^ (-1 / 2) = z ^ (-1 / 2) / 2
rw₁ : z ^ (-1 / 2) * 2⁻¹ = z ^ (-1 / 2) / 2
rw₂ rw₃ : z ^ (-1 / 2) / 2 = z ^ (-1 / 2) / 2
⊢ 2⁻¹ * z ^ HSub.hSub (α := ℂ) 2⁻¹ 1 = z ^ (-1 / 2) / 2

Tactic:
rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ HasStrictDerivAt sqrt (z ^ (-1 / 2) / 2) z

Tactic:
exact (Complex.hasStrictDerivAt_cpow_const (c := 2⁻¹) hz).congr_deriv (by
    rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv])

Premises used: HasStrictDerivAt.congr_deriv, Complex.hasStrictDerivAt_cpow_const
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ HasDerivAt sqrt (z ^ (-1 / 2) / 2) z

Tactic:
(hasStrictDerivAt_sqrt hz).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, Complex.hasStrictDerivAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
s : Set ℂ
hz : z ∈ slitPlane
⊢ HasDerivWithinAt sqrt (z ^ (-1 / 2) / 2) s z

Tactic:
(hasDerivAt_sqrt hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Complex.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ DifferentiableAt ℂ sqrt z

Tactic:
(hasDerivAt_sqrt hz).differentiableAt

Premises used: HasDerivAt.differentiableAt, Complex.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
s : Set ℂ
hz : z ∈ slitPlane
⊢ DifferentiableWithinAt ℂ sqrt s z

Tactic:
(differentiableAt_sqrt hz).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Complex.differentiableAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
⊢ DifferentiableOn ℂ sqrt slitPlane

Tactic:
fun _ hz => (differentiableAt_sqrt hz).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Complex.differentiableAt_sqrt, DifferentiableOn
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ deriv sqrt z = z ^ (-1 / 2) / 2

Tactic:
(hasDerivAt_sqrt hz).deriv

Premises used: HasDerivAt.deriv, Complex.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ derivWithin sqrt slitPlane z = z ^ (-1 / 2) / 2

Tactic:
(hasDerivWithinAt_sqrt hz).derivWithin (isOpen_slitPlane.uniqueDiffWithinAt hz)

Premises used: Complex.isOpen_slitPlane, IsOpen.uniqueDiffWithinAt, HasDerivWithinAt.derivWithin, Complex.hasDerivWithinAt_sqrt
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
z : ℂ
hz : 0 ≤ z.re ∨ z.im ≠ 0
⊢ 0 < re 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.SqrtDeriv
Goal:
⊢ ContinuousOn sqrt slitPlane

Tactic:
fun _ hz => (continuousAt_sqrt (hz.imp le_of_lt id)).continuousWithinAt

Premises used: Complex.continuousAt_sqrt, ContinuousAt.continuousWithinAt, le_of_lt, id, ContinuousOn, Or.imp
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
h : SummableLocallyUniformlyOn f s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
obtain :
  ∀ (g : ℂ → E) (hg : HasSumLocallyUniformlyOn f g s),
    DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s

Tactic:
obtain ⟨g, hg⟩ := h
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
refine_2 : ∀ (hc : DifferentiableOn ℂ g s), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
refine_1 : ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s

Tactic:
have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
refine_2 : ∀ x ∈ s, ∑' (n : ι), f n x = g x
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s

Tactic:
apply hc.congr

Premises used: DifferentiableOn.congr
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
hc : DifferentiableOn ℂ g s
⊢ ∀ x ∈ s, ∑' (n : ι), f n x = g x

Tactic:
apply hg.tsum_eqOn

Premises used: HasSumLocallyUniformlyOn.tsum_eqOn
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
t : Finset ι
r : ℂ
hr : r ∈ s
⊢ DifferentiableWithinAt.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ t, f i x2) s r

Tactic:
DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableWithinAt.fun_sum
-- Module: Mathlib.Analysis.Complex.SummableUniformlyOn
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
refine_1 :
  ∀ (a : Finset ι),
    Membership.mem (γ := Set (Finset ι))
      {x : Finset ι |
        (fun (n : Finset ι) ↦ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s) x}
      a
refine_1₁ : ∀ (a : Finset ι), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ a, f i x2) s
refine_1₂ :
  ∀ (t : Finset ι) (r : ℂ) (hr : r ∈ s),
    DifferentiableWithinAt.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ t, f i x2) s r
⊢ ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s

Tactic:
filter_upwards with t r hr using
      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.TaylorSeries
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
obtain : ∀ (r' : ℝ) (h₁ : dist c z < r') (h₂ : r' < r), ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)

Premises used: exists_between, Iff.mp, Metric.mem_ball'