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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ ∀ ⦃x : ℂ⦄, x ∈ verticalStrip 0 1 → ↑l + x • (↑u - ↑l) ∈ verticalStrip l u

Tactic:
intro z hz

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ ↑l + z • (↑u - ↑l) ∈ verticalStrip l u
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
⊢ ‖f z‖ ≤ C

Tactic:
suffices ‖f (z * I * -I)‖ ≤ C by simpa [mul_assoc] using this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
⊢ ‖f (z * I * -I)‖ ≤ C
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
⊢ Tendsto (fun x ↦ x * -I) (comap (fun x ↦ |x.re|) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b))
    (comap (fun x ↦ |x.im|) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b))

Tactic:
refine (tendsto_comap_iff.2 ?_).inf H.tendsto

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
c : ℝ
hc : c < π / (b - a)
B : ℝ
hO : f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
⊢ Tendsto ((fun x ↦ |x.im|) ∘ fun x ↦ x * -I) (comap (fun x ↦ |x.re|) atTop) atTop
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 : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
⊢ EqOn (fun z ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) (fun z ↦ (z - w)⁻¹ • f z) (sphere c |R|)

Tactic:
intro z hz

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : 0 < |R|
z : ℂ
hz : z ∈ sphere c |R|
⊢ (fun z ↦ (z - c)⁻¹ • ((z - c) * (z - w)⁻¹) • f z) z = (fun z ↦ (z - w)⁻¹ • f z) z
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

Goal state after:
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 : ℂ
hz : z ∈ ball c |R| \ ∅
⊢ DifferentiableAt ℂ f z
Module: Mathlib.Analysis.Complex.Harmonic.MeanValue

Goal state before:
pp: case neg
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|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ closedBall c |r| ⊆ ball c |R|

Tactic:
abs_of_pos hr.1

Goal state after:
case neg
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|)
r : ℝ
hr : r ∈ Set.Ioo 0 |R|
⊢ closedBall c r ⊆ ball c |R|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

Tactic:
simpa using mul_pos x.2 z.im_pos

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
h : 0 ≤ z.im
⊢ ‖f z‖ ≤ max C C'

Tactic:
refine quadrant_I (hd.mono fun _ => And.left) ⟨c, hc, B, ?_⟩
          (fun x hx => (hC' x hx).trans <| le_max_right _ _)
          (fun x _ => (him x).trans (le_max_left _ _)) hz h

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
C' : ℝ
hC' : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C'
z : ℂ
hz : 0 ≤ z.re
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
h : 0 ≤ z.im
⊢ f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun x ↦ x * log x) x = x⁻¹
⊢ deriv^[2] (fun x ↦ -(x * log x)) x = -x⁻¹

Tactic:
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp, deriv.fun_neg',
    Function.comp_apply] at h ⊢

Goal state after:
x : ℝ
h : ∀ (x : ℝ), deriv (deriv fun x ↦ x * log x) x = x⁻¹
⊢ -deriv (deriv fun i ↦ i * log i) x = -x⁻¹
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 {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
⊢ ball (↑x₀) (dist 0 ↑x₀) ⊆ {z | 0 < z.re}

Tactic:
intro z hz

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
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 : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : z ∈ ball (↑x₀) (dist 0 ↑x₀)
⊢ z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case pos
x : ℝ
hx : x = 0
⊢ ContinuousAt log⁺ x

pp: case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt log⁺ x

Tactic:
· apply ContinuousAt.congr (f := fun _ ↦ 0) (by fun_prop)
    filter_upwards [Metric.ball_mem_nhds _ zero_lt_one] with y hy
    rw [eq_comm, posLog_eq_zero_iff y]
    simp_all [le_of_lt]

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ ContinuousAt log⁺ x
Module: Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric

Goal state before:
pp: ⊢ (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (cos x) =
    (∫ (x : ℝ) in 0..π / 2, log (sin (2 * x))) - π / 2 * log 2 - ∫ (x : ℝ) in 0..π / 2, log (sin x)

Tactic:
simp [← sin_pi_div_two_sub,
        intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]

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

Goal state before:
pp: a : ℂ
h : ‖a‖ < 1
⊢ Set.EqOn (fun x ↦ log ‖x - a‖) (fun x ↦ log ‖1 - x⁻¹ * a‖) (sphere 0 |1|)

Tactic:
intro z hz

Goal state after:
a : ℂ
h : ‖a‖ < 1
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ (fun x ↦ log ‖x - a‖) z = (fun x ↦ log ‖1 - x⁻¹ * a‖) z
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: 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 : ℂ), 0 < z.re → f z = 0

Tactic:
intro z hz

Goal state after:
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
⊢ f z = 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
⊢ ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
intro z hz

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∀ z ∈ sphere 0 |1|, ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite

Tactic:
intro z hz

Goal state after:
a c : ℂ
R : ℝ
hR : R ≠ 0
z : ℂ
hz : z ∈ sphere 0 |1|
⊢ ∃ t ∈ nhds z, (t ∩ (sphere 0 |1| \ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0})).Finite
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
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x = C + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ 2 * sin x ^ n

Tactic:
simp [H, h, sq]

Goal state after:
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
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ -(sin b ^ (n + 1) * cos b) + sin a ^ (n + 1) * cos a = C
Module: Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.ZeroAtFilter g
⊢ l.ZeroAtFilter (f * g)

Tactic:
by
  rw [ZeroAtFilter, ← Asymptotics.isLittleO_one_iff (F := ℝ)] at hg ⊢
  simpa using! hf.mul_isLittleO hg

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

Goal state before:
pp: h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
by
  let q := 𝕢 h z
  have qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * π * I / h)) z := by
    simpa only [id_eq, mul_one] using! (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp
  -- Now show that the q-map has a differentiable local inverse at z, say L : ℂ → ℂ with L q = z.
  have diff_ne : q * (2 * π * I / h) ≠ 0 :=
    mul_ne_zero (exp_ne_zero _) (div_ne_zero two_pi_I_ne_zero <| mod_cast hh)
  let L := (qdiff.localInverse (𝕢 h) _ z) diff_ne
  have diff_L : DifferentiableAt ℂ L q :=
    (qdiff.to_localInverse diff_ne).hasStrictFDerivAt.differentiableAt
  have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) :=
    (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse
  -- Thus, if F = cuspFunction h f, we have F q' = f (L q') for q' near q.
  -- Since L is differentiable at q, and f is differentiable at L q [ = z], we conclude
  -- that F is differentiable at q.
  have hF := hL.fun_comp (cuspFunction h f)
  have : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L := funext fun z ↦ eq_cuspFunction hh hf (L z)
  rw [this] at hF
  rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
    at hol_z
  exact (hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm

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

Goal state before:
pp: P : ℂ[X]
h₀ : 0 < P.degree
⊢ (derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)

Tactic:
intro z hz

Goal state after:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : z ∈ (derivative P).rootSet ℂ
⊢ z ∈ (convexHull ℝ) (P.rootSet ℂ)
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
⊢ 0 ≤ f z

Tactic:
by
  refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_
  rw [← sub_nonneg] at hz
  rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]
  simpa only [Complex.norm_of_nonneg (nonneg_iff.mp hz).1] using! lt_add_one _

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

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ 2 = (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32

Tactic:
convert! integral_sin_pow_even_mul_cos_pow_even 1 1 using 1

Goal state after:
case e'_3
a b : ℝ
⊢ (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
intro z hz

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ HasStrictDerivAt f (2 * f z)⁻¹ z
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ 𝓝 (f x)

Tactic:
← (hdf x hx).map_nhds_eq (by simpa using hf₀ x hx)

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ map f (𝓝 x)
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ MapsTo (fun z ↦ ↑ε / (f z - x)) U (ball 0 1)

Tactic:
intro z hz

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ (fun z ↦ ↑ε / (f z - x)) z ∈ ball 0 1
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
⊢ ∀ z ∈ U, deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0

Tactic:
intro z hz

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case pos
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:
have h₃f := (divisor f CB).finiteSupport (isCompact_closedBall c |R|)

Goal state after:
case pos
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
⊢ 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‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : 0 ≤ re a
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)

Tactic:
simp [abs_of_nonneg ha', ← two_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt = ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
Complex.sqrt_eq_real_add_ite

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  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‖
integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) * Real.log (R / r) ≤
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]

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

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr

Tactic:
simpa using hell.le

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
refine hm.not_ge ?_

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ 0 ≤ (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := ↑g 1 0
d : ℝ := ↑g 1 1
⊢ (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2

Tactic:
by nlinarith

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ ↑(g • z) =
    (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
      (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))

Tactic:
rw [MulAction.compHom_smul_def, coe_smul_of_det_pos (by simp)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ num ((mapGL ℝ) g) ↑z / denom ((mapGL ℝ) g) ↑z =
    (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
      (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ ↑(g • z) =
    (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
      (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))

Tactic:
rw [MulAction.compHom_smul_def, coe_smul_of_det_pos (by simp)]
  rfl

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
this : ∀ (x : X), f x = a
⊢ (∀ (y : Y), ∃ x₁ x₂, (const Y a) y ∈ Icc (f x₁) (f x₂)) ∧ ⇑(const Y a) ∘ e = ⇑f

Tactic:
simp [this, funext_iff]

Goal state after: