mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ContMDiff I 𝓘(ℝ, ℝ) ↑n fun x ↦ f x / (f x + g x)

Tactic:
exact f_diff.div₀ (f_diff.add g_diff) (fun x ↦ ne_of_gt (A x))

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: case refine_1.hd₀
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)

Tactic:
refine Tendsto.comp ?_ φ_strict.tendsto_atTop

Goal state after:
case refine_1.hd₀
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto d atTop (𝓝 0)
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
⊢ ⋃ i ∈ ∅, Ioc (f i) (f (succ i)) = ∅

Tactic:
biUnion_empty

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
⊢ ∅ = ∅
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x₀ : ℝ
n : ℕ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hf : ContDiffOn ℝ (↑n) f s
⊢ Filter.Tendsto (fun x ↦ ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (𝓝[s] x₀) (𝓝 0)

Tactic:
by
  have h_isLittleO := (taylor_isLittleO hs hx₀s hf).norm_norm
  rw [Asymptotics.isLittleO_iff_tendsto] at h_isLittleO
  · rw [tendsto_zero_iff_norm_tendsto_zero]
    simpa [norm_smul, div_eq_inv_mul] using h_isLittleO
  · simp only [norm_pow, Real.norm_eq_abs, pow_eq_zero_iff', abs_eq_zero, ne_eq, norm_eq_zero,
      and_imp]
    intro x hx
    rw [sub_eq_zero] at hx
    simp [hx]

Goal state after:
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n : ℕ
inst✝ : CompleteSpace F
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
z : E
⊢ z ∈ (fun t ↦ x + t • y) '' Set.uIcc 0 1 → ContinuousWithinAt (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1) z

Tactic:
⟨t, ht, hz⟩

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n : ℕ
inst✝ : CompleteSpace F
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
z : E
t : ℝ
ht : t ∈ Set.uIcc 0 1
hz : (fun t ↦ x + t • y) t = z
⊢ ContinuousWithinAt (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1) z
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))

Tactic:
let s := fun n ↦ ∑ i ∈ range n, f i

Goal state after:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
⊢ Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
    (𝓝 (l - ∑' (n : ℕ), f n * z ^ n))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
have f_deriv_integral_ac :=
    hf.intervalIntegrable_deriv.absolutelyContinuousOnInterval_intervalIntegral
    (c := a) (by simp)

Goal state after:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.eq_def] at h

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
Module: Mathlib.Analysis.Complex.AbelLimit

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

Tactic:
let s := fun n ↦ ∑ i ∈ range n, f i

Goal state after:
case inr
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
⊢ Tendsto (fun z ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℂ
⊢ sin x = 2 * tan (x / 2) / (1 + tan (x / 2) ^ 2)

Tactic:
conv_lhs => rw [← mul_div_cancel₀ x two_ne_zero, sin_two_mul]

Goal state after:
x : ℂ
⊢ 2 * sin (x / 2) * cos (x / 2) = 2 * tan (x / 2) / (1 + tan (x / 2) ^ 2)
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ‖f z‖ ≤ C

Tactic:
closure_eq_self_union_frontier,

Goal state after:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U ∪ frontier U
⊢ ‖f z‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case refine_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x

pp: case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

pp: case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Tactic:
· rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]

Goal state after:
case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
⊢ x ∈ interior S →
    ∀ ⦃b : ℝ⦄, b ∈ interior S → x ≤ b → (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) b

Tactic:
hxs

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
⊢ ∀ ⦃b : ℝ⦄, b ∈ interior S → x ≤ b → (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
⊢ x ∈ interior S →
    ∀ ⦃b : ℝ⦄, b ∈ interior S → x ≤ b → (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) b

Tactic:
hxs

Goal state after:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
⊢ ∀ ⦃b : ℝ⦄, b ∈ interior S → x ≤ b → (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ENNReal.ofReal ‖x‖

Tactic:
exact ENNReal.ofReal_le_ofReal norm_exp_I_mul_ofReal_sub_one_le

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

Goal state before:
pp: x✝ y✝ x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
subst y

Goal state after:
x✝ y x : ℂ
hx : ‖x‖ = 1
hy : ‖1‖ = 1
⊢ ‖x - 1‖ ∈ Icc (2 / π * angle x 1) (angle x 1)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ slope f x y ≤ f'

Tactic:
apply ge_of_tendsto <| (hasDerivWithinAt_iff_tendsto_slope' self_notMem_Iio).mp hf'

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ π - angle x (-r • y) = angle x (-y)

Tactic:
angle_smul_right_of_pos x y (neg_pos_of_neg hr),

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : r < 0
⊢ π - angle x y = angle x (-y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)

Tactic:
norm_sub_pow_two_real

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ ⟪x, y⟫ = -(‖x‖ * ‖y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x + y‖ = ‖x‖ + ‖y‖ ↔ angle x y = 0

Tactic:
by
  refine ⟨?_, norm_add_eq_add_norm_of_angle_eq_zero⟩
  grind [inner_eq_mul_norm_iff_angle_eq_zero hx hy, norm_add_pow_two_real]

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
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖

Tactic:
norm_sub_pow_two_real

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = |‖x‖ - ‖y‖|
h1 : ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x - y‖ ^ 2 ↔ ⟪x, y⟫ = 0

Tactic:
norm_sub_pow_two_real

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x‖ ^ 2 + 2 * ⟪x, y⟫ + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * ⟪x, y⟫ + ‖y‖ ^ 2 ↔ ⟪x, y⟫ = 0
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ MapsTo f (ball 0 R) (closedBall (f 0) R)

Tactic:
h₀

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
R : ℝ
f : E → F
z : E
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (closedBall 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ MapsTo f (ball 0 R) (closedBall 0 R)
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hU : IsCompact U
hV : V ⊆ U
b : 𝕜
hb : ¬(divisor f V) b = 0
⊢ ¬(meromorphicOrderAt f b).untop₀ = 0

Tactic:
divisor_apply (fun x hx ↦ hf x (hV hx))
    ((divisor f V).supportWithinDomain hb)

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hU : IsCompact U
hV : V ⊆ U
b : 𝕜
hb : ¬(meromorphicOrderAt f b).untop₀ = 0
⊢ ¬(meromorphicOrderAt f b).untop₀ = 0
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

Tactic:
by_cases h₁ : meromorphicOrderAt f₁ z = ⊤

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
z : 𝕜
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
h₁z : z ∈ U
h₃ : meromorphicOrderAt (f₁ + f₂) z ≠ ⊤
hz : z ∈ U
h₁ : ¬meromorphicOrderAt f₁ z = ⊤
⊢ min (meromorphicOrderAt f₁ z).untop₀ (meromorphicOrderAt f₂ z).untop₀ ≤ (meromorphicOrderAt (f₁ + f₂) z).untop₀
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : 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
h₁f : MeromorphicAt f x
h₃ : meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f x = g x

pp: case neg
𝕜 : 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
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
· simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
      MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h
    apply EventuallyEq.eq_of_nhds (f := 0)
    rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (by fun_prop)]
    apply (h.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₃)).symm

Goal state after:
case neg
𝕜 : 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
h₁f : MeromorphicAt f x
h₃ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicTrailingCoeffAt 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 : 𝕜
n : ℤ
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ n • g z
⊢ meromorphicTrailingCoeffAt f x = g x

Tactic:
have h₄ : MeromorphicAt f x := by
    rw [MeromorphicAt.meromorphicAt_congr h]
    fun_prop
  have : meromorphicOrderAt f x = n := by
    simp only [meromorphicOrderAt_eq_int_iff h₄, ne_eq]
    use g, h₁g, h₂g
    exact h
  simp_all [meromorphicTrailingCoeffAt_of_eq_nhdsNE h₁g]

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

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
⊢ f ^ n =ᶠ[𝓝 x] 0

Tactic:
filter_upwards [hf] with z hz

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
n : ℤ
x : 𝕜
hn : ¬n = 0
hf : f =ᶠ[𝓝 x] 0
z : 𝕜
hz : f z = 0 z
⊢ (f ^ n) z = 0 z
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicAt f x
h : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose ⋯ • f z) x = ⊤ ↔ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0

Tactic:
simp only [h, eventually_nhdsWithin_iff, mem_compl_iff, mem_singleton_iff, true_iff]

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 : analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, ¬x_1 = x → f x_1 = 0
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicTrailingCoeffAt (fun x ↦ e) x = e

Tactic:
rw [he]

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x e : 𝕜
he : e = 0
⊢ meromorphicTrailingCoeffAt (fun x ↦ 0) x = 0
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 : MeromorphicNFAt f x
z : 𝕜
hz : z = x
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    f x

Tactic:
have h₀f := hf

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    f x
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case pos.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    f x

Tactic:
Filter.EventuallyEq.eq_of_nhds h₃g

Goal state after:
case pos.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x z : 𝕜
hz : z = x
h₀f : MeromorphicNFAt f x
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ (if h : True then Function.update f x (if h_1 : meromorphicOrderAt f x = 0 then Classical.choose ⋯ x else 0) else 0)
      x =
    ((fun x_1 ↦ x_1 - x) ^ n • g) x
Module: Mathlib.Analysis.Meromorphic.TrailingCoefficient

Goal state before:
pp: case neg
𝕜 : 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
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt 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
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : ↑n₁ < ↑n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x

Tactic:
WithTop.coe_lt_coe

Goal state after:
case neg
𝕜 : 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
n₂ : ℤ
hn₂ : ↑n₂ = meromorphicOrderAt 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
n₁ : ℤ
hn₁ : ↑n₁ = meromorphicOrderAt f₁ x
h : n₁ < n₂
g₁ : 𝕜 → E
h₁g₁ : AnalyticAt 𝕜 g₁ x
h₂g₁ : g₁ x ≠ 0
h₃g₁ : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f₁ z = (z - x) ^ n₁ • g₁ z
⊢ meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ 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₂f : ∀ (u : ↑U), meromorphicOrderAt f ↑u ≠ ⊤
u : 𝕜
hu : u ∈ U ∩ f ⁻¹' {0}
⊢ u ∈ Function.support ⇑(MeromorphicOn.divisor f U)

pp: case mpr
𝕜 : 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 : 𝕜
hu : u ∈ Function.support ⇑(MeromorphicOn.divisor f U)
⊢ u ∈ U ∩ f ⁻¹' {0}

Tactic:
· simp_all only [ne_eq, Subtype.forall, Set.mem_inter_iff, Set.mem_preimage,
      Set.mem_singleton_iff, Function.mem_support, h₁f.meromorphicOn, MeromorphicOn.divisor_apply,
      WithTop.untop₀_eq_zero, (h₁f hu.1).meromorphicOrderAt_eq_zero_iff, not_true_eq_false, or_self,
      not_false_eq_true]

Goal state after:
case mpr
𝕜 : 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 : 𝕜
hu : u ∈ Function.support ⇑(MeromorphicOn.divisor f U)
⊢ u ∈ U ∩ f ⁻¹' {0}
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicNFOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicNFAt (f ∘ fun x ↦ x + c) y

Tactic:
rw [meromorphicNFAt_comp_add_const_iff_meromorphicNFAt]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicNFOn f (U + {c})
y : 𝕜
hy : y ∈ U
⊢ MeromorphicNFAt f (y + c)