mathlib-initiative/mathlib-tactics huggingface dataset:
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)

pp: case refine_2
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‖ ≤ C

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:
· 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:
case refine_2
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‖ ≤ C

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
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: w c z : ℂ
η₂ : z - c ≠ 0
hz : z ∈ sphere c ‖z - c‖
hw : w ∈ ball c ‖z - c‖
η₀ : 0 < ‖z - c‖
h₁w : ¬‖w - c‖ = 0
⊢ 0 < ‖w - c‖

Tactic:
by simpa using h₁w

Goal state after:
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)

pp: case refine_2
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 : x ≤ 0
⊢ ‖(f ∘ Neg.neg) ↑x‖ ≤ C

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:
· 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:
case refine_2
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 : x ≤ 0
⊢ ‖(f ∘ Neg.neg) ↑x‖ ≤ C

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
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R : ℝ
w : ℂ
g : ℂ → ℝ
hg : CircleIntegrable g 0 R
hw : w ∈ ball 0 R
h₁ : CircleIntegrable (fun ζ ↦ ↑(g ζ)) 0 R
⊢ (circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R).re =
    circleAverage (re ∘ herglotzRieszKernel 0 w • g) 0 R

Tactic:
have h₂ : CircleIntegrable (fun ζ ↦ herglotzRieszKernel 0 w ζ • (g ζ : ℂ)) 0 R :=
    h₁.continuousOn_smul (continuousOn_herglotzRieszKernel_sphere hw)

Goal state after:
R : ℝ
w : ℂ
g : ℂ → ℝ
hg : CircleIntegrable g 0 R
hw : w ∈ ball 0 R
h₁ : CircleIntegrable (fun ζ ↦ ↑(g ζ)) 0 R
h₂ : CircleIntegrable (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R
⊢ (circleAverage (fun ζ ↦ herglotzRieszKernel 0 w ζ • ↑(g ζ)) 0 R).re =
    circleAverage (re ∘ herglotzRieszKernel 0 w • g) 0 R
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: ⊢ (fun x ↦ deriv (fun x ↦ x * log x) x) =ᶠ[atTop] fun x ↦ log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Goal state after:
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → deriv (fun x ↦ x * log x) b = log b + 1
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case inl
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 : z.im ≤ 0
⊢ ‖f z‖ ≤ max C C'

Tactic:
refine quadrant_IV (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
      exact hO.mono (inf_le_inf_left _ <| principal_mono.2 fun _ => And.left)

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

Goal state before:
pp: ⊢ (fun x ↦ derivWithin (fun x ↦ x * log x) (Set.Ioi x) x) =ᶠ[atTop] fun x ↦ log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Goal state after:
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → derivWithin (fun x ↦ x * log x) (Set.Ioi b) b = log b + 1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
intro c hc

Goal state after:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x ↦ x ^ r) volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

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

Tactic:
intro c hc

Goal state after:
a b : ℝ
r : ℂ
h : -1 < r.re
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) volume 0 c
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
⊢ IntervalIntegrable (fun x ↦ log ‖f x‖) volume a b

Tactic:
have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g

Goal state after:
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 (fun x ↦ log ‖f x‖) volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (min 0 c) 0
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
exact hx.2.ne

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
C : ℝ
f : ℂ → E
z : ℂ
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
ε : ℝ
ε₀ : ε < 0
g : ℂ → E := fun z ↦ cexp (↑ε * z) • f z
hd : DiffContOnCl ℂ g {z | 0 < z.re}
hgn : ∀ (z : ℂ), ‖g z‖ = expR (ε * z.re) * ‖f z‖
h₀ : Tendsto (fun x ↦ expR (ε * x)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ expR (ε * x) • f ↑x) atTop (𝓝 0)

Tactic:
exact h₀.zero_smul_isBoundedUnder_le hre

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
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
by_cases hc : c = 0
    · simp [hc]
    · rw [integral_const_mul, integral_inv_sq_add_sq hc]
      field_simp

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

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
⊢ ∃ c, ∀ x ∈ U, f x = ↑c + ↑c₀ * I

Tactic:
obtain ⟨cc, hcc⟩ := AnalyticOnNhd.eq_const_of_im_eq_const h₁f h₂f h₁U h₂U

Goal state after:
f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
cc : ℂ
hcc : ∀ x ∈ U, f x = cc
⊢ ∃ c, ∀ x ∈ U, f x = ↑c + ↑c₀ * I
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

Tactic:
simp only [derivRootWeight, if_neg hPz]
    apply Finset.sum_pos
    · intro w hw
      apply div_pos (by simp_all)
      suffices z ≠ w by simpa [sq_pos_iff, sub_eq_zero]
      rintro rfl
      simp_all
    · rw [Multiset.toFinset_nonempty]
      apply Splits.roots_ne_zero (IsAlgClosed.splits _)
      rwa [← pos_iff_ne_zero, natDegree_pos_iff_degree_pos]

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

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.natDegree
⊢ False

Tactic:
rw [natDegree_pos_iff_degree_pos] at hq''

Goal state after:
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < q.degree
⊢ False
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_on_ball hf hz using 3 with n

Goal state after:
case e'_5
c : ℂ
r : ℝ
z : ℂ
hz : z ∈ Metric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : ENNReal
hzr' : edist c z < r'
hr' : r' < r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
lift r' to NNReal using ne_top_of_lt hr'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
r' : NNReal
hzr' : edist c z < ↑r'
hr' : ↑r' < r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: 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 : ℕ
z : ℂ
hz : z ∈ ball 0 (r n)
⊢ z - ρ ≠ 0

Tactic:
grind [mem_ball, dist_zero_right]

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
⊢ 0 ∉ id '' U

Tactic:
rwa [image_id]

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

Goal state before:
pp: case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ circleAverage (fun z ↦ log ‖z - u‖) c R = log R

Tactic:
circleAverage_log_norm_sub_const_of_mem_closedBall

Goal state after:
case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ log R = log R

case e_a
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
u : ℂ
hu : u ∈ h.toFinset
⊢ u ∈ closedBall c |R|
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : 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
⊢ StrictMonoOn f (s ∪ t)

Tactic:
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim

Goal state after:
α : 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
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ StrictMonoOn f (s ∪ t)
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : 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
⊢ MonotoneOn f (s ∪ t)

Tactic:
have A : ∀ x, x ∈ s ∪ t → x ≤ c → x ∈ s := by
    intro x hx hxc
    cases hx
    · assumption
    rcases eq_or_lt_of_le hxc with (rfl | h'x)
    · exact hs.1
    exact (lt_irrefl _ (h'x.trans_le (ht.2 (by assumption)))).elim

Goal state after:
α : 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
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ MonotoneOn f (s ∪ t)
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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
⊢ divisor f CB = 0

Tactic:
ext x

Goal state after:
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 : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
x : ℂ
⊢ (divisor f CB) x = 0 x
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
⊢ { toFun := codRestrict ((Metric.closedBall 0 1).piecewise id g) (Metric.closedBall 0 1) ⋯,
          continuous_toFun := ⋯ }.comp
      { toFun := Subtype.val, continuous_toFun := ⋯ } =
    ContinuousMap.id ↑(Metric.closedBall 0 1)

Tactic:
ext x

Goal state after:
case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝¹ : NormedSpace ℝ E
this✝ : IsScalarTower ℝ 𝕜 E
g : E → E := ⋯
this : Continuous ((Metric.closedBall 0 1).piecewise id g)
x : ↑(Metric.closedBall 0 1)
⊢ ↑(({ toFun := codRestrict ((Metric.closedBall 0 1).piecewise id g) (Metric.closedBall 0 1) ⋯,
              continuous_toFun := ⋯ }.comp
          { toFun := Subtype.val, continuous_toFun := ⋯ })
        x) =
    ↑((ContinuousMap.id ↑(Metric.closedBall 0 1)) x)
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: 𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ closedBall 0 1 = ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r

Tactic:
ext x

Goal state after:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ x ∈ closedBall 0 1 ↔ x ∈ ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r
Module: Mathlib.Analysis.Complex.Tietze

Goal state before:
pp: X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
⊢ g'.domRestrict s = f

Tactic:
ext x

Goal state after:
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
x : ↑s
⊢ (g'.domRestrict s) x = f x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := ⋯.toHomeomorph
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
⊢ g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
ext x

Goal state after:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := ⋯.toHomeomorph
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
x : X₁
⊢ (g.comp { toFun := e, continuous_toFun := ⋯ }) x = f x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = f
⊢ ⇑g ∘ e = ⇑f

Tactic:
ext x

Goal state after:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
g : C(X, Y)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = f
x : X₁
⊢ (⇑g ∘ e) x = f x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed[inst✝²] s
Y : Type v
inst✝ : TopologicalSpace Y
f : C(↑s, Y)
t : Set Y
hf : ∀ (x : ↑s), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ restrict s ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g) = f

Tactic:
ext x

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s : Set X
hs : IsClosed[inst✝²] s
Y : Type v
inst✝ : TopologicalSpace Y
f : C(↑s, Y)
t : Set Y
hf : ∀ (x : ↑s), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
x : ↑s
⊢ (restrict s ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g)) x = f x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X₁ : Type u₁
inst✝³ : TopologicalSpace X₁
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst✝ : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
⊢ ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g).comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
ext x

Goal state after:
X₁ : Type u₁
inst✝³ : TopologicalSpace X₁
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
e : X₁ → X
he : IsClosedEmbedding e
Y : Type v
inst✝ : TopologicalSpace Y
f : C(X₁, Y)
t : Set Y
hf : ∀ (x : X₁), f x ∈ t
ht : TietzeExtension ↑t
g : C(X, ↑t)
hg : g.comp { toFun := e, continuous_toFun := ⋯ } = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }
x : X₁
⊢ (({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp g).comp { toFun := e, continuous_toFun := ⋯ }) x = f x