awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
have inr : ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
Tactic: refine norm_le_of_forall_mem_frontier_norm_le isBounded_ball (hdg'.diffContOnCl_ball subset_rfl)
    ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
inr : ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
⊢ ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
have inr₁ : z ∈ closure (ball c R₁)
Tactic: refine norm_le_of_forall_mem_frontier_norm_le isBounded_ball (hdg'.diffContOnCl_ball subset_rfl)
    ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
⊢ ∀ z ∈ frontier (ball c R₁), ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
have inr : ∀ z ∈ sphere c R₁, ‖g' z‖ ≤ R₂ / R₁ ^ (n + 1)
Tactic: grw [frontier_ball_subset_sphere]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)
have hwc : w ≠ c
Tactic: have hwc := ne_of_mem_sphere hw hR₁.ne'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)
have hfw : ‖f w - f c‖ ≤ R₂
Tactic: have hfw : ‖f w - f c‖ ≤ R₂ := by
      simpa [dist_eq_norm] using h_maps (sphere_subset_closedBall hw)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 c) (fun (x : ℂ) ↦ f x - f c) fun (w : ℂ) ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
g : ℂ → ℂ := fun (w : ℂ) ↦ ((w - c) ^ (n + 1))⁻¹ * (f w - f c)
g' : (a : ℂ) → ℂ := update (β := fun (a : ℂ) ↦ ℂ) g c ((𝓝[≠] c).limUnder g)
hdg' : DifferentiableOn ℂ g' (closedBall c R₁)
w : ℂ
hw : w ∈ sphere c R₁
hwc : w ≠ c
hfw : ‖f w - f c‖ ≤ R₂
⊢ ‖g' w‖ ≤ R₂ / R₁ ^ (n + 1)
have hw₁ : ‖w - c‖ = R₁
Tactic: rw [mem_sphere_iff_norm] at hw
Cleared hypotheses: hw, hwc, hfw
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₁
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hR₁ : 0 < R₁
Tactic: have hR₁ : 0 < R₁ := nonempty_ball.mp ⟨_, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₁
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hR₂ : 0 ≤ R₂
Tactic: have hR₂ : 0 ≤ R₂ := nonempty_closedBall.mp ⟨_, h_maps hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have inl : ∀ (heq : f z = f c), dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Tactic: rcases eq_or_ne (f z) (f c) with heq | hfne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
inl : ∀ (heq : f z = f c), dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have inr : ∀ (hfne : f z ≠ f c), dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Tactic: rcases eq_or_ne (f z) (f c) with heq | hfne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have trans : dist (f z) (f c) ≤ 0
Tactic: trans 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
heq : f z = f c
trans : dist (f z) (f c) ≤ 0
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have trans₁ : 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Tactic: trans 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have trans : dist (f z) (f c) ≤ 0
Tactic: trans 0 <;> [simp [heq]; positivity]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂
heq : f z = f c
trans : dist (f z) (f c) ≤ 0
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have trans₁ : 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Tactic: trans 0 <;> [simp [heq]; positivity]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hne : z ≠ c
Tactic: have hne : z ≠ c := ne_of_apply_ne _ hfne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have inr : ∀ (g : StrongDual ℂ F) (hg : ‖g‖ = 1) (hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)),
  dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Tactic: rcases exists_dual_vector ℂ _ (norm_sub_eq_zero_iff.not.mpr hfne) with ⟨g, hg, hgf⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hmaps_line : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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₂)
have refine : MapsTo (⇑g : (a : F) → ℂ) (closedBall (f c) R₂) (closedBall (h 0) R₂)
Tactic: refine MapsTo.comp ?_ (h_maps.comp hmaps_line)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₁)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hmaps : 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₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
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₂)
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hdiff : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
have 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
Tactic: simp only [h, ← map_sub, Function.comp_apply, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
have 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
Tactic: refine (g.isBigO_comp _ _).trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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.{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
have 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
Tactic: rw [← lineMap_apply_zero (k := ℂ) c z] at hn
Cleared hypotheses: hn, hz, hR₁, hR₂, hfne, hne, g, hg, hgf, h, hmaps_line, hmaps, hdiff
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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
have refine_1 : Tendsto (α := ℂ) (β := E) ((⇑(lineMap c z) : (a : ℂ) → E) : (a : ℂ) → E) (𝓝 0)
  (𝓝 ((lineMap c z : (a : ℂ) → E) 0) : Filter E)
Tactic: refine hn.comp_tendsto ?_ |>.trans_isBigO ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
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)
⊢ 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
have 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
Tactic: refine hn.comp_tendsto ?_ |>.trans_isBigO ?_