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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ ball 0 R
⊢ g z ≠ 0

Tactic:
rw [← MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff (h₂g (ball_subset_closedBall hz))]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
φ : ℂ → E := (∏ᶠ (c : ℂ), canonicalFactor R c ^ (divisor f (ball 0 R)) c) • f
hφ : MeromorphicOn φ (closedBall 0 R)
g : ℂ → E := toMeromorphicNFOn φ (closedBall 0 R)
h₃g : divisor g (ball 0 R) = 0
h₂g : MeromorphicNFOn g (closedBall 0 R)
h₄g : ∀ {z : ℂ}, z ∈ closedBall 0 R → meromorphicOrderAt g z ≠ ⊤
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ ball 0 R
⊢ meromorphicOrderAt g z = 0
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
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
a : 𝕜
hx : a ∈ U
h₁f h₁a : ∀ᶠ (x : 𝕜) in 𝓝[≠] a, f x = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
hax : a ≠ x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0

Tactic:
· exact h₁a

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
hx : x ∈ U
h₁f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
a : 𝕜
h₁a : ∀ᶠ (x : 𝕜) in 𝓝[{x}ᶜ] a, f x = 0
hax : a ≠ x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] a, f z = 0
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
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
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
H' : ↑I × A → E
⊢ H' = ⇑(cov.liftHomotopy H f H_0) →
    (∀ (a : A), Continuous[_, inst✝²] fun x ↦ H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a

Tactic:
rintro rfl; refine ⟨fun a ↦ ?_, cov.liftHomotopy_lifts H f H_0, cov.liftHomotopy_zero H f H_0⟩
    simp_rw [liftHomotopy_apply]; exact (cov.liftPath _ _ <| H_0 a).2

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ cf ≤ max cf cg

pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ 0 ≤ max 0 (max Bf Bg)

pp: case refine_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ Bf ≤ max 0 (max Bf Bg)

pp: case refine_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ cg ≤ max cf cg

pp: case refine_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ 0 ≤ max 0 (max Bf Bg)

pp: case refine_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
u : ℂ → ℝ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[l] fun z ↦ expR (Bf * expR (cf * |u z|))
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[l] fun z ↦ expR (Bg * expR (cg * |u z|))
⊢ Bg ≤ max 0 (max Bf Bg)

Tactic:
exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _),
    le_max_right _ _, le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cf ≤ max cf cg

pp: case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

pp: case refine_3
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bf ≤ max 0 (max Bf Bg)

pp: case refine_4
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ cg ≤ max cf cg

pp: case refine_5
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ 0 ≤ max 0 (max Bf Bg)

pp: case refine_6
E : Type u_1
inst✝ : NormedAddCommGroup E
a : ℝ
f g : ℂ → E
l : Filter ℂ
this :
  ∀ {c₁ c₂ B₁ B₂ : ℝ},
    c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → (fun z ↦ expR (B₁ * ‖z‖ ^ c₁)) =O[cobounded ℂ ⊓ l] fun z ↦ expR (B₂ * ‖z‖ ^ c₂)
cf : ℝ
hcf : cf < a
Bf : ℝ
hOf : f =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bf * ‖z‖ ^ cf)
cg : ℝ
hcg : cg < a
Bg : ℝ
hOg : g =O[cobounded ℂ ⊓ l] fun z ↦ expR (Bg * ‖z‖ ^ cg)
⊢ Bg ≤ max 0 (max Bf Bg)

Tactic:
exacts [le_max_left _ _, le_max_left _ _, (le_max_left _ _).trans (le_max_right _ _),
    le_max_right _ _, le_max_left _ _, (le_max_right _ _).trans (le_max_right _ _)]

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

Goal state before:
pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₁
⊢ meromorphicTrailingCoeffAt (fun x_1 ↦ x_1 - x) w ≠ 0

Tactic:
rw [meromorphicTrailingCoeffAt_id_sub_const]

Goal state after:
case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
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
this : MeromorphicAt h w
x : ℂ
hx : x ∈ t₁
⊢ (if w = x then 1 else w - x) ≠ 0
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 : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
hmero : MeromorphicAt f x
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)

Tactic:
meromorphicOrderAt_eq_int_iff hmero.deriv

Goal state after:
𝕜 : 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 : ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
hmero : MeromorphicAt f x
⊢ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, deriv f z = (z - x) ^ (n - 1) • g z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
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
x : ℂ
h₃x : ¬(divisor f (ball 0 R)) x = 0
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x

Tactic:
have h₁x : x ∈ ball 0 R := (divisor f (ball 0 R)).supportWithinDomain h₃x

Goal state after:
case neg
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
x : ℂ
h₃x : ¬(divisor f (ball 0 R)) x = 0
h₁x : x ∈ ball 0 R
⊢ meromorphicTrailingCoeffAt (canonicalFactor R x) w ^ (divisor f (ball 0 R)) x =
    canonicalFactor R x w ^ (divisor f (ball 0 R)) x
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f 1

Tactic:
← hz1

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz1 : z.re = 1
⊢ ‖f z‖ ≤ ε + sSupNormIm f z.re
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 : dist w.im a ≤ b
⊢ |(aff w).im| ≤ d * b

Tactic:
Real.dist_eq

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
⊢ |(aff w).im| ≤ d * b
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 0) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 0 = 0
Module: Mathlib.Analysis.Complex.Hadamard

Goal state before:
pp: case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ↑(sSupNormIm f 1) ≠ 0

Tactic:
simp only [Ne, ofReal_eq_zero]

Goal state after:
case neg.refine_2.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 1 = 0
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₁
⊢ ∀ (m n₁ n₂ : E), ∂_{m} (∂_{n₁ + n₂} f) = ∂_{m} (∂_{n₁} f) + ∂_{m} (∂_{n₂} f)

Tactic:
simp [lineDerivOp_left_add, lineDerivOp_add]

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

Goal state before:
pp: case hf.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ sSupNormIm f 0 ≠ 0 ∨ 0 ≤ 1 - z.re

Tactic:
· right; simp only [sub_nonneg, le_of_lt hz.2]

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

Goal state before:
pp: case right
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)

Tactic:
rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
      div_le_one (by simp [hul]), sub_le_sub_iff_right l]
    exact hz.2

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hw : w ∈ ball c |R|
hR : |R| ≤ 0
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c |R| = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
R : ℝ
c w : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hw : w ∈ ball c |R|
hR : |R| ≤ 0
⊢ circleAverage (fun z ↦ ((z - c) / (z - w)) • f z) c R = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℝ
a : ℝ
hf : CircleIntegrable f c R
h₂f : ∀ x ∈ sphere c |R|, f x ≤ a
⊢ ∫ (θ : ℝ) in 0..2 * π, f (circleMap c R θ) ≤ ∫ (θ : ℝ) in 0..2 * π, a

Tactic:
exact intervalIntegral.integral_mono_on_of_le_Ioo (le_of_lt two_pi_pos) hf
    intervalIntegrable_const (fun θ _ ↦ h₂f (circleMap c R θ) (circleMap_mem_sphere' c R θ))

Goal state after:
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))
h₃F : DifferentiableOn ℂ F (closure (ball c R))
x : ℂ
hx : x ∈ sphere c R
⊢ (re ∘ herglotzRieszKernel c w • f) x = (⇑reCLM ∘ fun z ↦ ((z - c + (w - c)) / (z - c - (w - c))).re • F z) x

Tactic:
simp [h₂F (sphere_subset_ball (lt_add_of_pos_left R h₁e) hx), herglotzRieszKernel_def]

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

Goal state before:
pp: ⊢ -1 + (algebraMap ℤ ℂ) 1 = 0

Tactic:
eq_intCast,

Goal state after:
⊢ -1 + ↑1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case neg
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
⊢ x - 1 < x * log x

Tactic:
cases lt_or_eq_of_le h0 <;> aesop

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : R ≤ 0
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w

Tactic:
let q := ‖w‖ / R

Goal state after:
case inr.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
⊢ Real.circleAverage (fun z ↦ ((z + w) / (z - w)).re • f z) 0 R = f w
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : ℂ → E
R : ℝ
w : ℂ
inst✝ : CompleteSpace E
hf : DiffContOnCl ℂ f (ball 0 R)
hw : w ∈ ball 0 R
hR : 0 < R
h₁w : w ≠ 0
W : ℂ := ↑R * cexp (↑w.arg * I)
q : ℝ := ‖w‖ / R
h₁q : 0 < q
h₂q : q < 1
η₀ : ∀ {x : ℂ}, ‖x‖ ≤ R → ↑q * x - W ≠ 0
⊢ ∮ (z : ℂ) in C(0, R), (↑q / (↑q * z - W)) • f z = 0

Tactic:
by
      apply DifferentiableOn.diffContOnCl ?_ |>.smul hf |>.circleIntegral_eq_zero hR.le
      rw [closure_ball 0 hR.ne']
      fun_prop (disch := aesop)

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

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

pp: case neg.inr.refine_2.inr
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
⊢ IntervalIntegrable (fun x ↦ ‖↑x ^ r‖) μ 0 c

Tactic:
· -- case `0 ≤ c`: integrand is identically 1
    have : IntervalIntegrable (fun _ => 1 : ℝ → ℝ) μ 0 c := intervalIntegrable_const
    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hc] at this ⊢
    refine IntegrableOn.congr_fun this (fun x hx => ?_) measurableSet_Ioc
    rw [Complex.norm_cpow_eq_rpow_re_of_pos hx.1, ← h', rpow_zero]

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

Goal state before:
pp: case inl
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 : R ≤ 0
⊢ Real.circleAverage (re ∘ herglotzRieszKernel c w • f) c R = f w

Tactic:
simp_all [ball_eq_empty.2 hR]

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

Goal state before:
pp: x : ℝ
⊢ log⁺ x = 0 ↔ |x| ≤ 1

Tactic:
rw [← posLog_abs, ← log_nonpos_iff (abs_nonneg x)]

Goal state after:
x : ℝ
⊢ log⁺ |x| = 0 ↔ log |x| ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∫ (x : ℝ) in 0..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)

Tactic:
apply integral_eq_sub_of_hasDeriv_right

Goal state after:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c ↦ ↑c ^ (r + 1) / (r + 1)) [[0, c]]

case hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (min 0 c) (max 0 c), HasDerivWithinAt (fun c ↦ ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

case hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y ↦ ↑y ^ r) MeasureTheory.volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
· calc
      ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by
        rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]
      _ = ∫ x in b - a..0, (-x) ^ n := by
        simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
        refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl
        rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
        exact hx.2
      _ = |b - a| ^ (n + 1) / (n + 1) := by
        simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

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 ≠ ⊤
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((divisor f (sphere c |R|)).finiteSupport (isCompact_sphere c |R|))
    have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
    apply CircleIntegrable.congr_codiscreteWithin h₄g.symm
    apply CircleIntegrable.add
    · apply CircleIntegrable.finsum
      intro i
      apply IntervalIntegrable.const_mul
      apply MeromorphicOn.intervalIntegrable_log_norm
      apply AnalyticOnNhd.meromorphicOn
      apply AnalyticOnNhd.sub _ analyticOnNhd_const
      apply (analyticOnNhd_circleMap c R).mono (by tauto)
    · apply ContinuousOn.intervalIntegrable
      apply ContinuousOn.log
      · apply ContinuousOn.norm
        apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn
        intro x hx
        simp
      · intro x hx
        rw [ne_eq, norm_eq_zero]
        apply h₂g ⟨circleMap c R x, circleMap_mem_sphere' c R x⟩

Goal state after: