mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
y : 𝕜
⊢ ContinuousAt f y → y ∈ U \ {x} → AnalyticAt 𝕜 f y

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : ∀ᶠ (y : 𝕜) in 𝓝[U \ {x}] x, ContinuousAt f y
y : 𝕜
hy : ContinuousAt f y
⊢ y ∈ U \ {x} → AnalyticAt 𝕜 f y
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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
y : 𝕜
⊢ AnalyticAt 𝕜 f y → AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ AnalyticAt 𝕜 f y ∨ y ∉ U
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
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
y : 𝕜
⊢ y ∈ Uᶜ → AnalyticAt 𝕜 f y ∨ y ∉ U

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
h : MeromorphicOn f U
hx : x ∈ U
this : {x}ᶜ = U \ {x} ∪ Uᶜ
y : 𝕜
hy : y ∈ Uᶜ
⊢ AnalyticAt 𝕜 f y ∨ y ∉ U
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
x : 𝕜
hx : x ∈ U
y : 𝕜
⊢ AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ → y ∈ (U \ {x | AnalyticAt 𝕜 f x})ᶜ

Tactic:
hy

Goal state after:
𝕜 : 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
y : 𝕜
hy : AnalyticAt 𝕜 f y ∨ y ∈ Uᶜ
⊢ y ∈ (U \ {x | AnalyticAt 𝕜 f x})ᶜ
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})
γ : FundamentalGroup X x
⊢ γ ∈ (⋯.monodromyPerm x).ker ↔ γ ∈ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

Tactic:
constructor <;> intro h

Goal state after:
case mp
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})
γ : FundamentalGroup X x
h : γ ∈ (⋯.monodromyPerm x).ker
⊢ γ ∈ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range

case mpr
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})
γ : FundamentalGroup X x
h : γ ∈ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } ⋯).range
⊢ γ ∈ (⋯.monodromyPerm x).ker
Module: Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Goal state before:
pp: case e_f
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ w m ⊗ₜ[ℝ] w m = ∑ n, ⟪w m, w n⟫_ℝ • w m ⊗ₜ[ℝ] w n

Tactic:
rw [Fintype.sum_eq_single m _, orthonormal_iff_ite.1 w.orthonormal]

Goal state after:
case e_f
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ w m ⊗ₜ[ℝ] w m = (if m = m then 1 else 0) • w m ⊗ₜ[ℝ] w m

E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
ι : Type u_2
inst✝ : Fintype ι
v : OrthonormalBasis ι ℝ E
w : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
m : Fin (Module.finrank ℝ E)
⊢ ∀ (x : Fin (Module.finrank ℝ E)), x ≠ m → ⟪w m, w x⟫_ℝ • w m ⊗ₜ[ℝ] w x = 0
Module: Mathlib.Analysis.Complex.Hadamard

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

Tactic:
apply differentiableAt_id

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
x : E
h : HarmonicAt f x
⊢ Δ (-f) =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [h.2] with x hx
    simp_all [laplacian_neg]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
⊢ HarmonicAt (⇑l ∘ f) x ↔ HarmonicAt f x

Tactic:
constructor <;> intro h

Goal state after:
case mp
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
h : HarmonicAt (⇑l ∘ f) x
⊢ HarmonicAt f x

case mpr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : E → F
x : E
l : F ≃L[ℝ] G
h : HarmonicAt f x
⊢ HarmonicAt (⇑l ∘ f) x
Module: Mathlib.Analysis.Complex.HasPrimitives

Goal state before:
pp: case calc_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
inst✝ : CompleteSpace E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
h : IsConservativeOn f (ball c r)
⊢ (fun x' ↦ c.wedgeIntegral x' f - c.wedgeIntegral z f - (x' - z) • f z) =ᶠ[𝓝 z] fun w ↦
    z.wedgeIntegral w f - (w - z) • f z

Tactic:
exact (h.eventually_nhds_wedgeIntegral_sub_wedgeIntegral f_cont hz).mono <| by simp

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = a
⊢ (z * -I).re = a

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z✝ : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z✝.re
hzb : z✝.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
z : ℂ
hz : z.im = b
⊢ (z * -I).re = b

pp: case refine_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ a ≤ (z * I).im

pp: case refine_5
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b C : ℝ
f : ℂ → E
z : ℂ
hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)
hB : ∃ c < π / (b - a), ∃ B, f =O[comap (abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z ↦ expR (B * expR (c * |z.im|))
hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C
hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C
hza : a ≤ z.re
hzb : z.re ≤ b
H : MapsTo (fun x ↦ x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)
⊢ (z * I).im ≤ b

Tactic:
all_goals simpa

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

Goal state before:
pp: case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
⊢ y ∈ ball z R → fderivWithin ℝ (⇑reCLM ∘ F) (ball z R) y = fderivWithin ℝ f (ball z R) y

Tactic:
hy

Goal state after:
case right.hf'
f : ℂ → ℝ
z : ℂ
R : ℝ
hf : HarmonicOnNhd f (ball z R)
hR : ¬R ≤ 0
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : DifferentiableOn ℂ g (ball z R)
F : ℂ → ℂ
hF : F z = ↑(f z) ∧ ∀ x ∈ ball z R, HasDerivAt F (g x) x
h₁F : DifferentiableOn ℂ F (ball z R)
h₂F : DifferentiableOn ℝ F (ball z R)
x : ℂ
hx : x ∈ ball z R
y : ℂ
hy : y ∈ ball z R
⊢ fderivWithin ℝ (⇑reCLM ∘ F) (ball z R) y = fderivWithin ℝ f (ball z R) y
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : HarmonicOnNhd f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ HarmonicContOnCl f s

Tactic:
exact h.harmonicContOnCl

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

Goal state before:
pp: f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
⊢ y ∈ univ → fderivWithin ℝ (⇑reCLM ∘ F) univ y = fderivWithin ℝ f univ y

Tactic:
hy

Goal state after:
f : ℂ → ℝ
hf : HarmonicOnNhd f univ
g : ℂ → ℂ := (⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) 1) - I • ⇑ofRealCLM ∘ fun x ↦ (fderiv ℝ f x) I
hg : Differentiable ℂ g
F : ℂ → ℂ
hF : F 0 = ↑(f 0) ∧ ∀ x ∈ univ, HasDerivAt F (g x) x
h₁F : ∀ (z₁ : ℂ), HasDerivAt F (g z₁) z₁
h₂F : Differentiable ℂ F
h₃F : Differentiable ℝ F
x y : ℂ
hy : y ∈ univ
⊢ fderivWithin ℝ (⇑reCLM ∘ F) univ y = fderivWithin ℝ f univ y
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : ContinuousOn f {z | ‖z - c‖ ∈ s}
hs : ∀ r ∈ s, 0 ≤ r
⊢ ContinuousOn (Real.circleAverage f c) s

Tactic:
rw [continuousOn_iff_continuous_domRestrict] at *

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
s : Set ℝ
c : ℂ
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z | ‖z - c‖ ∈ s}.domRestrict f)
hs : ∀ r ∈ s, 0 ≤ r
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s.domRestrict (Real.circleAverage f c))
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: θ φ r R : ℝ
h₁ : 0 < r
h₂ : r < R
⊢ ¬‖↑R * cexp (↑θ * I)‖ = ‖↑r * cexp (↑φ * I)‖

Tactic:
by simpa [abs_of_pos, h₁, h₁.trans h₂] using h₂.ne'

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

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

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

Tactic:
· nlinarith [Real.log_inv x, Real.log_lt_sub_one_of_pos (inv_pos.mpr hx_pos) (by aesop),
      mul_inv_cancel₀ hx_pos.ne']

Goal state after:
case neg
x : ℝ
h0 : 0 ≤ x
h1 : x ≠ 1
hx_pos : ¬0 < x
⊢ x - 1 < x * log x
Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R : ℝ
w c z : ℂ
hz : z ∈ sphere c R
hw : w ∈ ball c R
⊢ (R - ‖w - c‖) / (R + ‖w - c‖) ≤ ((z - c + (w - c)) / (z - c - (w - c))).re

Tactic:
by
  obtain ⟨η₀, rfl, η₂⟩ : 0 < R ∧ R = ‖z - c‖ ∧ z - c ≠ 0 := by
    grind [ball_eq_empty, mem_sphere, dist_eq_norm, norm_pos_iff]
  by_cases h₁w : ‖w - c‖ = 0
  · aesop
  simpa using le_re_herglotzRieszKernel_aux (z - c).arg (w - c).arg ‖w - c‖ ‖z - c‖
    (by simpa using h₁w) (mem_ball_iff_norm.1 hw)

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

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

Tactic:
hy

Goal state after:
x : ℝ
hx : ¬x = 0
y : ℝ
hy : y ≠ 0
⊢ deriv (fun x ↦ x * log x) y = log y + 1
Module: Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions

Goal state before:
pp: z : ℂ
g : ℂ → ℂ
h₁g : AnalyticAt ℂ g z
h₂g : g z ≠ 0
h₃g : g z ∈ slitPlane
⊢ Real.log ∘ ⇑normSq ∘ g =ᶠ[𝓝 z] ⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g)

Tactic:
· have t₀ := h₁g.differentiableAt.continuousAt.preimage_mem_nhds
      ((isOpen_slitPlane.inter isOpen_ne).mem_nhds ⟨h₃g, h₂g⟩)
    calc Real.log ∘ normSq ∘ g
    _ =ᶠ[𝓝 z] reCLM ∘ ofRealCLM ∘ Real.log ∘ normSq ∘ g := by aesop
    _ =ᶠ[𝓝 z] reCLM ∘ log ∘ ((conjCLE ∘ g) * g) := by
      filter_upwards with x
      simp only [Function.comp_apply, ofRealCLM_apply, Pi.mul_apply, conjCLE_apply]
      rw [ofReal_log, normSq_eq_conj_mul_self]
      exact normSq_nonneg (g x)
    _ =ᶠ[𝓝 z] reCLM ∘ (log ∘ conjCLE ∘ g + log ∘ g) := by
      filter_upwards [t₀] with x hx
      simp only [Function.comp_apply, Pi.mul_apply, conjCLE_apply, Pi.add_apply]
      congr
      rw [Complex.log_mul_eq_add_log_iff _ hx.2, Complex.arg_conj]
      · simp [Complex.slitPlane_arg_ne_pi hx.1, Real.pi_pos, Real.pi_nonneg]
      · simpa [ne_eq, map_eq_zero] using hx.2
    _ =ᶠ[𝓝 z] ⇑reCLM ∘ (⇑conjCLE ∘ log ∘ g + log ∘ g) := by
      apply Filter.eventuallyEq_iff_exists_mem.2
      use g ⁻¹' (Complex.slitPlane ∩ {0}ᶜ), t₀
      intro x hx
      simp only [Function.comp_apply, Pi.add_apply, conjCLE_apply]
      congr 1
      rw [← Complex.log_conj]
      simp [Complex.slitPlane_arg_ne_pi hx.1]

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

Goal state before:
pp: case refine_1
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
this✝ : IntegrableOn (fun x ↦ x⁻¹) (Ioo 0 (min 1 t)) volume
this : IntervalIntegrable (fun x ↦ x⁻¹) volume 0 (min 1 t)
⊢ False

Tactic:
simp [intervalIntegrable_inv_iff, I.ne] at this

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

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

Tactic:
refine (measurable_of_continuousOn_compl_singleton (0 : ℝ) ?_).aestronglyMeasurable
    exact continuousOn_of_forall_continuousAt fun x hx =>
      Complex.continuousAt_ofReal_cpow_const x r (Or.inr hx)

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
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : ‖z - ↑x₀‖ < ‖↑x₀‖
⊢ z ∈ {z | 0 < z.re}

Tactic:
Complex.norm_of_nonneg hx₀

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : Tendsto (fun x ↦ f ↑x) atTop (𝓝 0)
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hle : ∀ (C' : ℝ), (∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C') → ∀ (z : ℂ), 0 ≤ z.re → ‖f z‖ ≤ max C C'
x₀ : ℝ
hx₀ : 0 ≤ x₀
h : C < ‖f ↑x₀‖
hmax : IsMaxOn (norm ∘ f) {z | 0 < z.re} ↑x₀
z : ℂ
hz : ‖z - ↑x₀‖ < x₀
⊢ z ∈ {z | 0 < z.re}
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
⊢ IntervalIntegrable log volume a b

Tactic:
apply intervalIntegrable_of_even (log_neg_eq_log · |>.symm)
  intro x hx
  -- Split integral
  apply IntervalIntegrable.trans (b := 1)
  · -- Show integrability on [0…1] using non-negativity of the derivative
    rw [← neg_neg log]
    apply IntervalIntegrable.neg
    apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x))
    · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg
    · intro s ⟨hs, _⟩
      norm_num at *
      simpa using! (hasDerivAt_id s).sub (hasDerivAt_mul_log hs.ne.symm)
    · intro s ⟨hs₁, hs₂⟩
      grind [Pi.neg_apply, log_nonpos_iff]
  · -- Show integrability on [1…t] by continuity
    apply ContinuousOn.intervalIntegrable
    apply Real.continuousOn_log.mono
    apply Set.notMem_uIcc_of_lt zero_lt_one at hx
    simpa

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

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
⊢ y ∈ Set.Ici 0 → x ≤ y → log⁺ x ≤ log⁺ y

Tactic:
hy

Goal state after:
x : ℝ
hx : x ∈ Set.Ici 0
y : ℝ
hy : y ∈ Set.Ici 0
⊢ x ≤ y → log⁺ x ≤ log⁺ y
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
hx : x = 0
y : ℝ
⊢ y ∈ Metric.ball x 1 → 0 = log⁺ y

Tactic:
hy

Goal state after:
x : ℝ
hx : x = 0
y : ℝ
hy : y ∈ Metric.ball x 1
⊢ 0 = log⁺ y
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

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

Goal state after:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
hf : MeromorphicOn f [[a, b]]
⊢ IntervalIntegrable (log ∘ f) volume a b

Tactic:
rw [(by aesop : log ∘ f = (log ‖f ·‖))]
  exact hf.intervalIntegrable_log_norm

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

Goal state before:
pp: case neg
r : ℝ
hr : ¬r = 0
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sinc r)

Tactic:
rw [sinc_of_ne_zero hr]

Goal state after:
case neg
r : ℝ
hr : ¬r = 0
⊢ 2 * ↑(sin r) = 2 * ↑r * ↑(sin r / r)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: h : ℝ
hh : 0 < h
⊢ Tendsto (invQParam h) (𝓝[≠] 0) I∞

Tactic:
simp only [tendsto_comap_iff, comp_def, im_invQParam]
  apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))
  exact Real.tendsto_log_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
obtain ⟨z₀, hz₀, h⟩ := h

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
z₀ : E
hz₀ : z₀ ∈ U
h : ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case h
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
y : ℝ
q : ℂ
hq : q ∈ S
hq2 : q ∉ {0}
⊢ (norm ∘ cuspFunction h f) q = y → y ≤ c

Tactic:
hy

Goal state after:
case h
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, y ∈ {0}ᶜ → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
y : ℝ
q : ℂ
hq : q ∈ S
hq2 : q ∉ {0}
hy : (norm ∘ cuspFunction h f) q = y
⊢ y ≤ c
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
this : ∑ x ∈ s, weight x • (z - x) = 0
⊢ z = s.centerMass weight fun x ↦ z

Tactic:
rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
      exact (sum_derivRootWeight_pos hP z).ne'

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ z - c ∈ Metric.eball 0 ↑r'

Tactic:
Metric.eball_coe

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ z - c ∈ Metric.ball 0 ↑r'
Module: Mathlib.Analysis.Complex.TaylorSeries

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

Tactic:
Metric.eball_coe

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ ‖ε‖ / ‖f z - x‖ < 1

Tactic:
Real.norm_of_nonneg hε₀.le,

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ ε / ‖f z - x‖ < 1