mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ Tendsto f (𝓝[<] R) (𝓝 (f R))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: f : ℝ → ℝ
c r R : ℝ
h₁f : ContinuousOn f (Ioc r R)
hR : r < R
h₂f : EqOn f (fun x ↦ c) (Ioo r R)
⊢ f R = c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
⊢ DifferentiableOn ℂ F (closure (ball c |R|))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
⊢ ∃ F, AnalyticOnNhd ℂ F univ ∧ (fun z ↦ (F z).re) = f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : E
c : ℂ
R : ℝ
⊢ circleAverage (fun x ↦ a) c R = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ AnalyticAt ℝ f x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
a : E
hf : ∀ x ∈ sphere c |R|, f x = a
⊢ circleAverage f c R = a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ 0 < (2 * π)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
x : ℝ
x✝ : x ∈ Ioo 0 (2 * π)
⊢ f₁ (circleMap c R x) ≤ f₂ (circleMap c R x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
h : ∀ x ∈ sphere c |R|, f₁ x ≤ f₂ x
⊢ circleAverage f₁ c R ≤ circleAverage f₂ c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ circleAverage f c R ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F✝ : Type u_1
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
inst✝ : CompleteSpace F✝
f : ℂ → F✝
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F✝
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + |R|) ⊆ {x | HarmonicAt (⇑g ∘ f) x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + |R|))
h₂F : Set.EqOn (fun z ↦ (F z).re) (⇑g ∘ f) (ball c (e + |R|))
h₃F : DifferentiableOn ℂ F (closure (ball c |R|))
h₄F : Set.EqOn (⇑Complex.reCLM ∘ F) (⇑g ∘ f) (sphere c |R|)
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere c |R|
⊢ x✝¹ ∈ ball c (e + |R|)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |circleAverage f c R| ≤ circleAverage |f| c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c |R|)
⊢ circleAverage f c R = f c

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
h₂f : ∀ x ∈ sphere c |R|, 0 ≤ f x
⊢ 0 ≤ circleAverage f c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
c : ℂ
R : ℝ
inst✝ : CompleteSpace E
L : E →L[ℝ] F
f : ℂ → E
hf : CircleIntegrable f c R
⊢ circleAverage (⇑L ∘ f) c R = L (circleAverage f c R)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
x : ℂ
hx : x ∈ {z | ‖z - c‖ ∈ Set.Ioc 0 |R|}
⊢ |R| ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝³ : NormedDivisionRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : NormSMulClass 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : ℂ → E
c : ℂ
R : ℝ
a : 𝕜
⊢ circleAverage (a • f) c R = a • circleAverage f c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
⊢ ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
h : CircleIntegrable f c R
g : StrongDual ℝ F
hR : ¬R = 0
H : ContinuousOn (circleAverage (⇑g ∘ f) c) (Set.Ioc 0 |R|)
⊢ 0 < |R|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ ‖f z‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ + f₂) c R = circleAverage f₁ c R + circleAverage f₂ c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℂ → F
c : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c |R|)
⊢ circleAverage f c R = f c

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ circleAverage (∑ i ∈ s, f i) c R = ∑ i ∈ s, circleAverage (f i) c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℂ
R : ℝ
ι : Type u_4
s : Finset ι
f : ι → ℂ → E
h : ∀ i ∈ s, CircleIntegrable (f i) c R
⊢ circleAverage (fun z ↦ ∑ i ∈ s, f i z) c R = ∑ i ∈ s, circleAverage (f i) c R

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f₁ f₂ : ℂ → E
c : ℂ
R : ℝ
hf₁ : CircleIntegrable f₁ c R
hf₂ : CircleIntegrable f₂ c R
⊢ circleAverage (f₁ - f₂) c R = circleAverage f₁ c R - circleAverage f₂ c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.im
hz_im : 0 ≤ z.re
w : ℂ
hw : w ∈ Ioi 0 ×ℂ Ioi 0
⊢ (fun x ↦ x * I) w ∈ Iio 0 ×ℂ Ioi 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: c w : ℂ
R : ℝ
x✝ : w ∈ ball c R
⊢ ∀ x ∈ {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}, x - c - (w - c) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: c w : ℂ
R : ℝ
x✝ : w ∈ ball c R
⊢ ContinuousOn (fun x ↦ ((x - c + (w - c)) / (x - c - (w - c))).re) {z | ‖z - c‖ ∈ Set.Ioc ‖w - c‖ R}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ closedBall c R ⊆ {x | HarmonicAt f x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
⊢ DifferentiableOn ℂ F (closure (ball c R))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
⊢ Set.EqOn (re ∘ herglotzRieszKernel c w • f) (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z)
    (sphere c R)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ 0 < Complex.I.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ 0 < { re := -1 / 2, im := √3 / 2 }.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ ↑ρ ^ 2 = -↑ρ - 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ ‖↑ρ‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ ↑z ∈ slitPlane

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: τ τ' : ℍ
hre : τ.re = τ'.re
hnorm : ‖↑τ‖ = ‖↑τ'‖
⊢ τ = τ'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ 0 < normSq ↑z

Tactic:
rw [Complex.normSq_pos]; exact z.ne_zero

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ 0 < normSq ↑z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ 0 < (-↑z)⁻¹.im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
z : ℍ
this : 0 < ↑n * z.im / normSq ↑z
⊢ 0 < (-↑n / ↑z).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
z : ℍ
⊢ 0 < (-↑n / ↑z).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
x : ℝ
⊢ (↑z).im ≠ (↑x).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x : { x // 0 < x }
z : ℍ
⊢ 0 < (↑x • ↑z).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x • z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x : ℝ
z : ℍ
⊢ 0 < (↑x + ↑z).im

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x y : ℝ
z : ℍ
⊢ (x + y) +ᵥ z = x +ᵥ y +ᵥ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x✝ : ℍ
⊢ 0 +ᵥ x✝ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: x y : ℝ
z : ℍ
⊢ x +ᵥ z = y +ᵥ z ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x +ᵥ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

Goal state before:
pp: ⊢ Set.range UpperHalfPlane.coe = ℍₒ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
a : ℤ
x✝ : ∃ n, ↑n = x + ↑a
n : ℤ
hn : ↑n = x + ↑a
⊢ ↑(n - a) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
a : ℤ
x✝ : ∃ n, ↑n = x
n : ℤ
hn : ↑n = x
⊢ ↑(n + a) = x + ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
a : ℤ
⊢ x + ↑a ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 0
⊢ ↑0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 1
⊢ ↑1 = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℤ
⊢ x ^ 2 ≠ ↑n ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: ⊢ {z | 0 < z.im} ∩ ℂ_ℤ = {z | 0 < z.im}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: z : ℍ
n : ℤ
hn : n ≠ 0
w✝ : ℤ
hm : ↑w✝ = ↑n / ↑z
⊢ (↑n / ↑z).im ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IntegerCompl

Goal state before:
pp: z : ℍ
n : ℤ
hn : n ≠ 0
⊢ ↑n / ↑z ∈ ℂ_ℤ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
⊢ ‖f z‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.IsIntegral

Goal state before:
pp: ⊢ IsIntegral ℤ I

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
⊢ MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
r : ℝ
hr : r ∈ Set.Ioo ‖w - c‖ R
⊢ w ∈ ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere c |R|
⊢ (poissonKernel c w • f) x✝¹ = (re ∘ herglotzRieszKernel c w • f) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere c |R|
⊢ (poissonKernel c w • f) x✝¹ = (re ∘ herglotzRieszKernel c w • f) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicContOnCl f (ball c R)
hw : w ∈ ball c R
⊢ circleAverage (poissonKernel c w • f) c R = f w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w : ℂ
⊢ herglotzRieszKernel c w = fun z ↦ (z - c + (w - c)) / (z - c - (w - c))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w z : ℂ
⊢ herglotzRieszKernel c w (z + c) = herglotzRieszKernel 0 (w - c) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w z : ℂ
⊢ poissonKernel c w z = (‖z - c‖ ^ 2 - ‖w - c‖ ^ 2) / ‖z - c - (w - c)‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ ((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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ (a.re * a.re + a.im * a.im - (b.re * b.re + b.im * b.im)) / ‖a - b‖ ^ 2 = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: a b : ℂ
⊢ ((a + b) / (a - b)).re = (‖a‖ ^ 2 - ‖b‖ ^ 2) / ‖a - b‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
hz_re : z.re ≤ 0
hz_im : z.im ≤ 0
⊢ ‖f z‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: c w : ℂ
⊢ poissonKernel c w = re ∘ herglotzRieszKernel c w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
⊢ (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
w : ℂ
hw : w ∈ Iio 0 ×ℂ Ioi 0
⊢ -w ∈ Ioi 0 ×ℂ Iio 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ r R : ℝ
h₁ : 0 < r
h₂ : r < R
h_cos : R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ) ≥ (R - r) ^ 2
h_subst : (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ)) ≤ (R + r) / (R - r)
this :
  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 (θ - φ)
⊢ (‖↑R * cexp (↑θ * I)‖ ^ 2 - ‖↑r * cexp (↑φ * I)‖ ^ 2) / ‖↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)‖ ^ 2 =
    (R ^ 2 - r ^ 2) / (R ^ 2 + r ^ 2 - 2 * R * r * Real.cos (θ - φ))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: φ θ 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)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: 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‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ 0 < R + r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ¬‖↑R * cexp (↑θ * I)‖ = ‖↑r * cexp (↑φ * I)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ‖-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))‖ ≤ R * r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
x : ℂ
h : ContDiffAt ℂ 2 f x
⊢ HarmonicAt f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ R ^ 2 + r ^ 2 - 2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re ≤ R ^ 2 + r ^ 2 + 2 * (R * r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
t₀ : g ⁻¹' (slitPlane ∩ {y | y ≠ 0}) ∈ 𝓝 z
⊢ Real.log ∘ ⇑normSq ∘ g =ᶠ[𝓝 z] ⇑reCLM ∘ ⇑ofRealCLM ∘ Real.log ∘ ⇑normSq ∘ g

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ R ^ 2 + r ^ 2 + 2 * (R * r) = (R + r) * (R + r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : 0 < x
⊢ x⁻¹ ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
⊢ x - 1 < x * log x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
⊢ x - 1 ≤ x * log x

Tactic:
rcases eq_or_ne x 1 with rfl | h1
  · simp
  · exact le_of_lt (self_sub_one_lt_mul_log h0 h1)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h0 : 0 ≤ x
⊢ x - 1 ≤ x * log x

Tactic:
by

Goal state after: