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

Goal state before:
pp: case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = f c

Tactic:
rw [← circleAverage_smul_div hf (by aesop)]

Goal state after:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : ¬R = 0
⊢ Real.circleAverage f c R = Real.circleAverage (fun z ↦ ((z - c) / (z - c)) • f z) c R
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
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
ζ✝ : ℂ
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)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖(f ∘ cexp) ζ‖ ≤ C

Tactic:
← re_add_im ζ,

Goal state after:
case inr.refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
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
ζ✝ : ℂ
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)
ζ : ℂ
hζ : ζ.im = π / 2
⊢ ‖(f ∘ cexp) (↑ζ.re + ↑ζ.im * I)‖ ≤ C
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |(2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ)

Tactic:
abs_mul,

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℝ
⊢ |(2 * π)⁻¹| * |∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ)| ≤ (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, |f| (circleMap c R θ)
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:
simpa only [mem_reProdIm, mul_I_re, mul_I_im, neg_lt_zero, mem_Iio] using! hw.symm

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

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

Tactic:
simpa [UpperHalfPlane.ext_iff, Complex.ext_iff, hre, Complex.normSq, Complex.sq_norm,
    ← pow_two, pow_left_inj₀ τ.im_pos.le τ'.im_pos.le two_ne_zero] using hnorm

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
      simp [← normSq_apply, normSq_eq_norm_sq]

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

Goal state before:
pp: case mpr
x : ℝ
hx : x ≠ 0
this : x ∈ {0}ᶜ
⊢ DifferentiableAt ℝ negMulLog x

Tactic:
have := differentiableOn_negMulLog x this

Goal state after:
case mpr
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableAt ℝ negMulLog x
Module: Mathlib.Analysis.SpecialFunctions.Log.InvLog

Goal state before:
pp: ⊢ ¬DifferentiableAt ℝ (fun x ↦ (log x)⁻¹) 0

Tactic:
by
  simp only [← hasDerivAt_deriv_iff, hasDerivAt_iff_tendsto_slope_zero, zero_add, log_zero,
    inv_zero, sub_zero, smul_eq_mul, ← mul_inv, mul_comm _ (log _)]
  refine fun H ↦ (tendsto_nhdsWithin_mono_left (by grind : Set.Iio (0 : ℝ) ⊆ _) H).not_tendsto
    (by simp) (tendsto_inv_nhdsGT_zero.comp ?_)
  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
    tendsto_log_mul_self_nhdsLT_zero ?_
  simp only [← nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero, Set.mem_Ioi]
  refine eventually_nhdsWithin_of_forall fun x ⟨hx₁, hx₂⟩ ↦ mul_pos_of_neg_of_neg ?_ hx₂
  apply log_neg_eq_log x ▸ log_neg <;> grind

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

Goal state before:
pp: case hst
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioc 0 c
⊢ x ^ r.re = ‖↑x ^ r‖

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ IntervalIntegrable ((∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) volume a b

Tactic:
apply IntervalIntegrable.add

Goal state after:
case pos.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ IntervalIntegrable (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) volume a b

case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
t₀ : ∀ (u : ↑[[a, b]]), meromorphicOrderAt f ↑u ≠ ⊤
g : ℝ → E
h₁g : AnalyticOnNhd ℝ g [[a, b]]
h₂g : ∀ (u : ↑[[a, b]]), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin [[a, b]]] (∏ᶠ (u : ℝ), (fun x ↦ x - u) ^ (divisor f [[a, b]]) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin [[a, b]]]
    (∑ᶠ (u : ℝ), fun x ↦ ↑((divisor f [[a, b]]) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ IntervalIntegrable (fun x ↦ log ‖g x‖) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
h₁y : y ∈ sin ⁻¹' {0}ᶜ
⊢ y ∈ cos ⁻¹' {0}ᶜ → log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)

Tactic:
h₂y

Goal state after:
t₀ : sin ⁻¹' {0}ᶜ ∈ codiscrete ℝ
t₁ : cos ⁻¹' {0}ᶜ ∈ codiscrete ℝ
y : ℝ
h₁y : y ∈ sin ⁻¹' {0}ᶜ
h₂y : y ∈ cos ⁻¹' {0}ᶜ
⊢ log (sin y) = log (sin (2 * y)) - log 2 - log (cos y)
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) volume a b

Tactic:
apply IntervalIntegrable.add

Goal state after:
case hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * log ‖f x‖) volume a b

case hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (fun x ↦ 2⁻¹ * |log ‖f x‖|) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
⊢ ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2 = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2)

Tactic:
rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div
      (f := fun x ↦ log (4 * sin x ^ 2))]

Goal state after:
this : ∀ {x : ℝ}, x / 2 = 2⁻¹ * x
⊢ ∫ (x : ℝ) in 0 / 2..2 * π / 2, log (4 * sin x ^ 2) = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖ =
    ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖

Tactic:
simp [← hζ, inv_mul_cancel₀ (by aesop : a ≠ 0)]

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

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

Tactic:
have d := HasDerivAt.comp_ofReal (c.div_const z)

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

Goal state before:
pp: case neg
a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
hR : ¬R = 0
⊢ |R⁻¹ * ‖c - a‖| ≤ 1

Tactic:
abs_mul,

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

Goal state before:
pp: h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ ‖𝕢 h z‖ < rexp (-2 * π * A / h) ↔ A < z.im

Tactic:
rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]
  simpa using Real.pi_pos

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
⊢ g z = g z₀

Tactic:
have h3 : ∀ t ∈ ball (0 : ℂ) r, gray w t = g z₀ := by
      have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected
      have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h']
      specialize h1 w e2
      apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr)
      simpa [ray, gray] using! h w e2

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
⊢ g z = g z₀
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ (𝓝[≠] 0).BoundedAtFilter (cuspFunction h f)

Tactic:
by
  refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by simp)
  refine eventually_nhdsWithin_of_forall fun q hq ↦ ?_
  rw [cuspFunction_eq_of_nonzero _ _ hq, comp_def]

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

Goal state before:
pp: n : ℕ
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)
  refine integral_mono_on pi_pos.le ?_ ?_ H <;> exact (continuous_sin.pow _).intervalIntegrable 0 π

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, ‖cuspFunction h f x‖ ≤ c * ‖1 x‖
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
replace t := (eventually_differentiableAt_cuspFunction_nhds_ne_zero hh hf h_hol).and t

Goal state after:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * ‖1 x‖
⊢ DifferentiableAt ℂ (cuspFunction h f) 0
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z w : ℂ
⊢ 0 ≤ if eval z P = 0 then if w = z then 1 else 0 w else ↑(rootMultiplicity w P) / ‖z - w‖ ^ 2

Tactic:
split_ifs <;> first | positivity | simp

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case hws
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ 0 < ∑ i ∈ P.roots.toFinset, P.derivRootWeight z i

pp: case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ

Tactic:
· apply sum_derivRootWeight_pos h₀

Goal state after:
case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : c ≤ z
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z

Tactic:
← sub_nonneg

Goal state after:
f : ℂ → ℂ
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz₁ : 0 ≤ z - c
hz₂ : z ∈ Metric.ball c r
H : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
⊢ 0 ≤ f z
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ z ∈ Metric.ball c ((z - c).re + 1)

Tactic:
← sub_nonneg

Goal state after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : 0 ≤ z - c
⊢ z ∈ Metric.ball c ((z - c).re + 1)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
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 ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
· -- Trivial case: `f` vanishes on a codiscrete set
    have h₂f : ¬∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u ≠ ⊤ := by aesop
    rw [← h₁f.exists_meromorphicOrderAt_ne_top_iff_forall
      ⟨nonempty_closedBall.mpr (abs_nonneg R), (convex_closedBall c |R|).isPreconnected⟩] at h₂f
    push Not at h₂f
    have : divisor f CB = 0 := by
      ext x
      by_cases h : x ∈ CB
      <;> simp_all [CB]
    simp only [CB, this, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, Int.cast_zero,
      zero_mul, finsum_zero, add_zero, zero_add]
    rw [MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top (by aesop), norm_zero, log_zero]
    have : f =ᶠ[codiscreteWithin CB] 0 := by
      filter_upwards [h₁f.meromorphicNFAt_mem_codiscreteWithin, self_mem_codiscreteWithin CB]
        with z h₁z h₂z
      simpa [h₂f ⟨z, h₂z⟩] using (not_iff_not.2 h₁z.meromorphicOrderAt_eq_zero_iff)
    rw [circleAverage_congr_codiscreteWithin (f₂ := 0) _ hR]
    · simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero,
        smul_eq_mul, mul_zero]
    apply Filter.codiscreteWithin_mono (U := CB) sphere_subset_closedBall
    filter_upwards [this] with z hz
    simp_all

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
⊢ -‖f‖ ≤ f x ∧ f x ≤ ‖f‖

Tactic:
simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x

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

Goal state before:
pp: case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
simp [mul_pos h h', h, h']

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

Goal state before:
pp: g : GL (Fin 2) ℝ
⊢ Continuous (UpperHalfPlane.coe ∘ fun x ↦ g • x)

Tactic:
Function.comp_def,

Goal state after:
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ ↑(g • x)
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    !![z.re, -z.im; z.im, z.re] i j

Tactic:
Matrix.of_apply

Goal state after:
z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ eval 0 (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det

Tactic:
← coe_evalRingHom,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (evalRingHom 0) (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ eval 0 ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix)).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det

Tactic:
← coe_evalRingHom,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (evalRingHom 0) ((Matrix.comp m m n n R[X]) ((cornerAddX M k).map ⇑f.polyToMatrix)).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun x ↦ denom g ↑x ^ k

Tactic:
intro τ

Goal state after:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (fun x ↦ denom g ↑x ^ k) τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ g • τ

Tactic:
intro τ

Goal state after:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (fun τ ↦ g • τ) τ
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed[inst✝²] s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f

Tactic:
obtain ⟨g, hg, hgf⟩ :=
    exists_extension_forall_mem_of_isClosedEmbedding f hf hne hs.isClosedEmbedding_subtypeVal

Goal state after:
Y : Type u_2
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed[inst✝²] s
t : Set ℝ
inst✝ : t.OrdConnected
hf : ∀ (x : ↑s), f x ∈ t
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), g y ∈ t
hgf : ⇑g ∘ Subtype.val = ⇑f
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt (F ∘ G) ↑τ = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)

Tactic:
meromorphicOrderAt_comp_of_deriv_ne_zero

Goal state after:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt F (G ↑τ) = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)

case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ

case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
⊢ some ⁻¹' {∞} = ∅

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
D : Set ↑Y.toTop := {y}
hD : IsClosed D
y' : (fun X ↦ ↑X.toTop) X
hy' : (ConcreteCategory.hom f) y' = y
⊢ False

Tactic:
exact hy y' hy'

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

Goal state before:
pp: g : GL (Fin 2) ℝ
τ : ℍ
⊢ (fun x ↦ (σ g) (num x.1 ↑x.2 / denom x.1 ↑x.2)) =ᶠ[nhds (g, τ)] fun x ↦ (σ x.1) (num x.1 ↑x.2 / denom x.1 ↑x.2)

Tactic:
filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual

Goal state after: