awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
linarith :
  Real.log M - Real.log ‖f c‖ <
      ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) →
    -(HMul.hMul (α := ℝ) 1 (circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R) -
              (HMul.hMul (α := ℝ) 1
                  (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)) +
                1 * Real.log ‖f c‖)) +
          (circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R - Real.log M) +
        (1 * Real.log M - 1 * Real.log ‖f c‖ -
          HMul.hMul (α := ℝ) 1
            (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))) =
      0
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) ≤
    Real.log M - Real.log ‖f c‖

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
linarith : M = 0 → -1 + (1 - M) + (M - 0) = 0
⊢ M ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
rw rw₁ : Real.log (M / ‖f c‖) = Real.log (M / ‖f c‖)
⊢ Real.log M - Real.log ‖f c‖ = Real.log (M / ‖f c‖)

Tactic:
rw [← log_div (by linarith) (norm_ne_zero_iff.mpr h₂f)]

Premises used: Iff.mpr, Real.log_div, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
Bound :
  LE.le (α := ℝ) (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))
Bound₁ :
  ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) ≤
    Real.log M - Real.log ‖f c‖
Bound₂ : Real.log M - Real.log ‖f c‖ = Real.log (M / ‖f c‖)
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)

Tactic:
calc
  -- Bound by the sum from Jensen's formula
  _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]
  _ ≤ Real.log M - Real.log ‖f c‖ := by linarith --Uses jensen and integral_bound
  _ = _ := by rw [← log_div (by linarith) (norm_ne_zero_iff.mpr h₂f)]

Premises used: Norm.norm, Real.log
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
z : ℂ
hz : z ∈ sphere c R
⊢ ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)

Tactic:
simpa [norm_smul, norm_pow, norm_inv, ← div_eq_inv_mul, mem_sphere_iff_norm.1 hz] using
      (div_le_div_iff_of_pos_right (mul_pos (pow_pos hR n) hR)).2 (hC z hz)

Premises used: Iff.mpr, pow_pos, norm_smul, norm_pow, div_le_div_iff_of_pos_right, norm_inv, mul_pos, mem_sphere_iff_norm, Iff.mp, div_eq_inv_mul
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)

Tactic:
have hp (z) (hz : z ∈ sphere c R) : ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R) := by
    simpa [norm_smul, norm_pow, norm_inv, ← div_eq_inv_mul, mem_sphere_iff_norm.1 hz] using
      (div_le_div_iff_of_pos_right (mul_pos (pow_pos hR n) hR)).2 (hC z hz)
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0

Tactic:
simp [Nat.factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0

Tactic:
have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0
rw :
  n.factorial • (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)

Tactic:
rw [← inv_smul_smul₀ this (iteratedDeriv n f c), inv_div, div_eq_inv_mul, mul_comm,
      ← nsmul_eq_mul, smul_assoc]

Premises used: inv_smul_smul₀, smul_assoc, mul_comm, nsmul_eq_mul, inv_div, iteratedDeriv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0
⊢ n.factorial • (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)

Tactic:
simp [← DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul hR n hf]

Premises used: DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)

Tactic:
have hq : iteratedDeriv n f c = n.factorial • (2 * π * I)⁻¹ •
    ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z := by
    have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]
    rw [← inv_smul_smul₀ this (iteratedDeriv n f c), inv_div, div_eq_inv_mul, mul_comm,
      ← nsmul_eq_mul, smul_assoc]
    simp [← DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul hR n hf]
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
rw rw₁ :
  ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
⊢ ‖iteratedDeriv n f c‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖

Tactic:
rw [hq]
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ LT.lt (α := ℝ) 0 (↑n.factorial : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
rw :
  ‖HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤ R * (C / R ^ (n + 1))
⊢ ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤
    (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1)))

Tactic:
rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]

Premises used: RCLike.norm_nsmul, nsmul_eq_mul, Complex, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ ‖HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤ R * (C / R ^ (n + 1))

Tactic:
circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp

Premises used: LT.lt.le, circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ ‖HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤ R * (C / R ^ (n + 1))

Tactic:
exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp

Premises used: LT.lt.le, circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1))) = (↑n.factorial : ℝ) * C / R ^ n

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
n₁ :
  ‖iteratedDeriv n f c‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
n₂ :
  ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤
    (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1)))
n₃ : (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1))) = (↑n.factorial : ℝ) * C / R ^ n
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n

Tactic:
calc
    ‖iteratedDeriv n f c‖ = ‖n.factorial • (2 * π * I)⁻¹ •
      ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ := by rw [hq]
    _ ≤ n.factorial * (R * (C / (R ^ (n + 1)))) := by
      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp
    _ = n.factorial * C / R ^ n := by
      grind

Premises used: Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, HPow.hPow, HAdd.hAdd, Nat.factorial, iteratedDeriv, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
simpa using norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le 1 hR hf hC

Premises used: Complex.norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c

Tactic:
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
    e.hasFDerivAt.comp_hasDerivAt c
      (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
rw : ‖deriv f c‖ = norm (E := F̂) ((e : (a : F) → F̂) (deriv f c) : F̂)
⊢ ‖deriv f c‖ = norm (E := F̂) (deriv ((⇑e : (a : F) → F̂) ∘ f) c)

Tactic:
rw [this.deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
⊢ ‖deriv f c‖ = norm (E := F̂) ((e : (a : F) → F̂) (deriv f c) : F̂)

Tactic:
(UniformSpace.Completion.norm_coe _).symm

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.norm_coe, SeparationQuotient.mk, Eq.symm
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
⊢ ‖deriv f c‖ = norm (E := F̂) ((e : (a : F) → F̂) (deriv f c) : F̂)

Tactic:
exact (UniformSpace.Completion.norm_coe _).symm

Premises used: UniformSpace.Completion.norm_coe, Eq.symm
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
⊢ norm (E := F̂) (deriv ((⇑e : (a : F) → F̂) ∘ f) c) ≤ C / R

Tactic:
norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
        (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)

Premises used: Eq.trans_le, ContinuousLinearMap.differentiable, UniformSpace.Completion.norm_coe, _private.0.Complex.norm_deriv_le_aux, Differentiable.comp_diffContOnCl
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
f₁ : ‖deriv f c‖ = norm (E := F̂) (deriv ((⇑e : (a : F) → F̂) ∘ f) c)
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
calc
    ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
      rw [this.deriv]
      exact (UniformSpace.Completion.norm_coe _).symm
    _ ≤ C / R :=
      norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
        (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)

Premises used: deriv, Function.comp, Eq.trans_le, ContinuousLinearMap.differentiable, UniformSpace.Completion.norm_coe, _private.0.Complex.norm_deriv_le_aux, DFunLike.coe, Differentiable.comp_diffContOnCl
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : ℂ
suffices : ∀ (c : ℂ), deriv f c = 0
⊢ f z = f w

Tactic:
suffices ∀ c, deriv f c = 0 from is_const_of_deriv_eq_zero hf this z w
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
rcases : ∀ (C : ℝ) (hC : ∀ x ∈ range f, ‖x‖ ≤ C), ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩

Premises used: isBounded_iff_forall_norm_le, Iff.mp
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
hC : ∀ x ∈ range f, ‖x‖ ≤ C
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
        (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩

Premises used: Set.mem_range_self, Iff.mpr, zero_lt_one, Max.max, And.intro, Exists.intro, LE.le.trans, OfNat.ofNat, le_max_left, Or.inr, lt_max_iff
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
hC : ∀ x ∈ range f, ‖x‖ ≤ C
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C

Tactic:
exact
      ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
        (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
obtain : ∀ (C : ℝ) (C₀ : C > 0) (hC : ∀ (z : ℂ), ‖f z‖ ≤ C), deriv f c = 0
⊢ deriv f c = 0

Tactic:
obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C := by
    rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
    exact
      ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
        (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0

Tactic:
norm_le_zero_iff.1 (le_of_forall_gt_imp_ge_of_dense fun ε ε₀ => ?_)

Premises used: norm_le_zero_iff, Iff.mp, le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
refine : ∀ (ε : ℝ) (ε₀ : 0 < ε), ‖deriv f c‖ ≤ ε
⊢ deriv f c = 0

Tactic:
refine norm_le_zero_iff.1 (le_of_forall_gt_imp_ge_of_dense fun ε ε₀ => ?_)

Premises used: norm_le_zero_iff, Iff.mp, le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.Complex.Liouville
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
ε : ℝ
ε₀ : 0 < ε
⊢ ‖deriv f c‖ ≤ C / (C / ε)

Tactic:
norm_deriv_le_of_forall_mem_sphere_norm_le (div_pos C₀ ε₀) hf.diffContOnCl fun z _ => hC z

Premises used: Differentiable.diffContOnCl, Complex.norm_deriv_le_of_forall_mem_sphere_norm_le, div_pos