mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: t : |2⁻¹| = 2⁻¹
z : |log 2 - 429895798851992810179897 / 620208537104218167705600| ≤ 1 / 17179869184
⊢ |429895798851992810179897 / 620208537104218167705600 - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34

Tactic:
norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 287209 / 414355 < 0.6931471808

Tactic:
norm_num

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

Goal state before:
pp: ⊢ |2 / 3| = 2 / 3

Tactic:
norm_num

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

Goal state before:
pp: t : |2 / 3| = 2 / 3
⊢ |2 / 3| < 1

Tactic:
norm_num

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

Goal state before:
pp: t : |2 / 3| = 2 / 3
z : |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / (↑i + 1) + log (1 - 2 / 3)| ≤ (2 / 3) ^ (70 + 1) / (1 - 2 / 3)
⊢ 1 - 2 / 3 = 1 / 3

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
a : A
⊢ Continuous[_, inst✝²] fun x ↦ (cov.liftHomotopy H f H_0) (x, a)

Tactic:
liftHomotopy_apply

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
a : A
⊢ Continuous[_, inst✝²] fun x ↦
    (cov.liftPath (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f a) ⋯) x
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 109861228867 / 100000000000 < 1.0986122888

Tactic:
norm_num

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

Goal state before:
pp: ⊢ |4 / 5| = 4 / 5

Tactic:
norm_num

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

Goal state before:
pp: t : |4 / 5| = 4 / 5
⊢ |4 / 5| < 1

Tactic:
norm_num

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

Goal state before:
pp: t : |4 / 5| = 4 / 5
z : |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / (↑i + 1) + log (1 - 4 / 5)| ≤ (4 / 5) ^ (130 + 1) / (1 - 4 / 5)
⊢ 1 - 4 / 5 = 1 / 5

Tactic:
norm_num

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

Goal state before:
pp: ⊢ 1 / 10 ^ 10 + 160943791243 / 100000000000 < 1.6094379126

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
x y : X
γ : Path.Homotopic.Quotient x y
ex : ↑(p ⁻¹' {x})
ey : ↑(p ⁻¹' {y})
Γ : Path.Homotopic.Quotient ↑ex ↑ey
eq : Γ.map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
e_1✝ : ↑(p ⁻¹' {{ toFun := p, continuous_toFun := ⋯ } ↑ey}) = ↑(p ⁻¹' {y})
e_7✝ : { toFun := p, continuous_toFun := ⋯ } ↑ex = x
e_8✝ : { toFun := p, continuous_toFun := ⋯ } ↑ey = y
⊢ γ.cast ⋯ ⋯ ≍ γ

Tactic:
exact γ.cast_heq ..

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_2.mk
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
w✝ : FundamentalGroup E e₀
pΓΓ' : Path { as := e₀ }.as { as := e₀ }.as
eq :
  (Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid { as := e₀ }.as { as := e₀ }.as)) pΓΓ')
          { toFun := p, continuous_toFun := ⋯ }).cast
      ⋯ ⋯ =
    (FundamentalGroup.map f a₀) (fromPath (Path.Homotopic.Quotient.mk pγγ'))
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩

Tactic:
map_apply,

Goal state after:
case refine_2.mk
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
γ γ' : C(↑I, A)
Γ Γ' : C(↑I, E)
γ_0 : γ 0 = a₀
γ'_0 : γ' 0 = a₀
Γ_0 : Γ 0 = e₀
Γ'_0 : Γ' 0 = e₀
Γ_lifts : p ∘ ⇑Γ = ⇑(f.comp γ)
Γ'_lifts : p ∘ ⇑Γ' = ⇑(f.comp γ')
γγ'1 : γ 1 = γ' 1
pγ : Path a₀ (γ 1) := { toContinuousMap := γ, source' := γ_0, target' := ⋯ }
pγ' : Path a₀ (γ 1) := { toContinuousMap := γ', source' := γ'_0, target' := ⋯ }
pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
w✝ : FundamentalGroup E e₀
pΓΓ' : Path { as := e₀ }.as { as := e₀ }.as
eq :
  (Path.Homotopic.Quotient.map (Quot.mk (⇑(Path.Homotopic.setoid { as := e₀ }.as { as := e₀ }.as)) pΓΓ')
          { toFun := p, continuous_toFun := ⋯ }).cast
      ⋯ ⋯ =
    Path.Homotopic.Quotient.map (fromPath (Path.Homotopic.Quotient.mk pγγ')) f
⊢ cov.monodromy (Path.Homotopic.Quotient.mk (pγγ'.map ⋯)) ⟨e₀, he⟩ = id ⟨e₀, he⟩
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
inst✝ : SimplyConnectedSpace E
e : ↑(p ⁻¹' {x}) := ⟨⋯.choose, ⋯⟩
⊢ (⋯.monodromyPerm x).ker = ⊥

Tactic:
hp.ker_monodromyPerm e

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
inst✝ : SimplyConnectedSpace E
e : ↑(p ⁻¹' {x}) := ⟨⋯.choose, ⋯⟩
⊢ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range = ⊥
Module: Mathlib.Analysis.Complex.HalfPlane

Goal state before:
pp: x : ℝ
⊢ IsOpen {z | z.im < x}

Tactic:
simpa using isOpen_im_lt_EReal x

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

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ ((↑z.re + ↑y * I).re - c.re) ^ 2 + ((↑z.re + ↑y * I).im - c.im) ^ 2 ≤ (z.re - c.re) ^ 2 + (z.im - c.im) ^ 2

Tactic:
suffices (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2 by simpa

Goal state after:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ (y - c.im) ^ 2 ≤ (z.im - c.im) ^ 2
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
x : ℝ
hx : x ∈ Ioi 0
⊢ z.re ≠ 0

Tactic:
simpa using (ne_comm.mpr (ne_of_lt hz.1))

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ z.re ≠ 0

Tactic:
simpa using (ne_comm.mpr (ne_of_lt hz.1))

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f₁ f₂ : E → F
x : E
h₁ : HarmonicAt f₁ x
h₂ : HarmonicAt f₂ x
⊢ HarmonicAt (f₁ - f₂) x

Tactic:
by
  constructor
  · exact h₁.1.sub h₂.1
  · filter_upwards [h₁.1.laplacian_sub_nhds h₂.1, h₁.2, h₂.2]
    simp_all

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

Goal state before:
pp: case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ Δ (-f) =ᶠ[𝓝 x] 0

Tactic:
· filter_upwards [h.2] with x hx
    simp_all [laplacian_neg]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ (fun w ↦ (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - (w - z).re • f z) =o[𝓝 z] fun w ↦ w - z

Tactic:
suffices (fun x ↦ (∫ t in z.re..x, f (t + z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re]
      fun x ↦ x - z.re from
    this.comp_tendsto (continuous_re.tendsto z) |>.trans_isBigO isBigO_re_sub_re

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
⊢ (fun x ↦ (∫ (t : ℝ) in z.re..x, f (↑t + ↑z.im * I)) - (x - z.re) • f z) =o[𝓝 z.re] fun x ↦ x - z.re
Module: Mathlib.Analysis.Complex.Harmonic.Analytic

Goal state before:
pp: case e_a
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
h₂f : Laplacian.laplacian f x = 0 x
⊢ -(I * ↑(((fderiv ℝ (fderiv ℝ f) x) I) I)) = I * ↑(((fderiv ℝ (fderiv ℝ f) x) 1) 1)

Tactic:
simp only [laplacian_eq_iteratedFDeriv_complexPlane, iteratedFDeriv_two_apply, Fin.isValue,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, Pi.zero_apply,
      add_eq_zero_iff_eq_neg] at h₂f

Goal state after:
case e_a
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun z ↦ ↑((fderiv ℝ f z) 1) - I * ↑((fderiv ℝ f z) I)) =
    (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
h₁f : ContDiffAt ℝ 2 f x
h₂f : ((fderiv ℝ (fderiv ℝ f) x) 1) 1 = -((fderiv ℝ (fderiv ℝ f) x) I) I
⊢ -(I * ↑(((fderiv ℝ (fderiv ℝ f) x) I) I)) = I * ↑(((fderiv ℝ (fderiv ℝ f) x) 1) 1)
Module: Mathlib.Analysis.Complex.MeanValue

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : ¬|R| ≤ 0
⊢ ∀ z ∈ ball c |R| \ ∅, DifferentiableAt ℂ f z

Tactic:
· intro z hz
    rw [sdiff_empty] at hz
    apply (hf.1 z hz).differentiableAt (isOpen_ball.mem_nhds hz)

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

Goal state before:
pp: ⊢ IsIntegral ℤ I

Tactic:
refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩
  rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]

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:
ext z

Goal state after:
c w z : ℂ
⊢ herglotzRieszKernel c w z = (z - c + (w - c)) / (z - c - (w - c))
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
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
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ Neg.neg) (↑x * I)‖ ≤ C

Tactic:
· rw [comp_apply, ← neg_mul, ← ofReal_neg]
    exact him (-x) (neg_nonpos.2 hx)

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

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

Tactic:
ext z

Goal state after:
c w z : ℂ
⊢ poissonKernel c w z = (re ∘ herglotzRieszKernel c w) z
Module: Mathlib.Analysis.Complex.Poisson

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

Tactic:
have key := calc
    (-(R * cexp (θ * I) * (starRingEnd ℂ) (r * cexp (φ * I)))).re ≤ _ := re_le_norm _
    _ ≤ R * r := by simp [abs_of_pos, h₁, h₁.trans h₂]

Goal state after:
θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
key : (-(↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I)))).re ≤ R * r
⊢ 1 *
      (‖↑R * cexp (↑θ * I)‖ ^ 2 + ‖↑r * cexp (↑φ * I)‖ ^ 2 -
        2 * (↑R * cexp (↑θ * I) * (starRingEnd ℂ) (↑r * cexp (↑φ * I))).re) ≤
    (R + r) * (R + r)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
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
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖(f ∘ Neg.neg) (↑x * I)‖ ≤ C

Tactic:
· rw [comp_apply, ← neg_mul, ← ofReal_neg]
    exact him (-x) (neg_nonpos.2 hx)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c

Tactic:
rw [IntervalIntegrable.iff_comp_neg, neg_zero]

Goal state after:
case inr
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ (-x) ^ r) volume 0 (-c)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: ⊢ Continuous sinc

Tactic:
refine continuous_iff_continuousAt.mpr fun x ↦ ?_

Goal state after:
x : ℝ
⊢ ContinuousAt sinc x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c

Tactic:
rw [IntervalIntegrable.iff_comp_neg, neg_zero]

Goal state after:
case inr
a b : ℝ
r : ℂ
h : -1 < r.re
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (fun x ↦ ↑(-x) ^ r) volume 0 (-c)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
apply hf.circleAverage_re_herglotzRieszKernel_smul hw

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hbc
a b x : ℝ
hx : 0 < x
⊢ IntervalIntegrable log volume 1 x

Tactic:
· -- Show integrability on [1…t] by continuity
    apply ContinuousOn.intervalIntegrable
    apply Real.continuousOn_log.mono
    apply Set.notMem_uIcc_of_lt zero_lt_one at hx
    simpa

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

Goal state before:
pp: x : ℝ
⊢ log⁺ x - log⁺ x⁻¹ = log x

Tactic:
rw [posLog_apply, posLog_apply, log_inv]
  by_cases! h : 0 ≤ log x
  · simp [h]
  · simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
hg : CircleIntegrable f 0 R
hw : w ∈ ball 0 R
hR : 0 < R
d : ℝ
hd : d > 0
hsub : ball w d ⊆ ball 0 R
hdist : ∀ x ∈ ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap 0 R θ - x‖
hgm : AEStronglyMeasurable (fun θ ↦ f (circleMap 0 R θ)) (volume.restrict (uIoc 0 (2 * π)))
θ : ℝ
a✝ : θ ∈ uIoc 0 (2 * π)
x : ℂ
hx : x ∈ ball w d
⊢ ‖2‖ = 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, x ^ r ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re

Tactic:
rpow_def,

Goal state after:
case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, (↑x ^ ↑r).re ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume).re
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: this✝ : AnalyticOnNhd ℝ (fun x ↦ 4 * sin x ^ 2) Set.univ
this : ((fun x ↦ 4 * sin x ^ 2) ⁻¹' {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : ¬sin a = 0
⊢ log (4 * sin a ^ 2) = log 4 + 2 * log (sin a)

Tactic:
log_mul (by simp) (by simp_all),

Goal state after:
this✝ : AnalyticOnNhd ℝ (fun x ↦ 4 * sin x ^ 2) Set.univ
this : ((fun x ↦ 4 * sin x ^ 2) ⁻¹' {0})ᶜ ∈ codiscrete ℝ
a : ℝ
ha : ¬sin a = 0
⊢ log 4 + log (sin a ^ 2) = log 4 + 2 * log (sin a)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 1 + 1 - 2 * cos x = 2 - 2 * cos x

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (fun z ↦ log ‖↑R * z + c - a‖) = fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖

Tactic:
ext z

Goal state after:
case e_f
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
⊢ log ‖↑R * z + c - a‖ = log ‖↑R * (z + ↑R⁻¹ * (c - a))‖
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case h
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
z₁ : ℂ
hz₁ : z₁ ∈ sphere 0 1 \ {z | ¬z + (↑R)⁻¹ * (c - a) = 0}
z₂ : ℂ
hz₂ : z₂ ∈ sphere 0 1 \ {z | ¬z + (↑R)⁻¹ * (c - a) = 0}
⊢ z₁ = z₂

Tactic:
simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_sdiff,
        Set.mem_ofPred_eq, Decidable.not_not]

Goal state after:
case h
a c : ℂ
R : ℝ
z z₁ z₂ : ℂ
hR : ¬R = 0
hz : ‖z‖ = 1
hz₁ : ‖z₁‖ = 1 ∧ z₁ + (↑R)⁻¹ * (c - a) = 0
hz₂ : ‖z₂‖ = 1 ∧ z₂ + (↑R)⁻¹ * (c - a) = 0
⊢ z₁ = z₂
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = log R

Tactic:
rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left,
    posLog_eq_zero_iff, abs_mul, abs_inv, abs_of_nonneg (norm_nonneg (c - a))]

Goal state after:
case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R|⁻¹ * ‖c - a‖ ≤ 1
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
⊢ 𝓝 (f z₀) ≤ map f (𝓝 z₀)

Tactic:
refine (nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
hf : AnalyticAt ℂ f z₀
h : ¬∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
R : ℝ
hR : 0 < R
⊢ ∃ i, 0 < i ∧ ball (f z₀) i ⊆ f '' closedBall z₀ R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * 0 + 1) = 2 * ∏ i ∈ Finset.range 0, (2 * ↑i + 2) / (2 * ↑i + 3)

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, ((2 - 1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n

Tactic:
norm_num

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

Goal state before:
pp: case hf.refine_2
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
⊢ ContinuousWithinAt (fun x ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x

Tactic:
suffices ‖x - ρ‖ ≠ 0 by fun_prop

Goal state after:
case hf.refine_2
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
⊢ ‖x - ρ‖ ≠ 0
Module: Mathlib.Analysis.Complex.SqrtDeriv

Goal state before:
pp: z : ℂ
hz : z ∈ slitPlane
⊢ 2⁻¹ - 1 = -1 / 2

Tactic:
norm_num

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

Goal state before:
pp: z : ℂ
hz : 0 ≤ z.re ∨ z.im ≠ 0
⊢ 0 < 2⁻¹.re

Tactic:
norm_num

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s

Tactic:
· exact hs.1

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s

Tactic:
· exact hs.1

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖

Tactic:
by
  rw [h₁f.meromorphicOn.circleAverage_log_norm hR, h₁f.divisor_apply (by simp),
    (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f,
    (h₁f c (by simp)).meromorphicTrailingCoeffAt_of_ne_zero h₂f]
  simp

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

Goal state before:
pp: ⊢ 0 < 2⁻¹

Tactic:
norm_num

Goal state after: