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_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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)

Tactic:
rw [map_sub] at hgf

Premises used: map_sub
-- 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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
⊢ MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)

Tactic:
rw [map_sub] at hgf

Premises used: map_sub
-- 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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
hmaps_line₁ : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
⊢ let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)

Tactic:
rw [map_sub] at hgf

Premises used: map_sub
-- 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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
hmaps_line₁ : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
⊢ let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))

Tactic:
rw [map_sub] at hgf

Premises used: map_sub
-- 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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
hmaps_line₁ : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n

Tactic:
rw [map_sub] at hgf

Premises used: map_sub
-- 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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
hmaps_line₁ : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn₁ :
  let h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E);
  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:
rw [map_sub] at hgf

Premises used: map_sub
-- 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 : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (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
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
simpa [hgf, h, dist_eq_norm_sub] using schwarz_aux hdiff hmaps hn hmem

Premises used: dist_eq_norm_sub, _private.0.Complex.schwarz_aux
-- 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
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO (n := 0) hd h_maps ?_ hz |>.trans_eq ?_

Premises used: LE.le.trans_eq, Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_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
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
refine_1 :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦
    HPow.hPow (β := ℕ) ‖w - c‖ 0
refine_2 : R₂ * (dist z c / R₁) ^ HAdd.hAdd (α := ℕ) 0 1 = R₂ / R₁ * dist z c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
refine dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO (n := 0) hd h_maps ?_ hz |>.trans_eq ?_

Premises used: LE.le.trans_eq, Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_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
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦
    HPow.hPow (β := ℕ) ‖w - c‖ 0

Tactic:
simpa using hd.continuousOn.continuousAt
      (ball_mem_nhds _ <| nonempty_ball.mp ⟨_, hz⟩) |>.sub_const (f c)

Premises used: DifferentiableOn.continuousOn, Metric.nonempty_ball, Filter.Tendsto.sub_const, Metric.ball_mem_nhds, Exists.intro, Iff.mp, ContinuousOn.continuousAt
-- 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
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ R₂ * (dist z c / R₁) ^ HAdd.hAdd (α := ℕ) 0 1 = R₂ / R₁ * dist z c

Tactic:
simp [field]
-- 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
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ 0 ≤ R₂

Tactic:
have : 0 ≤ R₂ := nonempty_closedBall.mp <| h_maps.nonempty <| nonempty_ball.mpr h₀
-- 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
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
⊢ 0 ≤ R₂ / R₁

Tactic:
positivity
-- 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
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
refine : ∀ᶠ (x : E) in 𝓝 c, ‖f x - f c‖ ≤ R₂ / R₁ * ‖x - c‖
⊢ norm (E := E →L[ℂ] F) (fderiv ℂ f c) ≤ R₂ / R₁

Tactic:
refine norm_fderiv_le_of_lip' _ (by positivity) ?_

Premises used: norm_fderiv_le_of_lip'
-- 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
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
h : ∀ (z : E) (hz : z ∈ ball c R₁), ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖
⊢ ∀ᶠ (x : E) in 𝓝 c, ‖f x - f c‖ ≤ R₂ / R₁ * ‖x - c‖

Tactic:
filter_upwards [ball_mem_nhds _ h₀] with z hz

Premises used: Metric.ball_mem_nhds
-- 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
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
z : E
hz : z ∈ ball c R₁
⊢ ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖

Tactic:
simpa [dist_eq_norm_sub] using dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz

Premises used: dist_eq_norm_sub, Complex.dist_le_div_mul_dist_of_mapsTo_ball
-- 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
R : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (closedBall (f c) R)
hz : z ∈ ball c R
⊢ dist (f z) (f c) ≤ dist z c

Tactic:
simpa [(nonempty_ball.1 ⟨z, hz⟩).ne'] using dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz

Premises used: Metric.nonempty_ball, Complex.dist_le_div_mul_dist_of_mapsTo_ball, LT.lt.ne', Exists.intro, Iff.mp
-- 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
R : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (closedBall (f c) R)
hR : 0 < R
⊢ norm (E := E →L[ℂ] F) (fderiv ℂ f c) ≤ 1

Tactic:
simpa [hR.ne'] using norm_fderiv_le_div_of_mapsTo_ball hd h_maps hR

Premises used: LT.lt.ne', Complex.norm_fderiv_le_div_of_mapsTo_ball
-- 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
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
rwa rwa₁ rwa₂ rwa₃ : MapsTo f (ball 0 R) (closedBall 0 R)
⊢ MapsTo f (ball 0 R) (closedBall (f 0) R)

Tactic:
rwa [h₀]
-- 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
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ ‖f z‖ ≤ ‖z‖

Tactic:
simpa [h₀] using dist_le_dist_of_mapsTo_ball hd (by rwa [h₀]) (mem_ball_zero_iff.mpr hz)

Premises used: Iff.mpr, Complex.dist_le_dist_of_mapsTo_ball, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
rw : norm (E := ℂ →L[ℂ] E) (fderiv ℂ f c) ≤ R₂ / R₁
⊢ ‖deriv f c‖ ≤ R₂ / R₁

Tactic:
rw [norm_deriv_eq_norm_fderiv]

Premises used: norm_deriv_eq_norm_fderiv
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ norm (E := ℂ →L[ℂ] E) (fderiv ℂ f c) ≤ R₂ / R₁

Tactic:
norm_fderiv_le_div_of_mapsTo_ball hd h_maps h₀

Premises used: Complex.norm_fderiv_le_div_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ norm (E := ℂ →L[ℂ] E) (fderiv ℂ f c) ≤ R₂ / R₁

Tactic:
exact norm_fderiv_le_div_of_mapsTo_ball hd h_maps h₀

Premises used: Complex.norm_fderiv_le_div_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R)
h_maps : MapsTo f (ball c R) (closedBall (f c) R)
h₀ : 0 < R
⊢ ‖deriv f c‖ ≤ 1

Tactic:
(norm_deriv_le_div_of_mapsTo_ball hd h_maps h₀).trans_eq (div_self h₀.ne')

Premises used: LE.le.trans_eq, LT.lt.ne', Complex.norm_deriv_le_div_of_mapsTo_ball, div_self
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
inl :
  ∀ (hd : DifferentiableOn ℂ f (ball z R₁)) (h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)) (hz : z ∈ ball z R₁),
    ‖dslope f z z‖ ≤ R₂ / R₁
inr : ∀ (hne : z ≠ c), ‖dslope f c z‖ ≤ R₂ / R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rcases eq_or_ne z c with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)
hz : z ∈ ball z R₁
⊢ 0 < R₁

Tactic:
simpa using hz
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)
hz : z ∈ ball z R₁
⊢ ‖dslope f z z‖ ≤ R₂ / R₁

Tactic:
simpa using norm_deriv_le_div_of_mapsTo_ball hd h_maps (by simpa using hz)

Premises used: Complex.norm_deriv_le_div_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
inr : dist (f z) (f c) ≤ R₂ / R₁ * dist z c
inr₁ : 0 < dist z c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rw [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← dist_eq_norm_sub,
      ← dist_eq_norm_sub, ← div_eq_inv_mul, div_le_iff₀]

Premises used: div_le_iff₀, norm_smul, dist_eq_norm_sub, norm_inv, dslope_of_ne, div_eq_inv_mul, slope_def_module
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz

Premises used: Complex.dist_le_div_mul_dist_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c

Tactic:
exact dist_le_div_mul_dist_of_mapsTo_ball hd h_maps hz

Premises used: Complex.dist_le_div_mul_dist_of_mapsTo_ball
-- Module: Mathlib.Analysis.Complex.Schwarz
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ 0 < dist z c

Tactic:
simpa
-- 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₁
⊢ 0 < R₁

Tactic:
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
-- 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₁
h : ∀ (w : ℂ), g w = ((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w
⊢ g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c

Tactic:
ext w
-- 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 :
  Eq (α := UniformSpace.Completion E) (dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c w)
    (((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w)
⊢ g w = ((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w

Tactic:
simp only [g]