awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
match_scalars : (z - c)⁻¹ * ((z - c) * (z - w)⁻¹ * 1) = (z - w)⁻¹ * 1
⊢ Eq.{u_1 + 1} (α := E) ((fun (z : ℂ) ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) z) ((fun (z : ℂ) ↦ (z - w)⁻¹ • f z) z)

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Complex.MeanValue
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 ≠ 0

Tactic:
grind [ne_of_mem_sphere]

Premises used: Metric.ne_of_mem_sphere
-- Module: Mathlib.Analysis.Complex.MeanValue
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 ≠ 0

Tactic:
have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
this : z - c ≠ 0
⊢ (z - c)⁻¹ * ((z - c) * (z - w)⁻¹ * 1) = (z - w)⁻¹ * 1

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
rw : (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I) • f w = f w
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z) = f w

Tactic:
rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw h₁f h₂f]

Premises used: Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
match_scalars : (2 * (↑π : ℂ) * I)⁻¹ * (2 * (↑π : ℂ) * I * 1) = 1
⊢ (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I) • f w = f w

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Complex.MeanValue
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 * 1) = 1

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Complex.MeanValue
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)
calc₁ : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, |R|), (z - w)⁻¹ • f z) = f w
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c |R| = 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]

Premises used: Real.pi, HMul.hMul, abs, HSub.hSub, Complex.ofReal, Inv.inv, circleIntegral, HSMul.hSMul, OfNat.ofNat, Complex.I, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.MeanValue
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
neg : ∀ (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

Tactic:
by_cases hR : |R| ≤ 0
-- Module: Mathlib.Analysis.Complex.MeanValue
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

Tactic:
simp_all [ball_eq_empty.2 hR]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Complex.MeanValue
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|)
apply₁ : ∀ z ∈ ball c |R| \ ∅, DifferentiableAt ℂ f z
⊢ circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - w)) • f z) c R = f w

Tactic:
apply circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable countable_empty _ _ hw

Premises used: circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable, Set.countable_empty
-- Module: Mathlib.Analysis.Complex.MeanValue
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
⊢ ContinuousOn f (closedBall c |R|)

Tactic:
simpa [← closure_ball _ (ne_of_not_ge hR).symm] using hf.2

Premises used: Ne.symm, DiffContOnCl.continuousOn, closure_ball, ne_of_not_ge
-- Module: Mathlib.Analysis.Complex.MeanValue
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| \ ∅
⊢ z ∈ ball c |R|

Tactic:
rw [diff_empty] at hz

Premises used: Set.diff_empty
-- Module: Mathlib.Analysis.Complex.MeanValue
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

Tactic:
apply (hf.1 z hz).differentiableAt (isOpen_ball.mem_nhds hz)

Premises used: DifferentiableWithinAt.differentiableAt, Metric.isOpen_ball, IsOpen.mem_nhds, DiffContOnCl.differentiableOn
-- Module: Mathlib.Analysis.Complex.MeanValue
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
neg : ∀ (hR : ¬R = 0), circleAverage f c R = f c
⊢ circleAverage f c R = f c

Tactic:
by_cases hR : R = 0
-- Module: Mathlib.Analysis.Complex.MeanValue
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

Tactic:
simp [hR]
-- Module: Mathlib.Analysis.Complex.MeanValue
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
⊢ c ∈ ball c |R|

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.MeanValue
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
neg : circleAverage f c R = circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
⊢ circleAverage f c R = f c

Tactic:
rw [← circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable hs h₁f h₂f (by aesop)]

Premises used: circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable
-- Module: Mathlib.Analysis.Complex.MeanValue
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
apply : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), f z = ((z - c) / (z - c)) • f z
⊢ circleAverage f c R = circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R

Tactic:
apply circleAverage_congr_sphere fun z hz ↦ ?_

Premises used: Real.circleAverage_congr_sphere
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
⊢ z - c ≠ 0

Tactic:
grind [ne_of_mem_sphere]

Premises used: Metric.ne_of_mem_sphere
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
⊢ z - c ≠ 0

Tactic:
have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
this : z - c ≠ 0
⊢ f z = ((z - c) / (z - c)) • f z

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.MeanValue
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
neg : ∀ (hR : ¬R = 0), Real.circleAverage f c R = f c
⊢ Real.circleAverage f c R = f c

Tactic:
by_cases hR : R = 0
-- Module: Mathlib.Analysis.Complex.MeanValue
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

Tactic:
simp [hR]
-- Module: Mathlib.Analysis.Complex.MeanValue
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
⊢ c ∈ ball c |R|

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.MeanValue
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
neg : Real.circleAverage f c R = Real.circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R
⊢ Real.circleAverage f c R = f c

Tactic:
rw [← circleAverage_smul_div hf (by aesop)]

Premises used: DiffContOnCl.circleAverage_smul_div
-- Module: Mathlib.Analysis.Complex.MeanValue
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
apply : ∀ (z : ℂ) (hz : z ∈ sphere c |R|), f z = ((z - c) / (z - c)) • f z
⊢ Real.circleAverage f c R = Real.circleAverage (fun (z : ℂ) ↦ ((z - c) / (z - c)) • f z) c R

Tactic:
apply circleAverage_congr_sphere fun z hz ↦ ?_

Premises used: Real.circleAverage_congr_sphere
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
⊢ z - c ≠ 0

Tactic:
grind [ne_of_mem_sphere]

Premises used: Metric.ne_of_mem_sphere
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
⊢ z - c ≠ 0

Tactic:
have : z - c ≠ 0 := by grind [ne_of_mem_sphere]
-- Module: Mathlib.Analysis.Complex.MeanValue
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|
this : z - c ≠ 0
⊢ f z = ((z - c) / (z - c)) • f z

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ ‖z‖ = √((normSq : (a : ℂ) → ℝ) z)

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ ‖z‖ * ‖z‖ = (normSq : (a : ℂ) → ℝ) z

Tactic:
Real.mul_self_sqrt (normSq_nonneg _)

Premises used: Real.mul_self_sqrt, Complex.normSq_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ 0 ≤ ‖z‖

Tactic:
Real.sqrt_nonneg _

Premises used: Real.sqrt_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw : z.re * z.re ≤ (normSq : (a : ℂ) → ℝ) z
⊢ |z.re| ≤ ‖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]

Premises used: Complex.norm_mul_self_eq_normSq, Complex.norm_nonneg, mul_self_le_mul_self_iff, Complex.re, abs_mul_abs_self, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ z.re * z.re ≤ (normSq : (a : ℂ) → ℝ) z

Tactic:
apply re_sq_le_normSq

Premises used: Complex.re_sq_le_normSq
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ z.re ≤ ‖z‖

Tactic:
(abs_le.1 (abs_re_le_norm _)).2

Premises used: abs_le, Complex.abs_re_le_norm, And.right, Iff.mp
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
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 : ℂ)))
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖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]

Premises used: Complex.norm_mul_self_eq_normSq, mul_assoc, Complex.normSq_add, Real.sqrt_mul, add_right_comm, Complex.normSq_conj, map_mul, Complex.norm_def, Complex.normSq_nonneg, add_mul_self_eq
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
bc :
  (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
    √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
⊢ (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
    √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))

Tactic:
re_le_norm (z * conj w)

Premises used: HMul.hMul, Complex.re_le_norm, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
⊢ (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re ≤
    √((normSq : (a : ℂ) → ℝ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)))

Tactic:
exact re_le_norm (z * conj w)

Premises used: HMul.hMul, Complex.re_le_norm, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ ‖z‖ = 0 ↔ z = 0

Tactic:
(Real.sqrt_eq_zero <| normSq_nonneg _).trans normSq_eq_zero

Premises used: Complex.normSq_nonneg, Iff.trans, Complex.normSq_eq_zero, Real.sqrt_eq_zero
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
⊢ norm (E := ℂ) 0 = 0

Tactic:
Complex.norm_eq_zero_iff.mpr rfl

Premises used: Iff.mpr, Complex.norm_eq_zero_iff, rfl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (-z)) = ‖z‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (-z)) = √((normSq : (a : ℂ) → ℝ) z)
rw₂ rw₃ : √((normSq : (a : ℂ) → ℝ) z) = √((normSq : (a : ℂ) → ℝ) z)
⊢ ‖-z‖ = ‖z‖

Tactic:
rw [Complex.norm_def, norm_def, normSq_neg]

Premises used: Complex.norm_def, Complex.normSq_neg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z * w)) = ‖z‖ * ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z * w)) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
rw₃ :
  √(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
    √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
rw₄ rw₅ :
  √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w) = √((normSq : (a : ℂ) → ℝ) z) * √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z * w‖ = ‖z‖ * ‖w‖

Tactic:
rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]

Premises used: Complex.normSq_mul, Real.sqrt_mul, Complex.norm_def, Complex.normSq_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z w : ℂ
rw : √((normSq : (a : ℂ) → ℝ) (z / w)) = ‖z‖ / ‖w‖
rw₁ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / ‖w‖
rw₂ : √((normSq : (a : ℂ) → ℝ) (z / w)) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
rw₃ :
  √(HDiv.hDiv (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)) =
    √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
rw₄ rw₅ :
  √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w) = √((normSq : (a : ℂ) → ℝ) z) / √((normSq : (a : ℂ) → ℝ) w)
⊢ ‖z / w‖ = ‖z‖ / ‖w‖

Tactic:
rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]

Premises used: Complex.normSq_div, Complex.norm_def, Complex.normSq_nonneg, Real.sqrt_div
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
n : ℕ
⊢ ‖z ^ n‖ = ‖z‖ ^ n

Tactic:
map_pow isAbsoluteValueNorm.abvHom _ _

Premises used: IsAbsoluteValue.abvHom, map_pow, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
n : ℤ
⊢ ‖z ^ n‖ = ‖z‖ ^ n

Tactic:
map_zpow₀ isAbsoluteValueNorm.abvHom _ _

Premises used: IsAbsoluteValue.abvHom, map_zpow₀, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℂ
⊢ ‖s.prod f‖ = ∏ i ∈ s, ‖f i‖

Tactic:
map_prod isAbsoluteValueNorm.abvHom _ _

Premises used: IsAbsoluteValue.abvHom, map_prod, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) = ‖z‖

Tactic:
simp [norm_def]

Premises used: Complex.norm_def
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
⊢ ‖I‖ = 1

Tactic:
simp [norm]

Premises used: Norm.norm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
⊢ ‖I‖₊ = 1

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
r : ℝ
⊢ ‖(↑r : ℂ)‖ = ‖r‖

Tactic:
simp [norm_def, Real.sqrt_mul_self_eq_abs]

Premises used: Complex.norm_def, Real.sqrt_mul_self_eq_abs
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
r : ℝ
h : 0 ≤ r
⊢ ‖(↑r : ℂ)‖ = r

Tactic:
(norm_real _).trans (abs_of_nonneg h)

Premises used: Complex.norm_real, abs_of_nonneg, Eq.trans
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
r : ℝ
a : (↑‖(↑r : ℂ)‖₊ : ℝ) = (↑‖r‖₊ : ℝ)
⊢ ‖(↑r : ℂ)‖₊ = ‖r‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
r : ℝ
⊢ (↑‖(↑r : ℂ)‖₊ : ℝ) = (↑‖r‖₊ : ℝ)

Tactic:
norm_real _

Premises used: Complex.norm_real, NNReal.toReal
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
r : ℝ
⊢ (↑‖(↑r : ℂ)‖₊ : ℝ) = (↑‖r‖₊ : ℝ)

Tactic:
exact norm_real _

Premises used: Complex.norm_real
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℕ
⊢ norm (E := ℂ) (↑n : ℂ) = (↑n : ℝ)

Tactic:
Complex.norm_of_nonneg n.cast_nonneg

Premises used: Nat.cast_nonneg, Complex.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ norm (E := ℂ) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
norm_natCast n

Premises used: Complex.norm_natCast
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
⊢ norm (E := ℂ) 2 = 2

Tactic:
norm_ofNat 2

Premises used: Complex.norm_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℕ
⊢ (↑(nnnorm (E := ℂ) (↑n : ℂ)) : ℝ) = (↑(↑n : NNReal) : ℝ)

Tactic:
simp [norm_natCast]

Premises used: Complex.norm_natCast
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ nnnorm (E := ℂ) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
nnnorm_natCast n

Premises used: Complex.nnnorm_natCast
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℤ
rw : ‖(↑(↑n : ℝ) : ℂ)‖ = |(↑n : ℝ)|
rw₁ : norm (E := ℝ) (↑n : ℝ) = |(↑n : ℝ)|
rw₂ rw₃ : Eq (α := ℝ) |(↑n : ℝ)| |(↑n : ℝ)|
⊢ norm (E := ℂ) (↑n : ℂ) = |(↑n : ℝ)|

Tactic:
rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]

Premises used: Complex.ofReal_intCast, Complex.norm_real, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
n : ℤ
hn : 0 ≤ n
rw : Eq (α := ℝ) |(↑n : ℝ)| (↑n : ℝ)
rw₁ : Eq (α := ℝ) (↑|n| : ℝ) (↑n : ℝ)
rw₂ rw₃ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
⊢ norm (E := ℂ) (↑n : ℂ) = (↑n : ℝ)

Tactic:
rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]

Premises used: Int.cast_abs, abs_of_nonneg, Complex.norm_intCast
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
q : ℚ
⊢ norm (E := ℂ) (↑q : ℂ) = |(↑q : ℝ)|

Tactic:
norm_real _

Premises used: Complex.norm_real
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
q : ℚ≥0
⊢ norm (E := ℂ) (↑q : ℂ) = (↑q : ℝ)

Tactic:
Complex.norm_of_nonneg q.cast_nonneg

Premises used: NNRat.cast_nonneg, Complex.norm_of_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
q : ℚ
⊢ nnnorm (E := ℂ) (↑q : ℂ) = nnnorm (E := ℝ) (↑q : ℝ)

Tactic:
nnnorm_real q

Premises used: Rat.cast, Complex.nnnorm_real
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
q : ℚ≥0
simp : NNReal.mk (↑q : ℝ) ⋯ = (↑q : NNReal)
⊢ nnnorm (E := ℂ) (↑q : ℂ) = (↑q : NNReal)

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
q : ℚ≥0
⊢ NNReal.mk (↑q : ℝ) ⋯ = (↑q : NNReal)

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ (normSq : (a : ℂ) → ℝ) z = HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
simp [norm_def, sq, Real.mul_self_sqrt (normSq_nonneg _)]

Premises used: Real.mul_self_sqrt, sq, Complex.norm_def, Complex.normSq_nonneg
-- Module: Mathlib.Analysis.Complex.Norm
Goal:
z : ℂ
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 = (normSq : (a : ℂ) → ℝ) z

Tactic:
(normSq_eq_norm_sq z).symm

Premises used: Complex.normSq_eq_norm_sq, Eq.symm