awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.PhragmenLindelof (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfd : DiffContOnCl ℂ f {z : ℂ | 0 < z.re}
hgd : DiffContOnCl ℂ g {z : ℂ | 0 < z.re}
hfexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) f fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hgexp : ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) g fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun (x : ℝ) ↦ ‖f (↑x : ℂ) - g (↑x : ℂ)‖
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
Cf : ℝ
hCf : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ Cf
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
have refine_2 : ∀ (Cg : ℝ) (hCg : ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ Cg), ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
Tactic: rcases hgim with ⟨Cg, hCg⟩
Cleared hypotheses: hgim
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w : ℂ
⊢ herglotzRieszKernel c w = fun (z : ℂ) ↦ (z - c + (w - c)) / (z - c - (w - c))
have h : ∀ (z : ℂ), herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
a b : ℂ
⊢ ((a + b) / (a - b)).re = (HPow.hPow (β := ℕ) ‖a‖ 2 - HPow.hPow (β := ℕ) ‖b‖ 2) / HPow.hPow (β := ℕ) ‖a - b‖ 2
have rw : ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
  (HPow.hPow (β := ℕ) ‖a‖ 2 - HPow.hPow (β := ℕ) ‖b‖ 2) / HPow.hPow (β := ℕ) ‖a - b‖ 2
Tactic: rw [div_re, normSq_eq_norm_sq (a - b), ← add_div, add_re, sub_re, add_im, sub_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
a b : ℂ
⊢ ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
    (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2
have h : (a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im) = a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
a b : ℂ
⊢ ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
    (HPow.hPow (β := ℕ) ‖a‖ 2 - HPow.hPow (β := ℕ) ‖b‖ 2) / HPow.hPow (β := ℕ) ‖a - b‖ 2
have calc : ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
  (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2
Tactic: calc ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / ‖a - b‖ ^ 2
    _ = ((a.re * a.re + a.im * a.im) - (b.re * b.re + b.im * b.im)) / ‖a - b‖ ^ 2 := by
      congr! 1; ring
    _ = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2 := by
      simp [← normSq_apply, normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
a b : ℂ
calc :
  ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
    (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2
⊢ ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
    (HPow.hPow (β := ℕ) ‖a‖ 2 - HPow.hPow (β := ℕ) ‖b‖ 2) / HPow.hPow (β := ℕ) ‖a - b‖ 2
have calc₁ : (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / HPow.hPow (β := ℕ) ‖a - b‖ 2 =
  (HPow.hPow (β := ℕ) ‖a‖ 2 - HPow.hPow (β := ℕ) ‖b‖ 2) / HPow.hPow (β := ℕ) ‖a - b‖ 2
Tactic: calc ((a.re + b.re) * (a.re - b.re) + (a.im + b.im) * (a.im - b.im)) / ‖a - b‖ ^ 2
    _ = ((a.re * a.re + a.im * a.im) - (b.re * b.re + b.im * b.im)) / ‖a - b‖ ^ 2 := by
      congr! 1; ring
    _ = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2 := by
      simp [← normSq_apply, normSq_eq_norm_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w : ℂ
⊢ poissonKernel c w = re ∘ herglotzRieszKernel c w
have h : ∀ (z : ℂ), poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w z : ℂ
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
have h : poissonKernel c w z = (herglotzRieszKernel c w z).re
Tactic: rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w z : ℂ
h : poissonKernel c w z = (herglotzRieszKernel c w z).re
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
have h₁ : (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
  (herglotzRieszKernel c w z).re
Tactic: rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w z : ℂ
h : poissonKernel c w z = (herglotzRieszKernel c w z).re
h₁ :
  (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
    (herglotzRieszKernel c w z).re
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
have h₂ : (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
  ((z - c + (w - c)) / (z - c - (w - c))).re
Tactic: rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
c w z : ℂ
h : poissonKernel c w z = (herglotzRieszKernel c w z).re
h₁ :
  (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
    (herglotzRieszKernel c w z).re
h₂ :
  (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
    ((z - c + (w - c)) / (z - c - (w - c))).re
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
have h₃ : (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2 =
  (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2
Tactic: rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
have nlinarith : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) < HPow.hPow (β := ℕ) (R - r) 2 →
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) - HPow.hPow (β := ℕ) (R - r) 2 +
        2 * (0 - (0 - HPow.hPow (β := ℕ) r 2) * (Real.cos (θ - φ) - 1)) +
      2 * (0 - (0 - r * (R - r)) * (Real.cos (θ - φ) - 1)) =
    0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂), Real.cos_le_one (θ - φ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
nlinarith :
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) < HPow.hPow (β := ℕ) (R - r) 2 →
    HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) - HPow.hPow (β := ℕ) (R - r) 2 +
          2 * (0 - (0 - HPow.hPow (β := ℕ) r 2) * (Real.cos (θ - φ) - 1)) +
        2 * (0 - (0 - r * (R - r)) * (Real.cos (θ - φ) - 1)) =
      0
⊢ HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
have nlinarith₁ : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) < HPow.hPow (β := ℕ) (R - r) 2 →
  GT.gt (α := ℝ) 2 0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂), Real.cos_le_one (θ - φ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re ≤
    (R + r) / (R - r)
have h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
Tactic: have h_cos : (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≥ (R - r) ^ 2 := by
    nlinarith [mul_pos h₁ (sub_pos.mpr h₂), Real.cos_le_one (θ - φ)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
⊢ (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
have rw : (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) ≤
  (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
Tactic: rw [div_le_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
rw :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) ≤
    (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
⊢ (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
have hb : 0 < HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
Tactic: rw [div_le_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
rw :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) ≤
    (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
hb : 0 < HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
⊢ (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
have hd : 0 < R - r
Tactic: rw [div_le_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
⊢ (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) ≤
    (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
have nlinarith : (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) <
    (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) →
  (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) -
          (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) +
        2 *
          (0 -
            (0 - r) *
              (HPow.hPow (β := ℕ) (R - r) 2 -
                (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)))) +
      (0 -
        (r - R) *
          (HPow.hPow (β := ℕ) (R - r) 2 -
            (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)))) =
    0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
nlinarith :
  (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) <
      (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) →
    (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) -
            (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) +
          2 *
            (0 -
              (0 - r) *
                (HPow.hPow (β := ℕ) (R - r) 2 -
                  (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)))) +
        (0 -
          (r - R) *
            (HPow.hPow (β := ℕ) (R - r) 2 -
              (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)))) =
      0
⊢ (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) ≤
    (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
have nlinarith₁ : (R + r) * (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) <
    (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) * (R - r) →
  GT.gt (α := ℝ) 2 0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
⊢ 0 < HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
have nlinarith : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≤ 0 →
  HPow.hPow (β := ℕ) (R - r) 2 - (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) +
        (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) - 0) +
      (0 - (r - R) * (r - R)) =
    0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
⊢ 0 < R - r
have nlinarith : R - r ≤ 0 → r - R + (R - r - 0) = 0
Tactic: nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (hypothesis)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
⊢ (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re ≤
    (R + r) / (R - r)
have h_subst : (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
    (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
  (R + r) / (R - r)
Tactic: have h_subst :
      (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r) := by
    rw [div_le_div_iff₀] <;> nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
h_subst :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
⊢ (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re ≤
    (R + r) / (R - r)
have h : (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
      ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re =
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
    (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
Tactic: convert! h_subst using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
h_subst :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
⊢ (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re =
    (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
have h : (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
    HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 =
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
    (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
Tactic: rw [← div_eq_mul_inv, poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
h_subst :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
this :
  HMul.hMul (β := ℝ) (R * R) ((normSq : (a : ℂ) → ℝ) (cexp ((↑θ : ℂ) * I)) : ℝ) +
        HMul.hMul (β := ℝ) (r * r) ((normSq : (a : ℂ) → ℝ) (cexp ((↑φ : ℂ) * I)) : ℝ) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
⊢ (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
      HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 =
    (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
have rw : (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
    HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 =
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
    (HMul.hMul (β := ℝ) (R * R) ((normSq : (a : ℂ) → ℝ) (cexp ((↑θ : ℂ) * I)) : ℝ) +
        HMul.hMul (β := ℝ) (r * r) ((normSq : (a : ℂ) → ℝ) (cexp ((↑φ : ℂ) * I)) : ℝ) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
h_subst :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
⊢ (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
      HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2 =
    (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ))
have h : HMul.hMul (β := ℝ) (R * R) ((normSq : (a : ℂ) → ℝ) (cexp ((↑θ : ℂ) * I)) : ℝ) +
      HMul.hMul (β := ℝ) (r * r) ((normSq : (a : ℂ) → ℝ) (cexp ((↑φ : ℂ) * I)) : ℝ) -
    2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
Tactic: suffices (R * R * normSq (cexp (θ * I)) + r * r * normSq (cexp (φ * I)) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ))) =
      (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) by
    rw [← this]; simp [← normSq_eq_norm_sq, Complex.normSq_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2
h_subst :
  (HPow.hPow (β := ℕ) R 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)
⊢ HMul.hMul (β := ℝ) (R * R) ((normSq : (a : ℂ) → ℝ) (cexp ((↑θ : ℂ) * I)) : ℝ) +
        HMul.hMul (β := ℝ) (r * r) ((normSq : (a : ℂ) → ℝ) (cexp ((↑φ : ℂ) * I)) : ℝ) -
      2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
    HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)
have h : R * R + r * r - 2 * (R * Real.cos θ * (r * Real.cos φ) + R * Real.sin θ * (r * Real.sin φ)) =
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * (Real.cos θ * Real.cos φ + Real.sin θ * Real.sin φ)
Tactic: simp [normSq_eq_norm_sq, Real.cos_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (R + ‖w - c‖) / (R - ‖w - c‖)
have obtain : ∀ (η₂ : z - c ≠ 0) (hz : z ∈ sphere c ‖z - c‖) (hw : w ∈ ball c ‖z - c‖) (η₀ : 0 < ‖z - c‖),
  ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
Tactic: obtain ⟨η₀, rfl, η₂⟩ : 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0 := by
    grind [ball_eq_empty, mem_sphere, dist_eq_norm, norm_pos_iff]
Cleared hypotheses: R, hz, hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
have pos : ∀ (h₁w : ‖w - c‖ = 0), ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
Tactic: by_cases h₁w : ‖w - c‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
pos : ∀ (h₁w : ‖w - c‖ = 0), ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
have neg : ∀ (h₁w : ¬‖w - c‖ = 0), ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
Tactic: by_cases h₁w : ‖w - c‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (R - r) / (R + r) ≤
    (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) /
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))).re
have rw : (R - r) / (R + r) ≤
  (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
    HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
Tactic: rw [poissonKernel_eq_re_herglotzRieszKernel_aux]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (R - r) / (R + r) ≤
    (HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I)‖ 2 - HPow.hPow (β := ℕ) ‖(↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2) /
      HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
have simp : (R - r) / (R + r) ≤
  (R + r) * (R - r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
Tactic: simp only [Complex.norm_mul, norm_real, norm_eq_abs, norm_exp_ofReal_mul_I, mul_one, sq_abs,
    sq_sub_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ (R - r) / (R + r) ≤
    (R + r) * (R - r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
have field_simp : 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp (I * (↑φ : ℂ))‖ 2
Tactic: field_simp [sub_pos.mpr h₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp (I * (↑φ : ℂ))‖ 2
have simp : 1 / (R + r) ≤ (R + r) / HPow.hPow (β := ℕ) ‖(↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I)‖ 2
Tactic: simp only [mul_comm I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < R + r
have positivity : 0 < R → 0 < R + r
Tactic: positivity [h₁.trans h₂]