awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
j : Fin 2
⊢ ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have a₁ : ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).re -
        (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).im,
      (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).im +
        (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))).re]
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
    (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
j : Fin 2
a₁ :
  ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
have a₂ : ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).re -
        (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).im,
      (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).im +
        (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))).re]
    ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
    (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
⊢ Eq (α := ℝ)
    ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
      ℝ)
    (1 : ℝ)
have rw : (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im sorry) : Matrix (Fin 2) (Fin 2) ℝ) 0 0 *
      (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im sorry) : Matrix (Fin 2) (Fin 2) ℝ) 1 1 -
    (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im sorry) : Matrix (Fin 2) (Fin 2) ℝ) 0 1 *
      (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im sorry) : Matrix (Fin 2) (Fin 2) ℝ) 1 0 =
  1
Tactic: rw [← LinearMap.det_toMatrix basisOneI, toMatrix_rotation, Matrix.det_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
⊢ Eq (α := ℝˣ)
    ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) :
      ℝˣ)
    (1 : ℝˣ)
have rw : Eq (α := ℝ)
  (↑((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
    ℝ)
  (↑1 : ℝ)
Tactic: rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
rw :
  Eq (α := ℝ)
    (↑((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
          (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
      ℝ)
    (↑1 : ℝ)
⊢ Eq (α := ℝˣ)
    ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) :
      ℝˣ)
    (1 : ℝˣ)
have rw₁ : Eq (α := ℝ)
  ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
      (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
    ℝ)
  ((↑1 : ℝ) : ℝ)
Tactic: rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
rw :
  Eq (α := ℝ)
    (↑((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
          (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
      ℝ)
    (↑1 : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
      ℝ)
    ((↑1 : ℝ) : ℝ)
⊢ Eq (α := ℝˣ)
    ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) :
      ℝˣ)
    (1 : ℝˣ)
have rw₂ : Eq (α := ℝ) 1 (↑1 : ℝ)
Tactic: rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
rw :
  Eq (α := ℝ)
    (↑((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
          (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
      ℝ)
    (↑1 : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
      ℝ)
    ((↑1 : ℝ) : ℝ)
rw₂ : Eq (α := ℝ) 1 (↑1 : ℝ)
⊢ Eq (α := ℝˣ)
    ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) :
      ℝˣ)
    (1 : ℝˣ)
have rw₃ : Eq (α := ℝ) 1 1
Tactic: rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
⊢ ContinuousAt (herglotzLogIntegrand w ρ) z
have this : ‖z - ρ‖ ≠ 0
Tactic: have : ‖z - ρ‖ ≠ 0 := by simp_all [sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
⊢ ContinuousAt (herglotzLogIntegrand w ρ) z
have simp : ContinuousAt (HMul.hMul (α := ℂ → ℝ) (Complex.re ∘ fun (z : ℂ) ↦ (z + w) / (z - w)) fun (x : ℂ) ↦ log ‖x - ρ‖) z
Tactic: simp only [herglotzLogIntegrand, herglotzRieszKernel_fun_def, sub_zero, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
⊢ ContinuousAt (HMul.hMul (α := ℂ → ℝ) (Complex.re ∘ fun (z : ℂ) ↦ (z + w) / (z - w)) fun (x : ℂ) ↦ log ‖x - ρ‖) z
have funProp : z - w ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
⊢ Continuous (Y := ℝ) fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)
have rw : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
⊢ ContinuousAt (Y := ℝ) (fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) θ
have apply : circleMap 0 r θ ≠ w
Tactic: apply ContinuousAt.comp (continuousAt_herglotzLogIntegrand _ _) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
apply : circleMap 0 r θ ≠ w
⊢ ContinuousAt (Y := ℝ) (fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) θ
have apply₁ : circleMap 0 r θ ≠ ρ
Tactic: apply ContinuousAt.comp (continuousAt_herglotzLogIntegrand _ _) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
⊢ HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
    HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
have rw : (↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (circleMap 0 r₁ θ) : ℝ) ((normSq : (a : ℂ) → ℝ) ρ : ℝ) -
        2 * (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re) :
    ℂ) =
  (↑(HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)) : ℂ)
Tactic: rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
⊢ (↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (circleMap 0 r₁ θ) : ℝ) ((normSq : (a : ℂ) → ℝ) ρ : ℝ) -
          2 * (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re) :
      ℂ) =
    (↑(HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)) : ℂ)
have suffices : (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
Tactic: suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
| (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re
have rw : r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
Tactic: rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
⊢ (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
have conv_lhs : (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
Tactic: conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
conv_lhs :
  (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
⊢ (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
have conv_lhs₁ : r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
Tactic: conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have h_cos_law : ∀ (r₁ : ℝ),
  HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
    HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
Tactic: have h_cos_law (r₁ : ℝ) :
      ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - Complex.arg ρ) := by
    rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]
    suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
    conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
have rw : r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R
Tactic: rw [div_mul_eq_mul_div, div_le_iff₀ hR]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R
have nlinarith : HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R < r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 →
  HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R - r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 +
              (0 - (0 - HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) * (r₀ - r)) +
            -((0 - r₀) *
                  (HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 -
                    (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) R 2 - 2 * R * R * Real.cos (θ - ρ.arg))) -
                0) +
          ((0 - R) *
              (HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 -
                (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) R 2 - 2 * r * R * Real.cos (θ - ρ.arg))) -
            0) +
        -((r₀ - r) *
              (HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 -
                (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) R 2 - 2 * R * R * Real.cos (θ - ρ.arg))) -
            0) +
      (0 - (r - R) * (R * r - R * R)) =
    0
Tactic: nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
Tactic: have : (r₀ / R) * ‖circleMap 0 R θ - ρ‖ ^ 2 ≤ ‖circleMap 0 r θ - ρ‖ ^ 2 := by
    rw [div_mul_eq_mul_div, div_le_iff₀ hR]
    nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have grw : √(r₀ / R) * √(HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
Tactic: grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
grw : √(r₀ / R) * √(HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have grw₁ : √(r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
Tactic: grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
grw : √(r₀ / R) * √(HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₁ : √(r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have grw₂ : √(HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
Tactic: grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
grw : √(r₀ / R) * √(HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₁ : √(r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₂ : √(HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
have grw₃ : ‖circleMap 0 r θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
Tactic: grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 r θ)‖ ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have simp : |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
  (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
Tactic: simp only [herglotzLogIntegrand, Pi.smul_apply', Function.comp_apply, smul_eq_mul, norm_mul,
    norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have hrw : 0 < r₀ - ‖w‖
Tactic: have ⟨hrw, hr⟩ : 0 < r₀ - ‖w‖ ∧ 0 < r := by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have hr : 0 < r
Tactic: have ⟨hrw, hr⟩ : 0 < r₀ - ‖w‖ ∧ 0 < r := by grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
Tactic: have h_norm_sub₁ := const_mul_norm_sub_circleMap_le_norm_sub_circleMap hρ hr₀ hR hr₀r hrR θ
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
Tactic: have h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖ := lt_of_lt_of_le (by positivity) h_norm_sub₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have h₁ : |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h₁ : |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)
have h₂ : |log ‖circleMap 0 r θ - ρ‖| ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
have h₁ : |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
Tactic: simp only [herglotzRieszKernel_def, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
have grw : ‖(circleMap 0 r θ + w) / (circleMap 0 r θ - w)‖ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
Tactic: grw [Complex.abs_re_le_norm, norm_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
grw : ‖(circleMap 0 r θ + w) / (circleMap 0 r θ - w)‖ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
have grw₁ : ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
Tactic: grw [Complex.abs_re_le_norm, norm_div]