mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case e_a.e_a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
m : ℕ
p : 𝕜 → 𝕜
hq_ne : ¬q (g x) = 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hm : ↑m = analyticOrderAt (fun x_1 ↦ g x_1 - g x) x
h₁p : AnalyticAt 𝕜 p x
h₂p : ¬p x = 0
h₃p : ∀ᶠ (z : 𝕜) in 𝓝 x, g z - g x = (z - x) ^ m * p z
a : 𝕜
h₁a : g a - g x = (a - x) ^ m * p a
h₂a : f (g a) = (((a - x) ^ m) ^ n * p a ^ n) • q (g a)
⊢ ((a - x) ^ m) ^ n = (a - x) ^ (n * ↑m)

Tactic:
rw [mul_comm, zpow_mul, zpow_natCast]

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

Goal state before:
pp: case mpr.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
hu : ¬(MeromorphicOn.divisor f U) u = 0
⊢ u ∈ f ⁻¹' {0}

Tactic:
Set.mem_preimage,

Goal state after:
case mpr.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
h₁f : MeromorphicNFOn f U
h₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
hu : ¬(MeromorphicOn.divisor f U) u = 0
⊢ f u ∈ {0}
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case h₂
𝕜 : 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
⊢ meromorphicTrailingCoeffAt f₁ x + -meromorphicTrailingCoeffAt f₂ x ≠ 0

Tactic:
← sub_eq_add_neg

Goal state after:
case h₂
𝕜 : 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
⊢ meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
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
this : U ∈ Filter.codiscreteWithin U
a : 𝕜
h₁a : AnalyticAt 𝕜 f a
h₂a : a ∈ U
⊢ f a = toMeromorphicNFOn f U a

Tactic:
simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 h₁a.meromorphicNFAt).symm]

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

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
h'o : meromorphicOrderAt f x = ⊤
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
apply tendsto_const_nhds.congr'
    filter_upwards [meromorphicOrderAt_eq_top_iff.1 h'o] with y hy using hy.symm

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

Goal state before:
pp: case refine_1.coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
nneg : 0 ≤ meromorphicOrderAt f x
n : ℤ
h₀ : meromorphicOrderAt f x = ↑n
g : 𝕜 → E
hg : AnalyticAt 𝕜 g x
hfg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • g z) x

Tactic:
exact (AnalyticAt.zpow_nonneg (by fun_prop) (by simpa [h₀] using nneg)).smul hg

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

Goal state before:
pp: R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))) w = -1

Tactic:
fun_meromorphicOrderAt_div (by fun_prop) (by fun_prop),

Goal state after:
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ meromorphicOrderAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w - meromorphicOrderAt (fun z ↦ ↑R * (z - w)) w = -1
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
cov : IsCoveringMap p
γ : C(↑I, X)
e : E
γ_0 : γ 0 = p e
U : X → Set X := fun x ↦ ⋯.choose
mem_base : ∀ (x : X), x ∈ ⋯.choose
U_open : ∀ (x : X), IsOpen[inst✝] ⋯.choose
h✝ : ∀ (x : X), IsOpen[inst✝¹] (p ⁻¹' ⋯.choose)
H : (x : X) → ↑(p ⁻¹' ⋯.choose) ≃ₜ ↑⋯.choose × ↑(p ⁻¹' {x})
x✝ : ∀ (x : X) (x_1 : ↑(p ⁻¹' ⋯.choose)), ↑((H x) x_1).1 = p ↑x_1
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub✝ : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
n : ℕ
Γ : ↑I → E
cont : ContinuousOn Γ (Set.Icc 0 (t n))
eqOn : Set.EqOn (p ∘ Γ) (⇑γ) (Set.Icc 0 (t n))
Γ_0 : Γ 0 = e
x : X
t_sub : Set.Icc (t n) (t (n + 1)) ⊆ ⇑γ ⁻¹' ⋯.choose
pΓtn : p (Γ (t n)) = γ (t n)
this : Nonempty ↑(p ⁻¹' {x})
q : Bundle.Trivialization (↑(p ⁻¹' {x})) p := ⋯.toTrivialization
⊢ ContinuousOn (fun s ↦ q.invFun (γ s, (↑q (Γ (t n))).2)) (Set.Icc 0 (t (n + 1)) ∩ closure {a | ¬a ≤ t n})

Tactic:
apply q.continuousOn_invFun.comp ((Continuous.prodMk_left _).comp γ.2).continuousOn
    simp_rw [not_le, q.target_eq]; intro s h
    exact ⟨t_sub ⟨closure_lt_subset_le continuous_const continuous_subtype_val h.2, h.1.2⟩, ⟨⟩⟩

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

Goal state before:
pp: t : |2⁻¹| = 2⁻¹
z : |429895798851992810179897 / 620208537104218167705600 + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z

Goal state after:
t : |2⁻¹| = 2⁻¹
z : |log 2 - 429895798851992810179897 / 620208537104218167705600| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℤ
hn : ↑n ≠ 0
hf : meromorphicOrderAt f x = ↑n
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)

Tactic:
have hmero : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero (by aesop)
  rw [meromorphicOrderAt_eq_int_iff hmero] at hf
  rw [meromorphicOrderAt_eq_int_iff hmero.deriv]
  obtain ⟨g, hga, hg0, (hg : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z)⟩ := hf
  refine ⟨fun z ↦ (n : 𝕜) • g z + (z - x) • deriv g z, by fun_prop, by simpa using ⟨hn, hg0⟩, ?_⟩
  filter_upwards [hga.eventually_analyticAt.filter_mono (nhdsWithin_le_nhds),
    eventually_mem_nhdsWithin, hg.nhdsNE_deriv] with z hgz hmem hz
  have hzx : z - x ≠ 0 := by simpa [sub_eq_zero] using hmem
  calc
    deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z :=
      hz
    _ = (z - x) ^ n • deriv g z + deriv ((· ^ n) ∘ (· - x)) z • g z :=
      deriv_fun_smul (by fun_prop (disch := grind)) hgz.differentiableAt
    _ = (z - x) ^ n • deriv g z + (n * (z - x) ^ (n - 1)) • g z := by
      rw [deriv_comp _ (by fun_prop (disch := grind)) (by fun_prop)]
      simp [deriv_zpow]
    _ = (z - x) ^ (n - 1) • ((n : 𝕜) • g z + (z - x) • deriv g z) := by
      simp [smul_smul, ← zpow_add_one₀ hzx, add_comm, mul_comm]

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

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
he : p e₀ = f a₀
le : (FundamentalGroup.map f a₀).range ≤ (mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range
⊢ ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

Tactic:
by
  refine cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
    fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_
  · simpa [and_comm] using cov.exists_path_lifts (f.comp γ) e₀ (by simp [γ_0, he])
  rw [(cov.eq_liftPath_iff' <| by simp [γ_0, he]).mpr ⟨Γ_lifts, Γ_0⟩,
    (cov.eq_liftPath_iff' <| by simp [γ'_0, he]).mpr ⟨Γ'_lifts, Γ'_0⟩]
  let pγ : Path a₀ (γ 1) := ⟨γ, γ_0, rfl⟩
  let pγ' : Path a₀ (γ 1) := ⟨γ', γ'_0, γγ'1.symm⟩
  change (cov.monodromy (.mk <| pγ.map f.continuous) ⟨e₀, he⟩).1 =
    (cov.monodromy (.mk <| pγ'.map f.continuous) ⟨e₀, he⟩).1
  rw [← Subtype.ext_iff]
  apply (cov.monodromy_bijective <| .mk (pγ'.map f.continuous).symm).1
  simp_rw [← monodromy_trans_apply, ← mk_trans]
  conv_rhs => rw [← eq.2 ⟨.reflTransSymm _⟩, mk_refl, monodromy_refl]
  rw [Path.map_symm, ← Path.map_trans]
  set pγγ' : Path a₀ a₀ := pγ.trans pγ'.symm
  obtain ⟨⟨pΓΓ'⟩, eq⟩ := le ⟨fromPath (.mk pγγ'), rfl⟩
  rw [mapOfEq_apply, map_apply, ← mk_map] at eq
  exact eq ▸ Subtype.ext congr($(cov.monodromy_map <| .mk _))

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

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : C(A, ↑s)
he : p e₀ = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
⊢ e₀ ∈ p ⁻¹' s

Tactic:
Set.mem_preimage,

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
e₀ : E
f : C(A, ↑s)
he : p e₀ = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
⊢ p e₀ ∈ s
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
a : A
⊢ F' a ∈ p ⁻¹' s

Tactic:
Set.mem_preimage,

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
p : E → X
inst✝¹ : SimplyConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
s : Set X
cov : IsCoveringMapOn p s
a₀ : A
f : C(A, ↑s)
hs : ∀ (a : A), ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a ∈ s
F : C(A, ↑(p ⁻¹' s))
hF : s.restrictPreimage p ∘ ⇑F = ⇑f
he : p ↑(F a₀) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp f) a₀
hF_unique : ∀ (y : C(A, ↑(p ⁻¹' s))), (fun F_1 ↦ F_1 a₀ = F a₀ ∧ s.restrictPreimage p ∘ ⇑F_1 = ⇑f) y → y = F
F' : C(A, E)
hF'₁ : F' a₀ = ↑(F a₀)
hF'₂ : ∀ (x : A), p (F' x) = ↑(f x)
a : A
⊢ p (F' a) ∈ s
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
p : E → X
G : Type u_4
inst✝² : Group G
inst✝¹ : MulAction G E
hp : IsQuotientCoveringMap p G
x : X
e : ↑(p ⁻¹' {x})
inst✝ : PathConnectedSpace E
⊢ Surjective ⇑(hp.fundamentalGroupToMulOpposite e)

Tactic:
by
  intro g
  set e' : p⁻¹' {x} := ⟨MulOpposite.unop g • (e : E), by
    have := hp.map_smul (e := e) (MulOpposite.unop g); aesop⟩ with he'
  set Γ : Path (e : E) (e' : E) :=
    { toFun := PathConnectedSpace.somePath (e : E) (e' : E)
      continuous_toFun := by fun_prop
      source' := by simp
      target' := by simp }
  set γ : Path x x := (Γ.map hp.continuous).cast
    (by simpa using e.property.symm) (by simpa using e'.property.symm)
  use .fromPath ⟦γ⟧
  rw [fundamentalGroupToMulOpposite_apply_eq_Iff]
  change (e' : E) = _
  rw [← hp.isCoveringMap.monodromy_eq_of_map_eq (γ := ⟦γ⟧) (Γ := ⟦Γ⟧) rfl]

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

Goal state before:
pp: case pos.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ 0 = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z

Tactic:
· simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]
      right
      rw [eq_comm]
      simp only [Complex.ext_iff, zero_re, ne_of_lt hz.1, false_and, not_false_eq_true]

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
δ : ℝ
δ₀ : δ < 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|)) * expR (Real.log A)

Tactic:
Real.exp_log hA₀,

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.Distribution.DerivNotation

Goal state before:
pp: V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{init (tail m)} (∂_{m (last n.succ)} f)) = ∂^{init m} (∂_{m (last (n + 1))} f)

Tactic:
iteratedLineDerivOp_succ_left,

Goal state after:
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
f : E
n : ℕ
IH : ∀ (m : Fin (n + 1) → V), ∂^{m} f = ∂^{init m} (∂_{m (last n)} f)
m : Fin (n + 1 + 1) → V
hmzero : init m 0 = m 0
hmtail : tail m (last n) = m (last n.succ)
⊢ ∂_{m 0} (∂^{init (tail m)} (∂_{m (last n.succ)} f)) = ∂_{init m 0} (∂^{tail (init m)} (∂_{m (last (n + 1))} f))
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case succ
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
y : V
f : E
n : ℕ
IH : ∂^{fun x ↦ y} f = ∂_{y}^[n] f
⊢ ∂^{fun x ↦ y} f = ∂_{y}^[n + 1] f

Tactic:
iteratedLineDerivOp_succ_left,

Goal state after:
case succ
V : Type u_11
E : Type u_12
inst✝ : LineDeriv V E E
y : V
f : E
n : ℕ
IH : ∂^{fun x ↦ y} f = ∂_{y}^[n] f
⊢ ∂_{y} (∂^{tail fun x ↦ y} f) = ∂_{y}^[n + 1] f
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case succ
V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
m : Fin (n + 1) → V
⊢ ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y

Tactic:
iteratedLineDerivOp_succ_left,

Goal state after:
case succ
V : Type u_5
E : Type u_6
inst✝³ : LineDeriv V E E
inst✝² : AddCommGroup V
inst✝¹ : AddCommGroup E
inst✝ : LineDerivAdd V E E
x y : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (x + y) = ∂^{m} x + ∂^{m} y
m : Fin (n + 1) → V
⊢ ∂_{m 0} (∂^{tail m} (x + y)) = ∂_{m 0} (∂^{tail m} x) + ∂_{m 0} (∂^{tail m} y)
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: case succ
R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x
m : Fin (n + 1) → V
⊢ ∂^{m} (r • x) = r • ∂^{m} x

Tactic:
iteratedLineDerivOp_succ_left,

Goal state after:
case succ
R : Type u_4
V : Type u_5
E : Type u_6
inst✝² : LineDeriv V E E
inst✝¹ : SMul R E
inst✝ : LineDerivSMul R V E E
r : R
x : E
n : ℕ
IH : ∀ (m : Fin n → V), ∂^{m} (r • x) = r • ∂^{m} x
m : Fin (n + 1) → V
⊢ ∂_{m 0} (∂^{tail m} (r • x)) = r • ∂_{m 0} (∂^{tail m} x)
Module: Mathlib.Analysis.Complex.Hadamard

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

Tactic:
simp only [scale, smul_eq_mul, sub_re] at hgoal

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

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
have hint : IntegrableOn f (Ι a b) μ := hf.integrableOn_of_subset_isCompact
    isCompact_uIcc measurableSet_uIoc uIoc_subset_uIcc hμfin

Goal state after:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
inst✝ : NullSingletonClass μ
hf : ContinuousOn f [[a, b]]
hμfin : μ (Ι a b) ≠ ⊤
hμ0 : μ (Ι a b) ≠ 0
hint : IntegrableOn f (Ι a b) μ
⊢ ∃ c ∈ uIoo a b, f c = ⨍ (x : ℝ) in Ι a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 θ)⁻¹ = ∫ (θ : ℝ) in 0..2 * π, f (circleMap 0 1 (-θ))

Tactic:
simp [circleMap_zero_inv]

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

Goal state before:
pp: z : ℍ
⊢ Function.Injective fun x ↦ x • z

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ h
  simp_all [UpperHalfPlane.ext_iff, ne_zero]

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

Goal state before:
pp: case neg
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b

Tactic:
rcases lt_or_eq_of_le h with (h' | h')

Goal state after:
case neg.inl
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 < r.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b

case neg.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ r) μ a b
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
c : ℂ
hf : DiffContOnCl ℂ f (ball c R)
hw : w ∈ ball c R
hR : 0 < R
h₁g : DiffContOnCl ℂ (fun z ↦ f (z + c)) (ball 0 R)
h₂g : w - c ∈ ball 0 R
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
simpa [← circleAverage_map_add_const, herglotzRieszKernel_def]
    using circleAverage_re_smul_on_ball_zero h₁g h₂g

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

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

Tactic:
intervalIntegral.integral_neg

Goal state after:
a b : ℝ
ha : 1 < a
hb : 1 < b
this : -∫ (x : ℝ) in a..b, x⁻¹ / log x ^ 2 = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹
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]]
⊢ HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x

Tactic:
convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1

Goal state after:
case e'_9.e'_6
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ ↑x = ↑x ^ (2 - 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
θ r₁ : ℝ
| r₁ * ‖ρ‖ * Real.cos (θ + -ρ.arg)

Tactic:
← sub_eq_add_neg

Goal state after:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
| r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ↑h / (2 * ↑π * I) * (2 * ↑π * I * (z / ↑h) + ↑m * (2 * ↑π * I)) = z + ↑m * ↑h

Tactic:
mul_comm (m : ℂ),

Goal state after:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * ↑π * I * z / ↑h)) = 2 * ↑π * I * z / ↑h + ↑m * (2 * ↑π * I)
⊢ ↑h / (2 * ↑π * I) * (2 * ↑π * I * (z / ↑h) + 2 * ↑π * I * ↑m) = z + ↑m * ↑h