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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
· aesop

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case top
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
⊢ ↑n * ⊤ + ⊤ = (↑n + 1) * ⊤

pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝

Tactic:
· aesop

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
hf : MeromorphicAt f x
n : ℕ
hn : meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
a✝ : ℤ
⊢ ↑n * ↑a✝ + ↑a✝ = (↑n + 1) * ↑a✝
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case pos
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z

pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : ¬z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z

Tactic:
· aesop

Goal state after:
case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz : ¬z ∉ U
⊢ (∑ x ∈ h.toFinset, F x • locallyFinsuppWithin.restrict (single x 1) ⋯) z = F z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
U : Set X
F : locallyFinsuppWithin U ℤ
h : F.support.Finite
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (∑ c ∈ h.toFinset, F c * if z ∈ U then (single c 1) z else 0) = F z

Tactic:
· aesop

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

Goal state before:
pp: case refine_4
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
this : Continuous[_, inst✝¹] fun st ↦ (Γ st.2) st.1
⊢ (Γ t) 1 = (Γ 0) 1

pp: case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

pp: case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1

Tactic:
· apply sep.const_of_comp homeo.isLocallyInjective (this.comp (.prodMk_right 1))
    intro t t'; change p (Γ _ _) = p (Γ _ _); simp_rw [Γ_lifts, γ.eq_fst _ (.inr rfl)]

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ (p ∘ fun st ↦ (Γ st.2) st.1) = ⇑((↑γ).comp ContinuousMap.prodSwap)

case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ Continuous[_, inst✝¹] fun x ↦ (Γ (0, x).2) (0, x).1

case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
p : E → X
homeo : IsLocalHomeomorph p
sep : IsSeparatedMap p
γ₀ γ₁ : C(↑I, X)
γ : γ₀.HomotopyRel γ₁ {0, 1}
Γ : ↑I → C(↑I, E)
Γ_lifts : ∀ (t s : ↑I), p ((Γ t) s) = γ (t, s)
Γ_0 : ∀ (t : ↑I), (Γ t) 0 = (Γ 0) 0
t : ↑I
⊢ ∀ (a : ↑I), Continuous[_, inst✝¹] fun x ↦ (Γ (x, a).2) (x, a).1
Module: Mathlib.Analysis.Complex.Isometry

Goal state before:
pp: f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE

Tactic:
have h0 : f I = I ∨ f I = -I := by
    simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
    constructor
    · rw [← I_re]
      exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
    · apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
      intro z
      rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]

Goal state after:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case succ.refine_1.refl
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
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ Γ (t n) = q.invFun (γ (t n), (↑q (Γ (t n))).2)

Tactic:
rw [← pΓtn]

Goal state after:
case succ.refine_1.refl
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
hs : t n ∈ Set.Icc 0 (t (n + 1)) ∩ frontier {a | a ≤ t n}
⊢ Γ (t n) = q.invFun (p (Γ (t n)), (↑q (Γ (t n))).2)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DivInvMonoid α
f : β → α
g : β → ℤ
x✝ : β
⊢ ¬f x✝ ^ g x✝ = 1 → ¬g x✝ = 0

Tactic:
contrapose!

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DivInvMonoid α
f : β → α
g : β → ℤ
x✝ : β
⊢ g x✝ = 0 → f x✝ ^ g x✝ = 1
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 : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
hU : IsConnected U
⊢ (∃ u ∈ U, meromorphicOrderAt f u ≠ ⊤) ↔ ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤

Tactic:
convert exists_meromorphicOrderAt_ne_top_iff_forall hf hU
  <;> simp

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

Goal state before:
pp: this : |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Tactic:
norm_num1 at *
    assumption

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

Goal state before:
pp: this : |log 3 - 109861228867 / 100000000000| ≤ (2 / 3) ^ 71 / 3⁻¹ + (1 / 10 ^ 10 - (2 / 3) ^ 71 / 3⁻¹)
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / 10 ^ 10

Tactic:
norm_num1 at *
    assumption

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

Goal state before:
pp: this : |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / 10 ^ 10

Tactic:
norm_num1 at *
    assumption

Goal state after:
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
inst✝ : SimplyConnectedSpace E
e : ↑(p ⁻¹' {x}) := ⟨⋯.choose, ⋯⟩
f : FundamentalGroup E ↑e →* FundamentalGroup X x := FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯
this : Subsingleton ↥f.range
⊢ f.range = ⊥

Tactic:
exact Subgroup.eq_bot_of_subsingleton _

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ (fun x ↦ invInterpStrip f x ε • f x) =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z ↦
    Real.exp (BF * Real.exp (0 * |z.im|))

Tactic:
Asymptotics.isBigO_iff

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : 0 < ε
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalClosedStrip 0 1
BF : ℝ
hBF : ∀ a ∈ verticalClosedStrip 0 1, ‖F f ε a‖ ≤ BF
⊢ ∃ c,
    ∀ᶠ (x : ℂ) in comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1),
      ‖invInterpStrip f x ε • f x‖ ≤ c * ‖Real.exp (BF * Real.exp (0 * |x.im|))‖
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ √(((↑z.re + ↑c.im * I).re - c.re) ^ 2 + ((↑z.re + ↑c.im * I).im - c.im) ^ 2) ≤
    √((z.re - c.re) ^ 2 + (z.im - c.im) ^ 2)

Tactic:
Real.le_sqrt (by positivity) (by positivity),

Goal state after:
c z : ℂ
r : ℝ
hz : z ∈ ball c r
⊢ √(((↑z.re + ↑c.im * I).re - c.re) ^ 2 + ((↑z.re + ↑c.im * I).im - c.im) ^ 2) ^ 2 ≤
    (z.re - c.re) ^ 2 + (z.im - c.im) ^ 2
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ √(((↑z.re + ↑y * I).re - c.re) ^ 2 + ((↑z.re + ↑y * I).im - c.im) ^ 2) ≤ √((z.re - c.re) ^ 2 + (z.im - c.im) ^ 2)

Tactic:
Real.le_sqrt (by positivity) (by positivity),

Goal state after:
c z : ℂ
r y : ℝ
z_in_ball : z ∈ closedBall c r
y_in_I : y ∈ Ι c.im z.im
⊢ √(((↑z.re + ↑y * I).re - c.re) ^ 2 + ((↑z.re + ↑y * I).im - c.im) ^ 2) ^ 2 ≤ (z.re - c.re) ^ 2 + (z.im - c.im) ^ 2
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ (norm ∘ scale f l u) z ∈ norm ∘ f '' verticalClosedStrip l u

Tactic:
exact ⟨l + z * (u - l), scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hz, rfl⟩

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 : IsBigOWith A (comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))) f fun z ↦ expR (B * expR (c * |z.re|))
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
simp only [isBigOWith_iff, eventually_inf_principal, eventually_comap, mem_Ioo,
      mem_preimage, (· ∘ ·), Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] at 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|))
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C
Module: Mathlib.Analysis.Distribution.DerivNotation

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

Tactic:
induction n with
  | zero =>
    simp
  | succ n IH =>
    simp_rw [iteratedLineDerivOp_succ_left, IH, lineDerivOp_add]

Goal state after:
Module: Mathlib.Analysis.Distribution.DerivNotation

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
R : Type u_4
V : Type u_5
E : Type u_6
F : Type u_7
V₁ : Type u_8
V₂ : Type u_9
V₃ : Type u_10
inst✝¹⁴ : LineDeriv E V₁ V₂
inst✝¹³ : LineDeriv E V₂ V₃
inst✝¹² : AddCommGroup V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : AddCommGroup V₃
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
inst✝⁶ : Module R V₂
inst✝⁵ : Module R V₃
inst✝⁴ : LineDerivAdd E V₂ V₃
inst✝³ : LineDerivAdd E V₁ V₂
inst✝² : LineDerivSMul R E V₂ V₃
inst✝¹ : LineDerivLeftSMul R E V₁ V₂
inst✝ : LineDerivLeftSMul R E V₂ V₃
f : V₁
⊢ ∀ (c : R) (m n : E), ∂_{c • m} (∂_{n} f) = c • ∂_{m} (∂_{n} f)

Tactic:
by simp [lineDerivOp_left_smul]

Goal state after:
Module: Mathlib.Analysis.Complex.Harmonic.Liouville

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ f z = f w

Tactic:
← sub_eq_zero,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
h_harm : HarmonicOnNhd f univ
h_bound : IsBounded (range f)
z w : ℂ
ℓ : StrongDual ℝ E
h₁ℓ : ‖ℓ‖ ≤ 1
h₂ℓ : ℓ (f z) - ℓ (f w) = ‖f z - f w‖
η₁ : IsBounded (range (⇑ℓ ∘ f))
⊢ f z - f w = 0
Module: Mathlib.Analysis.Complex.Harmonic.Poisson

Goal state before:
pp: f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
have h₃F : DifferentiableOn ℂ F (closure (ball c R)) := by
    intro x hx
    apply (h₁F x _).differentiableWithinAt
    grind [mem_ball, mem_closedBall.1 (closure_ball_subset_closedBall hx)]

Goal state after:
f : ℂ → ℝ
c w : ℂ
R : ℝ
hf : HarmonicOnNhd f (closedBall c R)
hw : w ∈ ball c R
e : ℝ
h₁e : 0 < e
h₂e : ball c (e + R) ⊆ {x | HarmonicAt f x}
F : ℂ → ℂ
h₁F : AnalyticOnNhd ℂ F (ball c (e + R))
h₂F : Set.EqOn (fun z ↦ (F z).re) f (ball c (e + R))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
⊢ circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case pos
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
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

pp: case neg
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
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)

Tactic:
· aesop

Goal state after:
case neg
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
⊢ ((z - c + (w - c)) / (z - c - (w - c))).re ≤ (‖z - c‖ + ‖w - c‖) / (‖z - c‖ - ‖w - c‖)
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: case pos
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
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

pp: case neg
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
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Tactic:
· aesop

Goal state after:
case neg
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
⊢ (‖z - c‖ - ‖w - c‖) / (‖z - c‖ + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ deriv (fun x ↦ x * log x) x = (fun x ↦ log x + 1) x

Tactic:
exact deriv_mul_log hx.ne'

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

Goal state before:
pp: case mpr.h
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ DifferentiableWithinAt ℝ negMulLog {0}ᶜ x

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

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

Goal state before:
pp: case mpr.hs
x : ℝ
hx : x ≠ 0
this✝ : x ∈ {0}ᶜ
this : DifferentiableWithinAt ℝ negMulLog {0}ᶜ x
⊢ {0}ᶜ ∈ 𝓝 x

Tactic:
simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true,
      compl_singleton_mem_nhds_iff]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc

Goal state before:
pp: case inr.inr
x : ℝ
hx : 0 < x
⊢ sin x ≤ 1

Tactic:
exact sin_le_one x

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

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = (-x) ^ 0 * ‖Complex.exp (↑π * Complex.I * r)‖

Tactic:
rpow_zero,

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = 1 * ‖Complex.exp (↑π * Complex.I * r)‖
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ IntervalIntegrable (fun x ↦ 1 / (1 + x ^ 2)) μ a b

Tactic:
apply Continuous.intervalIntegrable

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous fun x ↦ 1 / (1 + x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max (0 + 0) (log (x * y)) ≤ max 0 (log x) + max 0 (log y)

Tactic:
log_mul ha hb

Goal state after:
case neg
x y : ℝ
ha : ¬x = 0
hb : ¬y = 0
⊢ max (0 + 0) (log x + log y) ≤ max 0 (log x) + max 0 (log y)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) * ∫ (x : ℝ) in Ι a b, RCLike.re (↑x ^ ↑r) ∂MeasureTheory.volume =
    (if a ≤ b then 1 else -1) * RCLike.re (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume)

Tactic:
integral_re

Goal state after:
case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ (if a ≤ b then 1 else -1) * RCLike.re (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume) =
    (if a ≤ b then 1 else -1) * RCLike.re (∫ (x : ℝ) in Ι a b, ↑x ^ ↑r ∂MeasureTheory.volume)

case e'_2
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
h' : -1 < (↑r).re ∨ ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
⊢ MeasureTheory.Integrable (fun x ↦ ↑x ^ ↑r) (MeasureTheory.volume.restrict (Ι a b))
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case e'_2.inl
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
h' : -1 < (↑r).re
⊢ IntervalIntegrable (fun x ↦ ↑x ^ ↑r) MeasureTheory.volume a b

pp: case e'_2.inr
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
h' : ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x ↦ ↑x ^ ↑r) MeasureTheory.volume a b

Tactic:
· exact intervalIntegrable_cpow' h'

Goal state after:
case e'_2.inr
a b r : ℝ
h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
this : (∫ (x : ℝ) in a..b, ↑x ^ ↑r).re = ((↑b ^ (↑r + 1) - ↑a ^ (↑r + 1)) / (↑r + 1)).re
h' : ↑r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ IntervalIntegrable (fun x ↦ ↑x ^ ↑r) MeasureTheory.volume a b
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, |x| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n

Tactic:
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl

Goal state after:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0