mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Extr

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f x‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖

Tactic:
hx

Goal state after:
α : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
l : Filter α
c : α
y : E
h : IsMaxFilter (norm ∘ f) l c
hy : SameRay ℝ (f c) y
x : α
hx : ‖f x‖ ≤ ‖f c‖
⊢ ‖f c‖ + ‖y‖ ≤ ‖f c‖ + ‖y‖
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case inl
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : M ≤ 1
⊢ Tendsto (fun z ↦ ∑' (n : ℕ), f n * z ^ n) ⊥ (𝓝 l)

Tactic:
tendsto_bot

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

Goal state before:
pp: case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
⊢ x ∈ Ioi 0 → 0 < deriv^[2] (fun x ↦ x ^ m) x

Tactic:
hx

Goal state after:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv^[2] (fun x ↦ x ^ m) x
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x ↦ √x * log x) x < 0

Tactic:
rw [deriv2_sqrt_mul_log x]

Goal state after:
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (4 * √x ^ 3) < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2

Tactic:
refine (iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)

Goal state after:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
⊢ x ∈ D → z ∈ D → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
hx

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
⊢ z ∈ D → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
hx✝ : cos x = 0
hx : Complex.cos ↑x = 0
⊢ Tendsto Complex.ofReal (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)

Tactic:
exact tendsto_principal_principal.2 fun y => mt Complex.ofReal_inj.1

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

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

Tactic:
by
    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.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1

Tactic:
hx

Goal state after:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + |x| ^ 5 / 100
⊢ sin x < x

Tactic:
hx

Goal state after:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 5 / 100
⊢ sin x < x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x y : ℝ
⊢ |sin x - sin y| ≤ |x - y|

Tactic:
simpa [edist_dist] using! lipschitzWith_sin x y

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 y x

Tactic:
unfold angle
  rw [real_inner_comm, mul_comm]

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → derivWithin f S x ≤ derivWithin f S b

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → derivWithin f S x ≤ derivWithin f S b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ MonotoneOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with rfl | hxy'
  · rfl
  exact (hfc.derivWithin_le_slope hx hy hxy' (hfd x hx)).trans
    (hfc.slope_le_derivWithin hx hy hxy' (hfd y hy))

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → deriv f x ≤ deriv f b

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → deriv f x ≤ deriv f b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x < b → derivWithin f S x < derivWithin f S b

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x < b → derivWithin f S x < derivWithin f S b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x < b → deriv f x < deriv f b

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x < b → deriv f x < deriv f b
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: case hdb
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
w : ℂ := ⋯
hzR : ‖z‖ < R
hwR : ‖f z / (2 * ↑M - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * ↑M - f z ≠ 0
⊢ 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
simpa using norm_sub_le_norm_add 1 w

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → derivWithin f S b ≤ derivWithin f S x

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x ≤ b → derivWithin f S b ≤ derivWithin f S x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
⊢ x ∈ S → ∀ ⦃b : ℝ⦄, b ∈ S → x < b → derivWithin f S b < derivWithin f S x

Tactic:
hx

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
⊢ ∀ ⦃b : ℝ⦄, b ∈ S → x < b → derivWithin f S b < derivWithin f S x
Module: Mathlib.Analysis.Complex.BorelCaratheodory

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
⊢ x ∈ ball 0 R → (fun {z} ↦ f z - f 0) ∈ {z | z.re ≤ M + ‖f 0‖}

Tactic:
hx

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hR : 0 < R
hz : z ∈ ball 0 R
x : ℂ
hx : x ∈ ball 0 R
⊢ (fun {z} ↦ f z - f 0) ∈ {z | z.re ≤ M + ‖f 0‖}
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)

Tactic:
rcases eq_or_ne z c with rfl | hne

Goal state after:
case inl
f : ℂ → ℂ
z : ℂ
R₂ : ℝ
n : ℕ
R₁ : ℝ
hR₁ : 0 < R₁
hn : (fun x ↦ f x - f z) =o[𝓝 z] fun w ↦ (w - z) ^ n
hz : z ∈ ball z R₁
hd : DifferentiableOn ℂ f (closedBall z R₁)
h_maps : MapsTo f (closedBall z R₁) (closedBall (f z) R₂)
⊢ ‖f z - f z‖ ≤ R₂ * (‖z - z‖ / R₁) ^ (n + 1)

case inr
f : ℂ → ℂ
c z : ℂ
R₂ : ℝ
n : ℕ
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
R₁ : ℝ
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hd : DifferentiableOn ℂ f (closedBall c R₁)
h_maps : MapsTo f (closedBall c R₁) (closedBall (f c) R₂)
hne : z ≠ c
⊢ ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
Module: Mathlib.Analysis.Complex.BranchLogRoot

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g✝ : X → ℂ
hgc : ContinuousOn g✝ U
hU₀ : 0 ∉ g✝ '' U
this✝ : SimplyConnectedSpace ↑U
this : LocallyPathConnectedSpace ↑U
x₀ : { x // x ∈ U }
hx₀ : g✝ ↑x₀ ≠ 0
f : C(↑U, ℂ)
hf : cexp ∘ ⇑f = ⇑{ toFun := U.domRestrict g✝, continuous_toFun := ⋯ }
g : X → ℂ
hg : ∀ (z : ↑U), g ↑z = f z
x : X
⊢ x ∈ U → (cexp ∘ g) x = g✝ x

Tactic:
hx

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g✝ : X → ℂ
hgc : ContinuousOn g✝ U
hU₀ : 0 ∉ g✝ '' U
this✝ : SimplyConnectedSpace ↑U
this : LocallyPathConnectedSpace ↑U
x₀ : { x // x ∈ U }
hx₀ : g✝ ↑x₀ ≠ 0
f : C(↑U, ℂ)
hf : cexp ∘ ⇑f = ⇑{ toFun := U.domRestrict g✝, continuous_toFun := ⋯ }
g : X → ℂ
hg : ∀ (z : ↑U), g ↑z = f z
x : X
hx : x ∈ U
⊢ (cexp ∘ g) x = g✝ x
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rcases eq_or_ne z c with rfl | hne

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f (ball z R₁)
h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)
hz : z ∈ ball z R₁
⊢ ‖dslope f z z‖ ≤ R₂ / R₁

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
⊢ x ∈ U → x ∈ {x | f =ᶠ[𝓝[≠] x] g}

Tactic:
hx

Goal state after:
case h.right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
⊢ x ∈ {x | f =ᶠ[𝓝[≠] x] g}
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
⊢ x ∈ U → {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
hx

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
h : f =ᶠ[codiscreteWithin U] g
x : 𝕜
hx : x ∈ U
⊢ {x | deriv f x = deriv g x} ∪ Uᶜ ∈ 𝓝[≠] x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
y : 𝕜
hy : y ∈ g ⁻¹' {0}ᶜ
⊢ f y = (g⁻¹ • g • f) y

Tactic:
rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage,
        Set.mem_singleton_iff] at hy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
hprod : MeromorphicNFAt (g • f) x
y : 𝕜
hy : ¬g y = 0
⊢ f y = (g⁻¹ • g • f) y
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x✝ : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x✝] 0
x : 𝕜
⊢ f x = 0 x → f⁻¹ x = 0 x

Tactic:
hx

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x✝ : 𝕜
f : 𝕜 → 𝕜
h : f =ᶠ[𝓝 x✝] 0
x : 𝕜
hx : f x = 0 x
⊢ f⁻¹ x = 0 x
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : MeromorphicOn f U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
x : 𝕜
⊢ x ∈ U → (U \ {x | f x ≠ 0})ᶜ ∈ 𝓝[≠] x

Tactic:
hx

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
hf : MeromorphicOn f U
h'f : ∀ x ∈ U, meromorphicOrderAt f x ≠ ⊤
x : 𝕜
hx : x ∈ U
⊢ (U \ {x | f x ≠ 0})ᶜ ∈ 𝓝[≠] 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
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x =
    meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

pp: case h₁
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt (-f₂) x

pp: case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0

Tactic:
· rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg]

Goal state after:
case h₁
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicOrderAt f₁ x = meromorphicOrderAt (-f₂) x

case h₂
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x
h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0
⊢ meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt (-f₂) x ≠ 0
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
x : 𝕜
⊢ x ∈ Uᶜ → toMeromorphicNFOn f U x = f x

Tactic:
hx

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ᶜ
⊢ toMeromorphicNFOn f U x = f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : a ∈ Uᶜ
⊢ toMeromorphicNFOn f U a = f a

Tactic:
simp only [Set.mem_compl_iff] at ha

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
U : Set 𝕜
hf : MeromorphicOn f U
hx : x ∈ U
a : 𝕜
ha : a ∉ U
⊢ toMeromorphicNFOn f U a = f a
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
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x = 0
⊢ (∃ c, c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0

pp: case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
⊢ (∃ c, c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0

Tactic:
· simp [ho, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho]

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
ho : meromorphicOrderAt f x ≠ 0
⊢ (∃ c, c ≠ 0 ∧ Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
⊢ x ∈ support (update d u₀ 0) → x ∈ ↑((Finite.toFinset hd).erase u₀)

Tactic:
hx

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
u₀ : 𝕜
hd : HasFiniteSupport d
h₁d : ¬d u₀ = 0
this✝ : (Function.mulSupport fun u ↦ (fun x ↦ x - u) ^ d u) ⊆ ↑(Finite.toFinset hd)
this : u₀ ∈ Finite.toFinset hd
x : 𝕜
hx : x ∈ support (update d u₀ 0)
⊢ x ∈ ↑((Finite.toFinset hd).erase u₀)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w x : ℂ
⊢ x ∈ {w}ᶜ → AnalyticAt ℂ (canonicalFactor R w) x

Tactic:
hx

Goal state after:
R : ℝ
w x : ℂ
hx : x ∈ {w}ᶜ
⊢ AnalyticAt ℂ (canonicalFactor R w) x
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ η₀.toFinset
x : ℂ
⊢ x ∈ ball 0 R → meromorphicOrderAt (canonicalFactor R z ^ (divisor f (ball 0 R)) z) x ≠ ⊤

Tactic:
hx

Goal state after:
case h₂f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
η₀ : (-divisor f (ball 0 R)).support.Finite
z : ℂ
hz : z ∈ η₀.toFinset
x : ℂ
hx : x ∈ ball 0 R
⊢ meromorphicOrderAt (canonicalFactor R z ^ (divisor f (ball 0 R)) z) x ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : 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] 1 • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : ¬D.support.Finite
x : 𝕜
⊢ f x = (1 • g) x → log ‖f x‖ = (0 + fun x ↦ log ‖g x‖) x

Tactic:
hx

Goal state after:
𝕜 : 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] 1 • g
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : ¬D.support.Finite
x : 𝕜
hx : f x = (1 • g) x
⊢ log ‖f x‖ = (0 + fun x ↦ log ‖g x‖) x
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : 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
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
⊢ log ‖((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z‖ = ((∑ᶠ (u : 𝕜), fun x ↦ ↑(D u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) z

Tactic:
finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _
      (by simp_all [FactorizedRational.mulSupport]),

Goal state after:
𝕜 : 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
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
⊢ log ‖((∏ i ∈ h₃f.toFinset, (fun x ↦ x - i) ^ D i) • g) z‖ =
    ((∑ᶠ (u : 𝕜), fun x ↦ ↑(D u) * log ‖x - u‖) + fun x ↦ log ‖g x‖) z
Module: Mathlib.Analysis.Meromorphic.FactorizedRational

Goal state before:
pp: 𝕜 : 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
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
x : 𝕜
⊢ x ∈ h₃f.toFinset → ‖z - x‖ ^ D x ≠ 0

Tactic:
hx

Goal state after:
𝕜 : 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
t₁ : (support fun u x ↦ ↑(D u) * log ‖x - u‖) = D.support
h₃f : D.support.Finite
z : 𝕜
hz : f z = ((∏ᶠ (u : 𝕜), (fun x ↦ x - u) ^ D u) • g) z
h₂z : D z = 0
h₃z : z ∈ U
x : 𝕜
hx : x ∈ h₃f.toFinset
⊢ ‖z - x‖ ^ D x ≠ 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₁ f₂ : 𝕜 → E
x : 𝕜
hf₁ : MeromorphicAt f₁ x
hf₂ : MeromorphicAt f₂ x
h✝ : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

pp: case inr
𝕜 : 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
h✝ : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

Tactic:
· simpa [h.le] using meromorphicOrderAt_add_eq_left_of_lt hf₂ h

Goal state after:
case inr
𝕜 : 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
h✝ : meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x
h : meromorphicOrderAt f₂ x < meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)