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

Goal state before:
pp: case inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
trans 0

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ dist (f z) (f c) ≤ 0

E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ f =ᶠ[𝓝[≠] x] g

Tactic:
rw [eventuallyEq_iff_sub, ← (hf.sub hg).frequently_zero_iff_eventuallyEq_zero]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] x, f z = g z) ↔ ∃ᶠ (z : 𝕜) in 𝓝[≠] x, (f - g) z = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x

Tactic:
apply meromorphicTrailingCoeffAt_congr_nhdsNE

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₂ : MeromorphicAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
hf₁ : MeromorphicAt f₁ x
h₁f₂ : meromorphicOrderAt f₂ x = ⊤
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₁
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₂ x

Tactic:
apply meromorphicTrailingCoeffAt_congr_nhdsNE

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0
h₁f₁ : meromorphicOrderAt f₁ x = ⊤
⊢ f₁ + f₂ =ᶠ[𝓝[≠] x] f₂
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
⊢ f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U

Tactic:
have : U ∈ Filter.codiscreteWithin U := by simp
  filter_upwards [hf.analyticAt_mem_codiscreteWithin, this] with a h₁a h₂a
  simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 h₁a.meromorphicNFAt).symm]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : ¬meromorphicOrderAt f (g x) = ⊤
r : ℤ := (meromorphicOrderAt f (g x)).untop₀
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : F (g x) ≠ 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
⊢ meromorphicTrailingCoeffAt (f ∘ g) x = meromorphicTrailingCoeffAt ((fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g) x

Tactic:
apply meromorphicTrailingCoeffAt_congr_nhdsNE

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
h : ¬meromorphicOrderAt f (g x) = ⊤
r : ℤ := ⋯
F : 𝕜 → E
h₁F : AnalyticAt 𝕜 F (g x)
h₂F : F (g x) ≠ 0
h₃F : f =ᶠ[𝓝[≠] g x] fun z ↦ (z - g x) ^ (meromorphicOrderAt f (g x)).untop₀ • F z
⊢ f ∘ g =ᶠ[𝓝[≠] x] (fun x_1 ↦ g x_1 - g x) ^ r • F ∘ g
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₂ : meromorphicOrderAt f₂ x = ⊤
⊢ meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x

Tactic:
by
  rw [add_comm, meromorphicOrderAt_add_of_top_left hf₂]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ ∃ t, (∀ y ∈ t, ¬y = ↑w → f y = 0) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑w ∈ t

Tactic:
use t' \ {z.1}, fun y h₁y _ ↦ h₁t' y (mem_of_mem_sdiff h₁y) (mem_of_mem_inter_right h₁y)

Goal state after:
case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
z : ↑U
t' : Set 𝕜
h₁t' : ∀ y ∈ t', y ∈ {↑z}ᶜ → f y = 0
h₂t' : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t'
h₃t' : ↑z ∈ t'
w : ↑U
hw : w ∈ Subtype.val ⁻¹' t'
h₁w : ¬w = z
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t' \ {↑z}) ∧ ↑w ∈ t' \ {↑z}
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ ENat.map Nat.cast (analyticOrderAt (fun x_1 ↦ g x_1 - g x) x) ≠ 0

Tactic:
· simp [(show AnalyticAt 𝕜 (g · - g x) x by fun_prop).analyticOrderAt_eq_zero]

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

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
⊢ DiffContOnCl ℂ (fun z ↦ invInterpStrip f z ε) (verticalStrip 0 1)

Tactic:
apply Differentiable.diffContOnCl
  apply Differentiable.mul
  · apply Differentiable.const_cpow (Differentiable.sub_const differentiable_id 1) _
    left
    rw [← ofReal_add, ofReal_ne_zero]
    simp only [ne_eq, ne_of_gt (sSupNormIm_eps_pos f hε 0), not_false_eq_true]
  · apply Differentiable.const_cpow (Differentiable.neg differentiable_id)
    apply Or.inl
    rw [← ofReal_add, ofReal_ne_zero]
    exact (ne_of_gt (sSupNormIm_eps_pos f hε 1))

Goal state after:
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
η₀ : ∀ x ∈ t₁, ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0
η₁ : ∀ x ∈ t₂, ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0
⊢ meromorphicOrderAt f w ≠ ⊤

Tactic:
simp [h₂w]

Goal state after:
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
⊢ log ‖h w‖ =
    ∑ᶠ (i : ℂ), ↑((divisor f (ball 0 R)) i) * log ‖canonicalFactor R i w‖ -
        ∑ᶠ (i : ℂ), ↑((divisor f (sphere 0 R)) i) * log ‖w - i‖ +
      log ‖meromorphicTrailingCoeffAt f w‖

Tactic:
calc Real.log ‖h w‖
    _ = log ‖((∏ᶠ (i : ℂ), canonicalFactor R i w ^ (divisor f B₀R) i)
        * ∏ᶠ (i : ℂ), (w - i) ^ (-divisor f S₀R) i) • meromorphicTrailingCoeffAt f w‖ := by
      rw [D.eq_smul_meromorphicTrailingCoeffAt_of_meromorphicOrderAt
        h₁w h₂w hR, finprod_eq_prod_of_mulSupport_subset (s := t₂) _ (by aesop)]
    _ = log ‖((∏ i ∈ t₂, canonicalFactor R i w ^ (divisor f B₀R) i)
        * ∏ i ∈ t₁, (w - i) ^ (-divisor f S₀R) i) • meromorphicTrailingCoeffAt f w‖ := by
      rw [finprod_eq_prod_of_mulSupport_subset (s := t₂) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₁) _ _]
      <;> simpa [ht₁, ht₂] using mulSupport_pow_subset_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‖ := by
      have η₀ (x) (hx : x ∈ t₁) : ‖w - x‖ ^ (-divisor f S₀R) x ≠ 0 := by
        refine zpow_ne_zero _ ?_
        rw [norm_ne_zero_iff, sub_ne_zero]
        rintro rfl
        simp_all [divisor_def, ← Finset.mem_coe]
      have η₁ (x) (hx : x ∈ t₂) : ‖canonicalFactor R x w‖ ^ (divisor f B₀R) x ≠ 0 := by
        refine zpow_ne_zero _ ?_
        rw [norm_ne_zero_iff]
        have h₁x : x ∈ ball 0 R := (divisor f B₀R).supportWithinDomain (ht₂ ▸ hx)
        refine canonicalFactor_ne_zero h₁x h₁w fun _ ↦ ?_
        simp_all [divisor_def, ← Finset.mem_coe]
      simp_rw [norm_smul, norm_mul, norm_prod, norm_zpow]
      rw [Real.log_mul (mul_ne_zero_iff.2 ⟨Finset.prod_ne_zero_iff.2 η₁,
          Finset.prod_ne_zero_iff.2 η₀⟩) ?_, Real.log_mul (Finset.prod_ne_zero_iff.2 η₁)
        (Finset.prod_ne_zero_iff.2 η₀), Real.log_prod η₁, Real.log_prod η₀]
      simpa using (D.meromorphicOn w h₁w).meromorphicTrailingCoeffAt_ne_zero (by simp [h₂w])
    _ = ((∑ᶠ i, (divisor f B₀R i) * Real.log ‖canonicalFactor R i w‖)
        - (∑ᶠ i, (divisor f S₀R i) * Real.log ‖w - i‖))
        + Real.log ‖meromorphicTrailingCoeffAt f w‖ := by
      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.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
⊢ |d * (w - ↑a * I).im| ≤ d * b

Tactic:
sub_im,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
w : ℂ
hw : |w.im - a| ≤ b
⊢ |d * (w.im - (↑a * I).im)| ≤ d * b
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
R : ℝ
hR : expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) ≤ C
Hle : ∀ (a_1 : ℂ), |a_1.re| = R → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
w : ℂ
hre : |w.re| = R
him : w.im ∈ Ioo (a - b) (a + b)
⊢ ‖g ε w‖ * ‖f w‖ ≤ expR (δ * expR (d * |w.re|)) * expR (B * expR (c * |w.re|)) * A

Tactic:
mul_assoc,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
R : ℝ
hR : expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) ≤ C
Hle : ∀ (a_1 : ℂ), |a_1.re| = R → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
w : ℂ
hre : |w.re| = R
him : w.im ∈ Ioo (a - b) (a + b)
⊢ ‖g ε w‖ * ‖f w‖ ≤ expR (δ * expR (d * |w.re|)) * (expR (B * expR (c * |w.re|)) * A)
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
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
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
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑x * I * I)‖ ≤ C

Tactic:
mul_assoc,

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Ioi 0)
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
H : MapsTo (fun x ↦ x * I) (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Ioi 0)
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Ioi 0)] fun z ↦ expR (B * ‖z‖ ^ c)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (↑x * (I * I))‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case inr.refine_2
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ Filter.Tendsto (fun x ↦ log x * x) (pure 0) (𝓝 0)

Tactic:
convert! tendsto_pure_nhds (fun x ↦ log x * x) 0

Goal state after:
this : Set.univ = Set.Iio 0 ∪ Set.Ioi 0 ∪ {0}
⊢ 0 = log 0 * 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inl
x : ℝ
hx : x < 0
⊢ -(sin x * x * x⁻¹) ≤ 1

Tactic:
mul_assoc,

Goal state after:
case inl
x : ℝ
hx : x < 0
⊢ -(sin x * (x * x⁻¹)) ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ ‖x⁻¹‖ ≤ x ^ s

Tactic:
simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hx.1)]

Goal state after:
s t : ℝ
ht : 0 < t
h : s ≤ -1
H : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
I : 0 < min 1 t
H' : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 (min 1 t)) volume
x : ℝ
hx : x ∈ Ioo 0 (min 1 t)
⊢ x⁻¹ ≤ x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: case hab.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
⊢ s ∈ Ioo (min 0 1) (max 0 1) → HasDerivAt (fun x ↦ -(x * log x - x)) ((-log) s) s

Tactic:
⟨hs, _⟩

Goal state after:
case hab.hderiv
a b x : ℝ
hx : 0 < x
s : ℝ
hs : min 0 1 < s
right✝ : s < max 0 1
⊢ HasDerivAt (fun x ↦ -(x * log x - x)) ((-log) s) s
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ -(Complex.sin ↑r * Complex.I * Complex.I - -Complex.sin ↑r * Complex.I * Complex.I) = 2 * Complex.sin ↑r

Tactic:
mul_assoc,

Goal state after:
r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * Complex.I * Complex.I) = 2 * Complex.sin ↑r
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * Complex.I * Complex.I) = 2 * Complex.sin ↑r

Tactic:
mul_assoc,

Goal state after:
r : ℝ
⊢ -(Complex.sin ↑r * (Complex.I * Complex.I) - -Complex.sin ↑r * (Complex.I * Complex.I)) = 2 * Complex.sin ↑r
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log ‖a‖

Tactic:
by
  rw [InnerProductSpace.HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg]
  intro x hx
  apply AnalyticAt.harmonicAt_log_norm (by fun_prop)
  rw [sub_ne_zero]
  by_contra!
  simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right]
  linarith

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

Goal state before:
pp: case refine_2
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ContinuousOn (fun x ↦ x⁻¹ / log x) [[a, b]]

Tactic:
fun_prop (disch := grind [log_pos, Set.uIcc])

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

Goal state before:
pp: case refine_2
a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ContinuousOn (fun x ↦ -x⁻¹ * (log x)⁻¹ ^ 2) [[a, b]]

Tactic:
fun_prop (disch := grind [log_pos, Set.uIcc])

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

Goal state before:
pp: case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ ↑((1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))

Tactic:
simp_rw [ofReal_sub, ofReal_div, this a (t + 1), this b (t + 1)]

Goal state after:
case e'_3
a b t : ℝ
ht : t ≠ -1
this : ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s
⊢ (1 + ↑b ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) - (1 + ↑a ^ 2) ^ ↑(t + 1) / ↑(2 * (t + 1)) =
    (1 + ↑b ^ 2) ^ (↑t + 1) / (2 * (↑t + 1)) - (1 + ↑a ^ 2) ^ (↑t + 1) / (2 * (↑t + 1))
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law : ∀ (r₁ : ℝ), ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ r₀ * ‖circleMap 0 R θ - ρ‖ ^ 2 / R ≤ ‖circleMap 0 r θ - ρ‖ ^ 2

Tactic:
div_le_iff₀ hR

Goal state after:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law : ∀ (r₁ : ℝ), ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ r₀ * ‖circleMap 0 R θ - ρ‖ ^ 2 ≤ ‖circleMap 0 r θ - ρ‖ ^ 2 * R
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]

Goal state after:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π < 0
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
⊢ z = P.roots.toFinset.centerMass (P.derivRootWeight z) id

Tactic:
set weight : ℂ → ℝ := P.derivRootWeight z
  set s := P.roots.toFinset
  suffices ∑ x ∈ s, weight x • (z - x) = 0 by calc
    z = s.centerMass weight fun _ ↦ z := by
      rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
      exact (sum_derivRootWeight_pos hP z).ne'
    _ = s.centerMass weight (z - ·) + s.centerMass weight id := by
      simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]
    _ = s.centerMass weight id := by
      simp only [add_eq_right, Finset.centerMass, this, smul_zero]
  by_cases hzP : P.eval z = 0
  · simp only [weight, derivRootWeight, if_pos hzP]
    rw [Finset.sum_eq_single z] <;> simp_all
  calc
    ∑ x ∈ s, weight x • (z - x) = conj (∑ x ∈ s, P.rootMultiplicity x • (1 / (z - x))) := by
      simp only [map_sum, weight, derivRootWeight, if_neg hzP]
      refine Finset.sum_congr rfl fun x hx ↦ ?_
      have : z - x ≠ 0 := by
        rw [sub_ne_zero]
        rintro rfl
        simp_all [s]
      simp [← Complex.conj_mul', field]
    _ = conj (P.roots.map fun x ↦ 1 / (z - x)).sum := by
      simp only [Finset.sum_multiset_map_count, P.count_roots, s]
    _ = 0 := by
      rw [← (IsAlgClosed.splits _).eval_derivative_div_eval_of_ne_zero hzP]
      simp [hz]

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

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

Tactic:
replace hp := hp.leadingCoeff_isUnit

Goal state after:
q : ℤ[X]
this : ¬0 < q.natDegree
p : ℤ[X]
h : ∀ (z : ℂ), ¬((aeval z) (q * p) = 0 ∧ (aeval z) (q * p).mirror = 0)
hq' : q ∣ (q * p).mirror
hp : IsUnit (q * p).leadingCoeff
⊢ IsUnit q
Module: Mathlib.Topology.UrysohnsBounded

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (⇑f) 0 s
hft : EqOn (⇑f) 1 t
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∈ s
⊢ (BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X a x

Tactic:
by simp [hfs hx]

Goal state after: