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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
h₁w : w ∈ closedBall 0 R
h₂w : meromorphicOrderAt f w = 0
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
⊢ ∑ i ∈ t₂, log (‖canonicalFactor R i w‖ ^ (divisor f B₀R) i) + ∑ i ∈ t₁, log (‖w - i‖ ^ (-divisor f S₀R) i) +
      log ‖meromorphicTrailingCoeffAt f w‖ =
    ∑ᶠ (i : ℂ), ↑((divisor f B₀R) i) * log ‖canonicalFactor R i w‖ - ∑ᶠ (i : ℂ), ↑((divisor f S₀R) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
rw [finsum_eq_sum_of_support_subset (s := t₂) _ ?η₀,
        finsum_eq_sum_of_support_subset (s := t₁) _ ?η₁]
      case η₀ | η₁ => intro _ _; simp_all [S₀R, B₀R]
      rw [sub_eq_add_neg, ← Finset.sum_neg_distrib]
      congr! 3 with i hi i hi <;> simp

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

Goal state before:
pp: case h
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
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⋯
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := ⋯
γ : Path x x := ⋯
⊢ (hp.fundamentalGroupToMulOpposite e) (FundamentalGroup.fromPath ⟦γ⟧) = g

Tactic:
fundamentalGroupToMulOpposite_apply_eq_Iff

Goal state after:
case h
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
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
g : Gᵐᵒᵖ
e' : ↑(p ⁻¹' {x}) := ⟨MulOpposite.unop g • ↑e, ⋯⟩
he' : e' = ⟨MulOpposite.unop g • ↑e, ⋯⟩
Γ : Path ↑e ↑e' := { toFun := ⇑(PathConnectedSpace.somePath ↑e ↑e'), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
γ : Path x x := (Γ.map ⋯).cast ⋯ ⋯
⊢ MulOpposite.unop g • ↑e = ↑(⋯.monodromy (FundamentalGroup.fromPath ⟦γ⟧) e)
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
hgoal : ‖f z‖ ≤ ‖interpStrip' f l u z‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
exact hgoal

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
hgoal : ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))

Tactic:
exact hgoal

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

Goal state before:
pp: case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
⊢ z ∈ univ → HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z

Tactic:
_

Goal state after:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
inst✝ : CompleteSpace E
h₁ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h₂ : IsConservativeOn f univ
z : ℂ
a✝ : z ∈ univ
⊢ HasDerivAt (fun x ↦ wedgeIntegral 0 x f) (f z) z
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 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
⊢ z ∈ im ⁻¹' Ioo 0 (π / 2) → B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)

Tactic:
_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C
ζ : ℂ
hζ : ζ.im ∈ Icc 0 (π / 2)
hz_re : 0 ≤ (cexp ζ).re
hz_im : 0 ≤ (cexp ζ).im
hzne : cexp ζ ≠ 0
H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
z : ℂ
hz : z.re = x
a✝ : z ∈ im ⁻¹' Ioo 0 (π / 2)
⊢ B * expR (z.re * c) ≤ max B 0 * expR (c * |z.re|)
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
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)
⊢ ∃ c < 2, ∃ B, (f ∘ Neg.neg) =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hB with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, ?_⟩
    simpa only [Function.comp_def, norm_neg]
      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)

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
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C

Tactic:
have H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0) := fun w hw ↦ by
    simpa only [mem_reProdIm, neg_re, neg_im, neg_lt_zero, neg_pos, mem_Ioi, mem_Iio] using hw

Goal state after:
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)
⊢ ‖(f ∘ Neg.neg) z‖ ≤ C
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
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)
⊢ ∃ c < 2, ∃ B, (f ∘ Neg.neg) =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)

Tactic:
rcases hB with ⟨c, hc, B, hO⟩
    refine ⟨c, hc, B, ?_⟩
    simpa only [Function.comp_def, norm_neg]
      using hO.comp_tendsto (Filter.tendsto_neg_cobounded.inf H.tendsto)

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ deriv (fun x ↦ x * log x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Goal state after:
⊢ (fun x ↦ deriv (fun x ↦ x * log x) x) =ᶠ[atTop] fun x ↦ log x + 1
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ Tendsto (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Goal state after:
⊢ (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) =ᶠ[atTop] fun x ↦ log x + 1
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: case neg
f : ℂ → ℂ
z : ℂ
h₁f : AnalyticAt ℂ f z
h₂f : f z ≠ 0
this : (fun x ↦ Real.log ‖f x‖) = 2⁻¹ • Real.log ∘ ⇑normSq ∘ f
h₃f : f z ∉ slitPlane
⊢ HarmonicAt (Real.log ∘ ⇑normSq ∘ (-f)) z

Tactic:
exact analyticAt_harmonicAt_log_normSq h₁f.neg (by simpa)
      ((mem_slitPlane_or_neg_mem_slitPlane h₂f).resolve_left h₃f)

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

Goal state before:
pp: a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
⊢ x ∈ Icc 0 c → id x ≠ 0 ∨ 0 ≤ r + 1

Tactic:
_

Goal state after:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
a✝ : x ∈ Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1
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 * π)))
θ : ℝ
⊢ θ ∈ uIoc 0 (2 * π) →
    ∀ x ∈ ball w d,
      ‖(2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)‖ ≤
        2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖

Tactic:
_

Goal state after:
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 ∈ ball w d,
    ‖(2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)‖ ≤
      2 * R * (d ^ 2)⁻¹ * ‖f (circleMap 0 R θ)‖
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 * π)))
θ : ℝ
⊢ θ ∈ uIoc 0 (2 * π) →
    ∀ x ∈ ball w d,
      HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
        ((2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)) x

Tactic:
_

Goal state after:
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 ∈ ball w d,
    HasDerivAt (fun x ↦ herglotzRieszKernel 0 x (circleMap 0 R θ) • f (circleMap 0 R θ))
      ((2 * circleMap 0 R θ / (circleMap 0 R θ - x) ^ 2) • f (circleMap 0 R θ)) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ log (sin x)) MeasureTheory.volume 0 (π / 2)

Tactic:
apply intervalIntegrable_log_sin

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

Goal state before:
pp: ⊢ IntervalIntegrable (fun x ↦ log (sin x)) MeasureTheory.volume (π / 2) π

Tactic:
apply intervalIntegrable_log_sin

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

Goal state before:
pp: case hderiv
z : ℂ
hz : z ≠ 0
a b x : ℝ
⊢ x ∈ [[a, b]] → HasDerivAt (fun b ↦ Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
_

Goal state after:
case hderiv
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b ↦ Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case refine_1
a b : ℝ
ha : 1 < a
hb : 1 < b
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[a, b]]
⊢ DifferentiableAt ℝ (fun t ↦ (log t)⁻¹) x✝¹

Tactic:
exact differentiableOn_inv_log.differentiableAt (Ioi_mem_nhds (by grind [Set.uIcc]))

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

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
suffices ∫ t in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹ by
    simp_rw [deriv_inv_log, neg_div, intervalIntegral.integral_neg] at this
    linarith
  refine integral_deriv_eq_sub (fun _ _ ↦ ?_) (ContinuousOn.intervalIntegrable ?_)
  · exact differentiableOn_inv_log.differentiableAt (Ioi_mem_nhds (by grind [Set.uIcc]))
  suffices ContinuousOn (fun x ↦ (-x⁻¹) * ((log x)⁻¹) ^ 2) (.uIcc a b) by
    convert this using 2 with x
    simp [field]
  fun_prop (disch := grind [log_pos, Set.uIcc])

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

Goal state before:
pp: case inr.inl
a : ℂ
h : 1 = ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff]

Goal state after:
case inr.inl
a : ℂ
h : 1 = ‖a‖
⊢ |‖a‖| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
⊢ x ∈ [[a, b]] → HasDerivAt (fun {b} ↦ (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x

Tactic:
_

Goal state after:
case hderiv
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} ↦ (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1))) (↑x * (1 + ↑x ^ 2) ^ t) x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: case e_a.inr
a c : ℂ
R : ℝ
hR : R ≠ 0
h : 0 < R
⊢ log⁺ (|R|⁻¹ * ‖c - a‖) = log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
rw [abs_of_pos h]

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

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x

Tactic:
simpa only [neg_neg] using! (hasDerivAt_cos x).neg

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ Tendsto (fun x ↦ expR (↑x).re ^ n * ‖f ↑x‖) atTop (𝓝 0)

Tactic:
exact hre n

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

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

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_
  refine (nhds_basis_ball.le_basis_iff (nhds_basis_closedBall.map f)).mpr fun R hR => ?_
  have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h
  have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf
  obtain ⟨ρ, hρ, h3, h4⟩ :
    ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by
    simpa only [ofPred_and, subset_inter_iff] using!
      nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1))
  replace h3 : DiffContOnCl ℂ f (ball z₀ ρ) :=
    ⟨h3.differentiableOn.mono ball_subset_closedBall,
      (closure_ball z₀ hρ.lt.ne.symm).symm ▸ h3.continuousOn⟩
  let r := ρ ⊓ R
  have hr : 0 < r := lt_inf_iff.mpr ⟨hρ, hR⟩
  have h5 : closedBall z₀ r ⊆ closedBall z₀ ρ := closedBall_subset_closedBall inf_le_left
  have h6 : DiffContOnCl ℂ f (ball z₀ r) := h3.mono (ball_subset_ball inf_le_left)
  have h7 : ∀ z ∈ sphere z₀ r, f z ≠ f z₀ := fun z hz =>
    h4 z (h5 (sphere_subset_closedBall hz)) (ne_of_mem_sphere hz hr.ne.symm)
  have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  have h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) := continuous_norm.comp_continuousOn
    ((h6.sub_const (f z₀)).continuousOn_ball.mono sphere_subset_closedBall)
  obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_isMinOn h8 h9
  refine ⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩
  exact (h6.ball_subset_image_closedBall hr (fun z hz => hfx hz) (not_eventually.mp h)).trans
    (by gcongr; exact inf_le_right)

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

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + 0 + 0

Tactic:
by
        grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
        simp

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

Goal state before:
pp: case h₂
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ |log ‖circleMap 0 r θ - ρ‖| ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
· apply abs_le.mpr ⟨_, _⟩
    · have h_log_lower_bound :
          log ‖circleMap 0 r θ - ρ‖ ≥ log (sqrt (r₀ / R)) + log ‖circleMap 0 R θ - ρ‖ := by
        rw [← log_mul (by positivity) (by positivity)]
        gcongr
      grind
    · calc log ‖circleMap 0 r θ - ρ‖
      _ ≤ |log (2 * R)| + 0 + 0 := by
        grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
        simp
      _ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖| := by
        gcongr <;> positivity

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
⊢ θ ∈ uIoc 0 (2 * π) →
    Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
      (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
_

Goal state after:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
a✝ : θ ∈ uIoc 0 (2 * π)
⊢ Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
    (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
t₀ : c ∈ CB
⊢ CB ∈ 𝓝[≠] c

Tactic:
apply mem_nhdsWithin.mpr

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := ⋯
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
t₀ : c ∈ CB
⊢ ∃ u, IsOpen u ∧ c ∈ u ∧ u ∩ {c}ᶜ ⊆ CB
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
simp_rw [← mul_sub]

Goal state after:
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ (↑α).sqrt = ↑√α

Tactic:
rw [← re_add_im (α : ℂ).sqrt, re_sqrt_ofReal]

Goal state after:
α : ℝ
hα : α ≥ 0
ha : 0 ≤ ↑α
⊢ ↑√α + ↑(↑α).sqrt.im * I = ↑√α
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
h : (↑g).det < 0
⊢ g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

Tactic:
simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, htrace, hc, num, denom, σ, h.not_gt, mul_comm,
    eq_div_iff, h₀]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 = 0
h₀ : ↑g 1 1 ≠ 0
h : (↑g).det < 0
⊢ -(z.re * ↑g 1 1) + ↑g 0 1 = z.re * ↑g 1 1 ↔ z.re * (2 * ↑g 1 1) = ↑g 0 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z = (σ g) ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det

Tactic:
σ,

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z =
      (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ (num g z / denom g z).im = ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)

Tactic:
by
  simp only [num, denom, Complex.div_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re,
    Complex.ofReal_im, zero_mul, add_zero, Complex.add_re, Complex.mul_re, sub_zero, ← sub_div,
    GeneralLinearGroup.val_det_apply, g.1.det_fin_two]
  ring

Goal state after: