awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
⊢ ∃ c < 2, ∃ (B : ℝ), IsBigO (F := ℝ) (cobounded ℂ ⊓ 𝓟 {z : ℂ | 0 < z.re}) (f - g) fun (z : ℂ) ↦ expR (B * ‖z‖ ^ c)

Tactic:
exact isBigO_sub_exp_rpow hfexp hgexp

Premises used: PhragmenLindelof.isBigO_sub_exp_rpow
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
hfim : ∃ (C : ℝ), ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ C
hgim : ∃ (C : ℝ), ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ C
refine_2 : ∀ (Cf : ℝ) (hCf : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ Cf), ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
rcases hfim with ⟨Cf, hCf⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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
refine_2 : ∀ (Cg : ℝ) (hCg : ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ Cg), ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
rcases hgim with ⟨Cg, hCg⟩
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
Cf : ℝ
hCf : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ Cf
Cg : ℝ
hCg : ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ Cg
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
⟨Cf + Cg, fun x => norm_sub_le_of_le (hCf x) (hCg x)⟩

Premises used: norm_sub_le_of_le, HAdd.hAdd, Exists.intro
-- Module: Mathlib.Analysis.Complex.PhragmenLindelof
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 : ℂ)‖
Cf : ℝ
hCf : ∀ (x : ℝ), ‖f ((↑x : ℂ) * I)‖ ≤ Cf
Cg : ℝ
hCg : ∀ (x : ℝ), ‖g ((↑x : ℂ) * I)‖ ≤ Cg
⊢ ∃ (C : ℝ), ∀ (x : ℝ), ‖(f - g) ((↑x : ℂ) * I)‖ ≤ C

Tactic:
exact ⟨Cf + Cg, fun x => norm_sub_le_of_le (hCf x) (hCg x)⟩
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w : ℂ
h : ∀ (z : ℂ), herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))
⊢ herglotzRieszKernel c w = fun (z : ℂ) ↦ (z - c + (w - c)) / (z - c - (w - c))

Tactic:
ext z
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

Tactic:
herglotzRieszKernel_def c w z

Premises used: herglotzRieszKernel_def
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

Tactic:
exact herglotzRieszKernel_def c w z

Premises used: herglotzRieszKernel_def
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w z : ℂ
⊢ herglotzRieszKernel c w (z + c) = herglotzRieszKernel 0 (w - c) z

Tactic:
simp [herglotzRieszKernel_fun_def]

Premises used: herglotzRieszKernel_fun_def
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w z : ℂ
⊢ poissonKernel c w z =
    (HPow.hPow (β := ℕ) ‖z - c‖ 2 - HPow.hPow (β := ℕ) ‖w - c‖ 2) / HPow.hPow (β := ℕ) ‖z - c - (w - c)‖ 2

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
a b : ℂ
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
⊢ ((a + b) / (a - b)).re = (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]

Premises used: Complex.add_im, Complex.sub_im, Complex.sub_re, HSub.hSub, Complex.normSq_eq_norm_sq, Complex.add_re, Complex.div_re, add_div
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
a b : ℂ
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)
⊢ ((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:
congr! 1
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
a b : ℂ
⊢ (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:
ring
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
a b : ℂ
⊢ (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:
simp [← normSq_apply, normSq_eq_norm_sq]

Premises used: Complex.normSq_eq_norm_sq, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Poisson
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
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
⊢ ((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:
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]

Premises used: Norm.norm, HMul.hMul, Complex.im, HSub.hSub, Complex.re, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
c w : ℂ
h : ∀ (z : ℂ), poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
⊢ poissonKernel c w = re ∘ herglotzRieszKernel c w

Tactic:
ext z
-- Module: Mathlib.Analysis.Complex.Poisson
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
h₃ 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
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z

Tactic:
rw [Function.comp_apply, poissonKernel, herglotzRieszKernel,
    poissonKernel_eq_re_herglotzRieszKernel_aux]

Premises used: _private.0.poissonKernel_eq_re_herglotzRieszKernel_aux, poissonKernel, Function.comp_apply, herglotzRieszKernel
-- Module: Mathlib.Analysis.Complex.Poisson
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
nlinarith₁ nlinarith₂ :
  HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) < HPow.hPow (β := ℕ) (R - r) 2 →
    GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ) ≥ HPow.hPow (β := ℕ) (R - r) 2

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂), Real.cos_le_one (θ - φ)]

Premises used: Iff.mpr, sub_pos, HSub.hSub, mul_pos, Real.cos_le_one
-- Module: Mathlib.Analysis.Complex.Poisson
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

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 (θ - φ)]
-- Module: Mathlib.Analysis.Complex.Poisson
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 (θ - φ)
hd : 0 < R - r
⊢ (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:
rw [div_le_div_iff₀]

Premises used: div_le_div_iff₀
-- Module: Mathlib.Analysis.Complex.Poisson
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
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
⊢ (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:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

Premises used: Iff.mpr, sub_pos, mul_pos
-- Module: Mathlib.Analysis.Complex.Poisson
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 :
  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
⊢ 0 < HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

Premises used: Iff.mpr, sub_pos, mul_pos
-- Module: Mathlib.Analysis.Complex.Poisson
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 ≤ 0 → r - R + (R - r - 0) = 0
⊢ 0 < R - r

Tactic:
nlinarith [mul_pos h₁ (sub_pos.mpr h₂)]

Premises used: Iff.mpr, sub_pos, mul_pos
-- Module: Mathlib.Analysis.Complex.Poisson
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)

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₂)]
-- Module: Mathlib.Analysis.Complex.Poisson
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 2 - HPow.hPow (β := ℕ) r 2) /
      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) r 2 - 2 * R * r * Real.cos (θ - φ)) ≤
    (R + r) / (R - r)

Tactic:
h_subst
-- Module: Mathlib.Analysis.Complex.Poisson
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)
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 (θ - φ))
⊢ (((↑R : ℂ) * cexp ((↑θ : ℂ) * I) + (↑r : ℂ) * cexp ((↑φ : ℂ) * I)) *
        ((↑R : ℂ) * cexp ((↑θ : ℂ) * I) - (↑r : ℂ) * cexp ((↑φ : ℂ) * I))⁻¹).re ≤
    (R + r) / (R - r)

Tactic:
convert! h_subst using 1
-- Module: Mathlib.Analysis.Complex.Poisson
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)
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 (θ - φ))
⊢ (((↑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:
rw [← div_eq_mul_inv, poissonKernel_eq_re_herglotzRieszKernel_aux]

Premises used: _private.0.poissonKernel_eq_re_herglotzRieszKernel_aux, div_eq_mul_inv
-- Module: Mathlib.Analysis.Complex.Poisson
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 (θ - φ)
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 φ)))
⊢ (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 [← this]
-- Module: Mathlib.Analysis.Complex.Poisson
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) /
      (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:
simp [← normSq_eq_norm_sq, Complex.normSq_sub]

Premises used: Complex.normSq_eq_norm_sq, Complex.normSq_sub
-- Module: Mathlib.Analysis.Complex.Poisson
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)
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 (θ - φ)
⊢ (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:
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]
-- Module: Mathlib.Analysis.Complex.Poisson
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)
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 φ)
⊢ 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:
simp [normSq_eq_norm_sq, Real.cos_sub]

Premises used: Complex.normSq_eq_norm_sq, Real.cos_sub
-- Module: Mathlib.Analysis.Complex.Poisson
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 * 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:
ring
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0

Tactic:
grind [ball_eq_empty, mem_sphere, dist_eq_norm, norm_pos_iff]

Premises used: norm_pos_iff, dist_eq_norm, Metric.mem_sphere, Metric.ball_eq_empty
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
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‖)
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (R + ‖w - c‖) / (R - ‖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]

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Poisson
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‖)
neg : ∀ (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‖)

Tactic:
by_cases h₁w : ‖w - c‖ = 0
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ‖w - c‖ = 0
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ 0 < ‖w - c‖

Tactic:
simpa using h₁w