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

Goal state before:
pp: case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
⊢ ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) z

Tactic:
refine ⟨z, frontier_interior_subset hzU, fun x hx => (hle hx).out.trans_eq ?_⟩

Goal state after:
case inl
E : Type u
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℂ F
inst✝¹ : Nontrivial E
inst✝ : FiniteDimensional ℂ E
f : E → F
U : Set E
hb : Bornology.IsBounded U
hne : U.Nonempty
hd : DiffContOnCl ℂ f U
hc : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
w : E
hle : IsMaxOn (norm ∘ f) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) w
hwU : w ∈ interior U
this : interior U ≠ univ
z : E
hzU : z ∈ frontier (interior U)
hzw : infDist w (interior U)ᶜ = dist w z
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ (norm ∘ f) w = (norm ∘ f) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
    simp [deriv_zero_of_not_differentiableAt this, h, sq]

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ z ∈ s \ {x}

Tactic:
simp [hz.2.ne, hz.1]

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

Goal state before:
pp: case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

pp: case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Tactic:
· rw [tan_zero]

Goal state after:
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x < -1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
by
  rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]; congr 2; ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) (-y) = angle x y

Tactic:
unfold angle
  rw [inner_neg_neg, norm_neg, norm_neg]

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
convert! hθ

Goal state after:
case e'_4
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ -π + 2 * π = π
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: n : ℕ+
⊢ Continuous fun x ↦ x ^ n

Tactic:
by
  simp only [isEmbedding_coe.continuous_iff, Function.comp_def, coe_pow]
  fun_prop

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

Goal state before:
pp: z : 𝕔𝔻
⊢ ‖↑z‖ ^ 2 ≤ 1

Tactic:
sq_le_one_iff_abs_le_one,

Goal state after:
z : 𝕔𝔻
⊢ |‖↑z‖| ≤ 1
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: n : ℕ
⊢ Continuous fun x ↦ x ^ n

Tactic:
by
  simp only [isEmbedding_coe.continuous_iff, Function.comp_def, coe_pow]
  fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
⊢ ∀ z ∈ U,
    ∃ t ∈ 𝓝 z,
      (t ∩ Function.support fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0).Finite

Tactic:
by
    simp_all only [Function.support_subset_iff, ne_eq, ite_eq_right_iff, WithTop.untop₀_eq_zero,
      and_imp, Classical.not_imp, not_or, implies_true,
      ← supportDiscreteWithin_iff_locallyFiniteWithin]
    by_cases hf : MeromorphicOn f U
    · filter_upwards [mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
        hf.codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top]
      simp only [Set.mem_image, Set.mem_ofPred_eq, Subtype.exists, exists_and_left, exists_prop,
        exists_eq_right_right, Pi.ofNat_apply, ite_eq_right_iff, WithTop.untop₀_eq_zero, and_imp]
      tauto
    · simp [hf, Pi.zero_def]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
⊢ divisor (f ^ n) U = n • divisor f U

Tactic:
by
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬meromorphicOrderAt f x = 0 := cs
⊢ f x = g x

Tactic:
t₀,

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬meromorphicOrderAt g x = 0
⊢ f x = g x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ MeromorphicAt f x

Tactic:
rw [MeromorphicAt.meromorphicAt_congr h]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z
⊢ MeromorphicAt (fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
⊢ MeromorphicAt f x

Tactic:
rw [MeromorphicAt.meromorphicAt_congr h]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
x : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
⊢ MeromorphicAt (fun z ↦ (z - x) ^ n • g z) x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
⊢ MeromorphicNFAt 1 x

Tactic:
apply AnalyticAt.meromorphicNFAt

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hf : MeromorphicNFAt f x
hn : n = 0
⊢ AnalyticAt 𝕜 1 x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h₂f : meromorphicOrderAt f x = ⊤
this : toMeromorphicNFAt f x =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt (toMeromorphicNFAt f x) x

Tactic:
apply AnalyticAt.meromorphicNFAt

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

Goal state before:
pp: case mp
𝕜 : 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 : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
⊢ x ∈ U → AnalyticAt 𝕜 f x

Tactic:
intro hx

Goal state after:
case mp
𝕜 : 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 : 0 ≤ MeromorphicOn.divisor f U
x : 𝕜
hx : x ∈ U
⊢ AnalyticAt 𝕜 f x
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 : 𝕜
this : ¬meromorphicOrderAt f u = 0 ↔ ¬f u ≠ 0
hu : ¬meromorphicOrderAt f u = 0 ∧ ¬meromorphicOrderAt f u = ⊤
⊢ f u = 0

Tactic:
simp_all [hu.1]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z : 𝕜
d : 𝕜 → ℤ
hd : (support d).Finite
⊢ meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ d u) z ≠ ⊤

Tactic:
simp [meromorphicOrderAt_eq d hd]

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

Goal state before:
pp: case refine_1
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ MeromorphicNFAt (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w

Tactic:
apply AnalyticAt.meromorphicNFAt

Goal state after:
case refine_1
R : ℝ
w : ℂ
h : w ∈ ball 0 R
⊢ AnalyticAt ℂ (fun z ↦ ↑R ^ 2 - (starRingEnd ℂ) w * z) w
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ MeromorphicNFAt (canonicalFactor R w) 0

Tactic:
apply AnalyticAt.meromorphicNFAt

Goal state after:
case neg
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
hw : ¬w = 0
⊢ AnalyticAt ℂ (canonicalFactor R w) 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ (fun x ↦ ↑(D u) * log ‖x - u‖) = 0 → D u = 0

Tactic:
intro hx

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
hx : (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
⊢ D u = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
⊢ D u = 0 → (fun x ↦ ↑(D u) * log ‖x - u‖) = 0

Tactic:
intro hx

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
D : locallyFinsuppWithin U ℤ
hg : ∀ (u : ↑U), g ↑u ≠ 0
h : f =ᶠ[codiscreteWithin U] (∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g
u : 𝕜
hx : D u = 0
⊢ (fun x ↦ ↑(D u) * log ‖x - u‖) = 0
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E := (fun z ↦ (z - x) ^ (n₁ - n)) • g₁ + (fun z ↦ (z - x) ^ (n₂ - n)) • g₂
h₁g : AnalyticAt 𝕜 g x
this : f₁ + f₂ =ᶠ[𝓝[≠] x] (fun x_1 ↦ x_1 - x) ^ n • g
t₀ : MeromorphicAt ((fun x_1 ↦ x_1 - x) ^ n) x
t₁ : meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n
⊢ min ↑n₁ ↑n₂ ≤ meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x + meromorphicOrderAt g x

Tactic:
t₁

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt f₂ x
meromorphicOrderAt_add : MeromorphicAt f₁ x → MeromorphicAt f₂ x → min ↑n₁ ↑n₂ ≤ meromorphicOrderAt (f₁ + f₂) x
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
g₂ : 𝕜 → E
h₁g₂ : AnalyticAt 𝕜 g₂ x
h₂g₂ : g₂ x ≠ 0
h₃g₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₂ z = (z - x) ^ n₂ • g₂ z
n : ℤ := min n₁ n₂
g : 𝕜 → E := (fun z ↦ (z - x) ^ (n₁ - n)) • g₁ + (fun z ↦ (z - x) ^ (n₂ - n)) • g₂
h₁g : AnalyticAt 𝕜 g x
this : f₁ + f₂ =ᶠ[𝓝[≠] x] (fun x_1 ↦ x_1 - x) ^ n • g
t₀ : MeromorphicAt ((fun x_1 ↦ x_1 - x) ^ n) x
t₁ : meromorphicOrderAt ((fun x_1 ↦ x_1 - x) ^ n) x = ↑n
⊢ min ↑n₁ ↑n₂ ≤ ↑n + meromorphicOrderAt g x
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
g : ℂ → E
D : CanonicalDecomp f g R
s₁ : 0 ∈ closedBall 0 R
⊢ 0 ∈ ball 0 R

Tactic:
simp [hR]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : meromorphicOrderAt f (g x) = ⊤
⊢ meromorphicOrderAt (f ∘ g) x = ⊤

Tactic:
rw [meromorphicOrderAt_eq_top_iff] at hf' ⊢

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
g : 𝕜 → 𝕜
hf : MeromorphicAt f (g x)
hg : AnalyticAt 𝕜 g x
hg_nc : ¬EventuallyConst g (𝓝 x)
hf' : ∀ᶠ (z : 𝕜) in 𝓝[≠] g x, f z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f ∘ g) z = 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 : meromorphicOrderAt f x = ↑n
⊢ meromorphicOrderAt (deriv f) x = ↑(n - 1)

Tactic:
by
  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.Analysis.Complex.Hadamard

Goal state before:
pp: l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalClosedStrip l u

Tactic:
simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc] at hz ⊢
  constructor <;> nlinarith [hz.1, hz.2, hul]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f

Tactic:
set I₇ :=     ∫ x in z.re..w.re, f (x + c.im * I)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
r : ℝ
f : ℂ → E
f_cont : ContinuousOn f (ball c r)
z : ℂ
hz : z ∈ ball c r
hf : IsConservativeOn f (ball c r)
w : ℂ
w_in_z_ball : w ∈ ball z (r - dist z c)
I₁ : E := ∫ (x : ℝ) in c.re..w.re, f (↑x + ↑c.im * I)
I₂ : E := I • ∫ (y : ℝ) in c.im..w.im, f (↑w.re + ↑y * I)
I₃ : E := ∫ (x : ℝ) in c.re..z.re, f (↑x + ↑c.im * I)
I₄ : E := I • ∫ (y : ℝ) in c.im..z.im, f (↑z.re + ↑y * I)
I₅ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)
I₆ : E := I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)
I₇ : E := ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑c.im * I)
⊢ c.wedgeIntegral w f - c.wedgeIntegral z f = z.wedgeIntegral w f
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 : ℂ
s : Set ℂ
hs : s.Countable
h₁f : ContinuousOn f (closedBall c |R|)
h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z
hR : R = 0
⊢ circleAverage f c R = f c

Tactic:
simp [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 : ℂ
hf : DiffContOnCl ℂ f (ball c |R|)
hR : R = 0
⊢ Real.circleAverage f c R = f c

Tactic:
simp [hR]

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

Goal state before:
pp: c : ℂ
R : ℝ
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
h : R ≠ 0
⊢ circleAverage f c R = (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z

Tactic:
calc circleAverage f c R
  _ = (↑(2 * π) : ℂ)⁻¹ • ∫ θ in 0..2 * π, f (circleMap c R θ) := by
    simp [circleAverage, ← coe_smul]
  _ = (2 * π * I)⁻¹ • ∫ θ in 0..2 * π, I • f (circleMap c R θ) := by
    rw [intervalIntegral.integral_smul, mul_inv_rev, smul_smul]
    match_scalars
    field
  _ = (2 * π * I)⁻¹ • (∮ z in C(c, R), (z - c)⁻¹ • f z) := by
    unfold circleIntegral
    congr with θ
    simp [deriv_circleMap, circleMap_sub_center, smul_smul]
    field_simp [circleMap_ne_center h]

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

Goal state before:
pp: x : ℂ
a : ℤ
⊢ x + ↑a ∈ ℂ_ℤ ↔ x ∈ ℂ_ℤ

Tactic:
simp only [mem_integerComplement_iff, not_iff_not]

Goal state after:
x : ℂ
a : ℤ
⊢ (∃ n, ↑n = x + ↑a) ↔ ∃ n, ↑n = x
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (-(↑x * I))‖ ≤ C

Tactic:
← neg_mul,

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : 0 ≤ z.re
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (-↑x * I)‖ ≤ C
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (-(↑x * I))‖ ≤ C

Tactic:
← neg_mul,

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Iio 0)
hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Iio 0)] fun z ↦ expR (B * ‖z‖ ^ c)
hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C
him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C
z : ℂ
hz_re : z.re ≤ 0
hz_im : 0 ≤ z.im
H : MapsTo Neg.neg (Iio 0 ×ℂ Ioi 0) (Ioi 0 ×ℂ Iio 0)
x : ℝ
hx : 0 ≤ x
⊢ ‖f (-↑x * I)‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: case mpr
x : ℝ
⊢ x ≠ 0 → DifferentiableAt ℝ negMulLog x

Tactic:
intro hx

Goal state after:
case mpr
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ negMulLog x
Module: Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasDerivAt negMulLog (-log x - 1) x

Tactic:
rw [← deriv_negMulLog hx, hasDerivAt_deriv_iff]
  refine DifferentiableOn.differentiableAt differentiableOn_negMulLog ?_
  simp [hx]

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

Goal state before:
pp: case refine_2
s t : ℝ
ht : 0 < t
h : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume

pp: case refine_1
s t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
⊢ -1 < s

Tactic:
· rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le ht.le]
    apply intervalIntegrable_rpow' h (a := 0) (b := t)

Goal state after:
case refine_1
s t : ℝ
ht : 0 < t
h : IntegrableOn (fun x ↦ x ^ s) (Ioo 0 t) volume
⊢ -1 < s