awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
inl :
  ∀ (hf : TendstoLocallyUniformlyOn F f ⊥ U) (hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U),
    ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) ⊥ K
⊢ ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
have inr : ∀ (hne : φ.NeBot), ∀ K ⊆ U, IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
Tactic: rcases φ.eq_or_neBot with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
have inr : ∀ (δ : ℝ) (hδ : δ > 0) (hK4 : cthickening δ K ⊆ U) (h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K),
  TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
Tactic: obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
φ : Filter ι
F : ι → ℂ → E
f : ℂ → E
inst_2 : CompleteSpace E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : φ.NeBot
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
have inr : ∀ (z : ℂ) (hz : z ∈ K), closedBall z δ ⊆ U
Tactic: refine h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
have hc : TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
  (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
Tactic: have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
have refine : ∀ (s : Finset ι), DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U
Tactic: refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
have have : ∀
  (hc :
    TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
      (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U),
  DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
Tactic: classical
  have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
  refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
  exact DifferentiableOn.fun_sum fun i _ => hf i
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
have have₁ have₂ :
  ∀
    (hc :
      TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
        (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U),
    DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
⊢ DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (w : ℂ) ↦ ∑' (i : ι), F i w) U
have have₃ : ∀
  (hc :
    TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
      (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U)
  (s : Finset ι), DifferentiableOn.{0, 0, u_1} ℂ (F := E) (fun (x : ℂ) ↦ ∑ n ∈ s, F n x) U
Tactic: classical
  have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
  refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
  exact DifferentiableOn.fun_sum fun i _ => hf i
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ Tendsto.{u_2, u_1} (β := E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) (SummationFilter.unconditional ι).filter
    (𝓝 (deriv (fun (w : ℂ) ↦ ∑' (i : ι), F i w) z))
have hc : TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
  (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
Tactic: have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
⊢ Tendsto.{u_2, u_1} (β := E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) (SummationFilter.unconditional ι).filter
    (𝓝 (deriv (fun (w : ℂ) ↦ ∑' (i : ι), F i w) z))
have h : Eq (α := Finset ι → E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) fun (i : Finset ι) ↦
  (deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) i z
Tactic: convert!
    (hc.deriv (Eventually.of_forall fun s => DifferentiableOn.fun_sum fun i _ => hf i)
          hU).tendsto_at
      hz using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
U : Set ℂ
z : ℂ
F : ι → ℂ → E
inst_2 : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hz : z ∈ U
hc :
  TendstoLocallyUniformlyOn.{0, u_1, u_2} (β := E) (fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x)
    (fun (x : ℂ) ↦ ∑' (n : ι), F n x) atTop U
⊢ Eq (α := Finset ι → E) (fun (s : Finset ι) ↦ ∑ b ∈ s, deriv (F b) z) fun (i : Finset ι) ↦
    (deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) i z
have h : ∀ (s : Finset ι),
  Eq.{u_1 + 1} (α := E) (∑ b ∈ s, deriv (F b) z : E) ((deriv ∘ fun (t : Finset ι) (x : ℂ) ↦ ∑ n ∈ t, F n x) s z : E)
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
have rw : circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
Tactic: rw [← circleAverage_abs_radius]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
have inl : ∀ (hR : |R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
Tactic: rcases le_or_gt |R| 0 with hR | hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
inl : ∀ (hR : |R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
have inr : ∀ (hR : 0 < |R|), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
Tactic: rcases le_or_gt |R| 0 with hR | hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) * (z - w)⁻¹) • f z) c |R| =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
have simp : Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, |R|), (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z)
  (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
Tactic: simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ Eq.{u_1 + 1} (α := E) (∮ (z : ℂ) in C(c, |R|), (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z)
    (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
have apply : EqOn.{0, u_1} (β := E) (fun (z : ℂ) ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) (fun (z : ℂ) ↦ (z - w)⁻¹ • f z)
  (sphere c |R|)
Tactic: apply circleIntegral.integral_congr hR.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
z : ℂ
hz : z ∈ sphere c |R|
⊢ Eq.{u_1 + 1} (α := E) ((fun (z : ℂ) ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) z) ((fun (z : ℂ) ↦ (z - w)⁻¹ • f z) z)
have match_scalars : (z - c)⁻¹ * ((z - c) * (z - w)⁻¹ * 1) = (z - w)⁻¹ * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
z : ℂ
hz : z ∈ sphere c |R|
⊢ (z - c)⁻¹ * ((z - c) * (z - w)⁻¹ * 1) = (z - w)⁻¹ * 1
have this : z - c ≠ 0
Tactic: have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z) = f w
have rw : (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I) • f w = f w
Tactic: rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I) • f w = f w
have match_scalars : (2 * (↑π : ℂ) * I)⁻¹ * (2 * (↑π : ℂ) * I * 1) = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
have calc : circleAverage (fun (z : ℂ) ↦ ((z - c) * (z - w)⁻¹) • f z) c |R| =
  HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
Tactic: calc circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c |R|
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, |R|), (z - w)⁻¹ • f z) := by
    simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
    apply circleIntegral.integral_congr hR.le
    intro z hz
    match_scalars
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    grind
  _ = f w := by
    rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]
    match_scalars
    simp [field]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
calc :
  circleAverage (fun (z : ℂ) ↦ ((z - c) * (z - w)⁻¹) • f z) c |R| =
    HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z)
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = f w
have calc₁ : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z) = f w
Tactic: calc circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c |R|
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, |R|), (z - w)⁻¹ • f z) := by
    simp only [circleAverage_eq_circleIntegral hR.ne', mul_inv_rev, inv_I, neg_mul, neg_smul,
      neg_inj, ne_eq, mul_eq_zero, I_ne_zero, inv_eq_zero, ofReal_eq_zero, pi_ne_zero,
      OfNat.ofNat_ne_zero, or_self, not_false_eq_true, smul_right_inj]
    apply circleIntegral.integral_congr hR.le
    intro z hz
    match_scalars
    have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
    grind
  _ = f w := by
    rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]
    match_scalars
    simp [field]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
have pos : ∀ (hR : |R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
Tactic: by_cases hR : |R| ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
pos : ∀ (hR : |R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
have neg : ∀ (hR : ¬|R| ≤ 0), circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
Tactic: by_cases hR : |R| ≤ 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
have apply : ContinuousOn f (closedBall c |R|)
Tactic: apply circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable countable_empty _ _ hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
apply : ContinuousOn f (closedBall c |R|)
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w
have apply₁ : ∀ z ∈ ball c |R| \ ∅, DifferentiableAt ℂ f z
Tactic: apply circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable countable_empty _ _ hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
z : ℂ
hz : z ∈ ball c |R| \ ∅
⊢ DifferentiableAt ℂ f z
have hz₁ : z ∈ ball c |R|
Tactic: rw [diff_empty] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
⊢ circleAverage f c R = f c
have pos : ∀ (hR : R = 0), circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
pos : ∀ (hR : R = 0), circleAverage f c R = f c
⊢ circleAverage f c R = f c
have neg : ∀ (hR : ¬R = 0), circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
⊢ circleAverage f c R = f c
have neg : circleAverage f c R = circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
Tactic: rw [← circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable hs h₁f h₂f (by aesop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
⊢ circleAverage f c R = circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
have apply : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), f z = ((z - c) / (z - c)) • f z
Tactic: apply circleAverage_congr_sphere fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : ¬R = 0
z : ℂ
hz : z ∈ sphere c |R|
⊢ f z = ((z - c) / (z - c)) • f z
have this : z - c ≠ 0
Tactic: have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
⊢ Real.circleAverage f c R = f c
have pos : ∀ (hR : R = 0), Real.circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
pos : ∀ (hR : R = 0), Real.circleAverage f c R = f c
⊢ Real.circleAverage f c R = f c
have neg : ∀ (hR : ¬R = 0), Real.circleAverage f c R = f c
Tactic: by_cases hR : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = f c
have neg : Real.circleAverage f c R = Real.circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
Tactic: rw [← circleAverage_smul_div hf (by aesop)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = Real.circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
have apply : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), f z = ((z - c) / (z - c)) • f z
Tactic: apply circleAverage_congr_sphere fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.MeanValue (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
z : ℂ
hz : z ∈ sphere c |R|
⊢ f z = ((z - c) / (z - c)) • f z
have this : z - c ≠ 0
Tactic: have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z : ℂ
⊢ |z.re| ≤ ‖z‖
have rw : z.re * z.re ≤ (normSq : (a : ℂ) → ℝ) z
Tactic: rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (Complex.norm_nonneg _), abs_mul_abs_self,
    norm_mul_self_eq_normSq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Norm (goal)
Goal:
z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)
have rw : HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) : ℝ) +
    2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
  HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)
      ((normSq : (a : ℂ) → ℝ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) : ℝ) +
    2 * √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))
Tactic: rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
      add_right_comm, normSq_add, mul_assoc, norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z,
      ← normSq_conj w, ← map_mul]