awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
w : ℂ
hw : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) w
⊢ Membership.mem (α := E) (ball c R₁) ((lineMap c z : (a : ℂ) → E) w : E)

Tactic:
simpa [lt_div_iff₀, hne, dist_comm c] using hw

Premises used: lt_div_iff₀, dist_comm
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
⊢ MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)

Tactic:
have hmaps_line : MapsTo (lineMap c z) (ball (0 : ℂ) (R₁ / dist z c)) (ball c R₁) := by
    intro w hw
    simpa [lt_div_iff₀, hne, dist_comm c] using hw
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
⊢ MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)

Tactic:
MapsTo.comp ?_ (h_maps.comp hmaps_line)

Premises used: Set.MapsTo.comp
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
refine : MapsTo (⇑g : (a : F) → ℂ) (closedBall (f c) R₂) (closedBall (h 0) R₂)
⊢ MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)

Tactic:
refine MapsTo.comp ?_ (h_maps.comp hmaps_line)

Premises used: Set.MapsTo.comp
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
⊢ MapsTo (⇑g : (a : F) → ℂ) (closedBall (f c) R₂) (closedBall (h 0) R₂)

Tactic:
simpa [hg, h] using g.lipschitz.mapsTo_closedBall (f c) R₂

Premises used: ContinuousLinearMap.lipschitz, LipschitzWith.mapsTo_closedBall
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
⊢ MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)

Tactic:
have hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂) := by
    refine MapsTo.comp ?_ (h_maps.comp hmaps_line)
    simpa [hg, h] using g.lipschitz.mapsTo_closedBall (f c) R₂
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
⊢ DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))

Tactic:
have hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c)) :=
    g.differentiable.comp_differentiableOn <| hd.comp (lineMap c z).differentiableOn hmaps_line
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
simp :
  Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ (g : (a : F) → ℂ) (f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)))
    fun (w : ℂ) ↦ w ^ n
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n

Tactic:
simp only [h, ← map_sub, Function.comp_apply, sub_zero]

Premises used: map_sub, sub_zero, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ (g : (a : F) → ℂ) (f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)))
    fun (w : ℂ) ↦ w ^ n

Tactic:
(g.isBigO_comp _ _).trans_isLittleO ?_

Premises used: ContinuousLinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
refine :
  Asymptotics.IsLittleO.{0, u_2, 0} (E := F) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : ℂ) ↦ w ^ n
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ (g : (a : F) → ℂ) (f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)))
    fun (w : ℂ) ↦ w ^ n

Tactic:
refine (g.isBigO_comp _ _).trans_isLittleO ?_

Premises used: ContinuousLinearMap.isBigO_comp, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
rw :
  ∀
    (hn :
      Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
        (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
        ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n)
    (hz : z ∈ ball c R₁) (hR₁ : 0 < R₁) (hR₂ : 0 ≤ R₂) (hfne : f z ≠ f c) (hne : z ≠ c) (g : StrongDual ℂ F)
    (hg : ‖g‖ = 1) (hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)),
    let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
    ∀ (hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁))
      (hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂))
      (hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))),
      Asymptotics.IsLittleO.{0, u_2, 0} (E := F) (F := ℂ) (𝓝 0)
        (fun (x : ℂ) ↦ f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : ℂ) ↦ w ^ n
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := F) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : ℂ) ↦ w ^ n

Tactic:
rw [← lineMap_apply_zero (k := ℂ) c z] at hn

Premises used: AffineMap.lineMap_apply_zero
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
    (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
    ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := F) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : ℂ) ↦ w ^ n

Tactic:
hn.comp_tendsto ?_ |>.trans_isBigO ?_

Premises used: Asymptotics.IsLittleO.comp_tendsto, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
    (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
    ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
refine_1 :
  Tendsto (α := ℂ) (β := E) ((⇑(lineMap c z) : (a : ℂ) → E) : (a : ℂ) → E) (𝓝 0)
    (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
refine_2 :
  Asymptotics.IsBigO (E := ℝ) (F := ℂ) (𝓝 0)
    ((fun (w : E) ↦ ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n) ∘ (⇑(lineMap c z) : (a : ℂ) → E))
    fun (w : ℂ) ↦ w ^ n
⊢ Asymptotics.IsLittleO.{0, u_2, 0} (E := F) (F := ℂ) (𝓝 0)
    (fun (x : ℂ) ↦ f ((lineMap c z : (a : ℂ) → E) x) - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : ℂ) ↦ w ^ n

Tactic:
refine hn.comp_tendsto ?_ |>.trans_isBigO ?_

Premises used: Asymptotics.IsLittleO.comp_tendsto, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
    (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
    ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑(lineMap c z) : (a : ℂ) → E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
    (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
    ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Tendsto (α := ℂ) (β := E) ((⇑(lineMap c z) : (a : ℂ) → E) : (a : ℂ) → E) (𝓝 0)
    (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)

Tactic:
exact Continuous.tendsto (by fun_prop) 0

Premises used: Continuous.tendsto, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (α := E) (E := F) (F := ℝ) (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
    (fun (x : E) ↦ f x - f ((lineMap c z : (a : ℂ) → E) 0)) fun (w : E) ↦
    ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℂ) (𝓝 0)
    ((fun (w : E) ↦ ‖HSub.hSub (β := E) w ((lineMap c z : (a : ℂ) → E) 0 : E)‖ ^ n) ∘ (⇑(lineMap c z) : (a : ℂ) → E))
    fun (w : ℂ) ↦ w ^ n

Tactic:
simpa [Function.comp_def, ← dist_eq_norm_sub, mul_pow, mul_comm]
        using (Asymptotics.isBigO_refl (· ^ n) (𝓝 (0 : ℂ))).norm_left.const_mul_left _

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.const_mul_left, dist_eq_norm_sub, nhds, Function.comp_def, HPow.hPow, mul_comm, OfNat.ofNat, mul_pow, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n

Tactic:
have hn : (h · - h 0) =o[𝓝 0] (fun w ↦ (w - 0) ^ n) := by
    simp only [h, ← map_sub, Function.comp_apply, sub_zero]
    refine (g.isBigO_comp _ _).trans_isLittleO ?_
    rw [← lineMap_apply_zero (k := ℂ) c z] at hn
    refine hn.comp_tendsto ?_ |>.trans_isBigO ?_
    · exact Continuous.tendsto (by fun_prop) 0
    · simpa [Function.comp_def, ← dist_eq_norm_sub, mul_pow, mul_comm]
        using (Asymptotics.isBigO_refl (· ^ n) (𝓝 (0 : ℂ))).norm_left.const_mul_left _
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn_1 : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n
⊢ Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1

Tactic:
simpa [lt_div_iff₀, hne]

Premises used: lt_div_iff₀
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn_1 : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n
⊢ Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1

Tactic:
have hmem : 1 ∈ ball (0 : ℂ) (R₁ / dist z c) := by
    simpa [lt_div_iff₀, hne]