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

Goal state before:
pp: 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 : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport ⇑(f c)
⊢ x ∉ support ⇑(f c)

Tactic:
contrapose Hx

Goal state after:
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 : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ support ⇑(f c)
⊢ x ∈ tsupport ⇑(f c)
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: 𝕜 : 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}
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
let ⟨r, hr⟩ := exists_one_lt_norm 𝕜

Goal state after:
𝕜 : 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‖
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
⊢ Ici (f a) ⊆ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
⊢ b ∈ Ici (f a) → b ∈ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
⊢ Ioi (f a) ⊆ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
⊢ b ∈ Ioi (f a) → b ∈ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
⊢ y ∈ tangentConeAt 𝕜 s x →
    ∃ c d,
      Tendsto (fun x ↦ ‖c x‖) atTop atTop ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)

Tactic:
rw [mem_tangentConeAt_iff_exists_seq]

Goal state after:
case mp.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x y : E
hy₀ : y ≠ 0
⊢ (∃ c d, Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)) →
    ∃ c d,
      Tendsto (fun x ↦ ‖c x‖) atTop atTop ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) atTop (𝓝 y)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ 1 - ‖z‖ = ‖1‖ - ‖z‖

Tactic:
norm_one

Goal state after:
M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ 1 - ‖z‖ = 1 - ‖z‖
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Tactic:
refine tendsto_map' <| tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within ofReal
    (tendsto_nhdsWithin_of_tendsto_nhds <| ofRealCLM.continuous.tendsto' 1 1 rfl) ?_

Goal state after:
M : ℝ
hM : 1 < M
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, ↑x ∈ stolzSet M
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ uIoo x₀ x ⊆ [[x₀, x]]

Tactic:
grind [uIoo, uIcc]

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

Goal state before:
pp: case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - √(z.re ^ 2 + z.im ^ 2))
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M

Tactic:
← norm_eq_sqrt_sq_add_sq

Goal state after:
case h.h.h.h
s : ℝ
hs : 0 < s
M ε : ℝ
hM : 0 < M
hε : 0 < ε
z : ℂ
hzl : (1 - z).re < ε
hzr : |z.im| < s * (1 - z).re
H : ‖1 - z‖ < M * (1 - ‖z‖)
h : z.im ^ 2 = (1 - z).im ^ 2
⊢ z ∈ stolzSet M
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x ↦ x ^ m

Tactic:
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
  · exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx
  intro x hx
  rw [mem_Ioi] at hx
  rw [iter_deriv_zpow]
  refine mul_pos ?_ (zpow_pos hx _)
  norm_cast
  refine int_prod_range_pos (by decide) fun hm => ?_
  rw [← Finset.coe_Ico] at hm
  norm_cast at hm
  fin_cases hm <;> simp_all

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

Goal state before:
pp: θ : ℂ
⊢ sin θ = 0 ↔ ∃ k, θ = ↑k * ↑π

Tactic:
rw [← Complex.cos_sub_pi_div_two, cos_eq_zero_iff]

Goal state after:
θ : ℂ
⊢ (∃ k, θ - ↑π / 2 = (2 * ↑k + 1) * ↑π / 2) ↔ ∃ k, θ = ↑k * ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case refine_1
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ↔ y = 2 * ↑k * ↑π + x

Tactic:
refine Eq.congr rfl ?_

Goal state after:
case refine_1
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 = 2 * ↑k * ↑π + x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case refine_2
x y : ℂ
k : ℤ
⊢ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 ↔ y = (2 * ↑k + 1) * ↑π - x

Tactic:
refine Eq.congr rfl ?_

Goal state after:
case refine_2
x y : ℂ
k : ℤ
⊢ 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2 = (2 * ↑k + 1) * ↑π - x
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
suffices ‖(f ∘ e) (1 : ℂ)‖ = ‖(f ∘ e) (0 : ℂ)‖ by simpa [e]

Goal state after:
case inr
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
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✝¹ : StrictConvexSpace ℝ F
inst✝ : ProperSpace E
f : E → F
r b : ℝ
h_an : DifferentiableOn ℂ f (ball 0 b)
hr_nn : 0 ≤ r
hr_lt : r < b
hr : ∀ z ∈ ball 0 b, ∃ w ∈ closedBall 0 r, ‖f z‖ ≤ ‖f w‖
x : E
hx_mem : x ∈ closedBall 0 r
hx_max : IsMaxOn (fun x ↦ ‖f x‖) (closedBall 0 r) x
z : E
hz : z ∈ ball 0 b
w : E
hw : w ∈ closedBall 0 r
hw' : ‖f z‖ ≤ ‖f w‖
⊢ z ∈ {x_1 | (fun x_2 ↦ (norm ∘ f) x_2 ≤ (norm ∘ f) x) x_1}

Tactic:
exact hw'.trans (hx_max hw)

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

Goal state before:
pp: x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
by
  have := tan_add (x := x) (y := -y) <| by
    rcases h with ⟨x_ne, minus_y_ne⟩ | ⟨x_eq, minus_y_eq⟩
    · refine .inl ⟨x_ne, fun l => ?_⟩
      rw [Ne, neg_eq_iff_eq_neg]
      convert! minus_y_ne (-l - 1) using 2
      push_cast
      ring
    · refine .inr ⟨x_eq, ?_⟩
      rcases minus_y_eq with ⟨l, rfl⟩
      use -l - 1
      push_cast
      ring
  rw [tan_neg] at this
  convert! this using 2
  ring

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ deriv (deriv f) x = f'' x

Tactic:
rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ HasDerivWithinAt (deriv f) (f'' y) (interior D) y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
⊢ deriv (deriv f) x = f'' x

Tactic:
rw [deriv_eqOn isOpen_interior (fun y hy ↦ ?_) hx]

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ HasDerivWithinAt (deriv f) (f'' y) (interior D) y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inr
x y : ℝ
h : x < 1 / y
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
← inv_eq_one_div

Goal state after:
case inr
x y : ℝ
h : x < y⁻¹
hy : 0 < y
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = 0

Tactic:
by
  rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  simp [hx, hy, arg_div_coe_angle, sub_eq_zero]

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : (f u - f x) / (u - x) < (f y - f x) / (y - x)
⊢ f' < slope f x y

Tactic:
simp only [← slope_def_field] at this

Goal state after:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConvexOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
u : ℝ
hxu : x < u
huy : u < y
hu : u ∈ S
this : slope f x u < slope f x y
⊢ f' < slope f x y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ StrictMonoOn (deriv f) S

Tactic:
intro x hx y hy hxy
  exact (hfc.deriv_lt_slope hx hy hxy (hfd x hx)).trans (hfc.slope_lt_deriv hx hy hxy (hfd y hy))

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
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π

Tactic:
sin_eq_zero_iff_cos_eq,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = 1 ∨ cos (angle x y) = -1 ↔ angle x y = 0 ∨ angle x y = π
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
n : ℕ
⊢ ↑z ^ n ∈ Submonoid.unitClosedBall ℂ

Tactic:
simp [pow_le_one₀ (norm_nonneg _) z.norm_le_one]

Goal state after:
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
⊢ (divisor f V).support ⊆ (divisor f U).support

Tactic:
intro b

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 : 𝕜
⊢ b ∈ (divisor f V).support → b ∈ (divisor f U).support
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case right
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
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
hf : MeromorphicAt f x
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact eventually_nhdsWithin_of_eventually_nhds h₃g

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
⊢ ((divisor (f₁ + f₂) U) z)⁻ ≤ max ((divisor f₁ U) z)⁻ ((divisor f₂ U) z)⁻

Tactic:
simp [divisor_apply (hf₁.add hf₂) hz, hf₁₂, negPart_nonneg]

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

Goal state before:
pp: case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left✝ : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right✝ : f x = 0
⊢ AnalyticAt 𝕜 f x

Tactic:
by_contra h'

Goal state after:
case mp.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left✝ : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right✝ : f x = 0
h' : ¬AnalyticAt 𝕜 f x
⊢ False
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr
𝕜 : 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
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g

Tactic:
· exact (Filter.EventuallyEq.filter_mono · nhdsWithin_le_nhds)

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) x
⊢ MeromorphicNFAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)

Tactic:
show x = (x + c) - c by ring

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
h : MeromorphicNFAt (f ∘ fun x ↦ x + c) (x + c - c)
⊢ MeromorphicNFAt ((f ∘ fun x ↦ x + c) ∘ fun z ↦ z - c) (x + c)
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
⊢ AnalyticAt 𝕜 (toMeromorphicNFAt f x) x

Tactic:
analyticAt_congr this

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 𝕜 0 x
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 : 𝕜
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
h₃f : ¬n = 0
⊢ 0 = 0 ^ n • g x

Tactic:
· simp [h₃f, zero_zpow]

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

Goal state before:
pp: case right
𝕜 : 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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
exact eventually_nhdsWithin_of_eventually_nhds h₃g

Goal state after:
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 : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
⊢ Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop

Tactic:
simp only [norm_smul]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : meromorphicOrderAt f x < 0
hf : MeromorphicAt f x
m : ℤ
hm : ↑m = meromorphicOrderAt f x
m_neg : m < 0
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • g z
⊢ Tendsto (fun z ↦ ‖(z - x) ^ m‖ * ‖g z‖) (𝓝[≠] x) atTop
Module: Mathlib.Analysis.Meromorphic.NormalForm

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

Tactic:
add_singleton,

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
h : MeromorphicNFOn (f ∘ fun x ↦ x + c) U
y : 𝕜
hy : y ∈ (fun x ↦ x + c) '' U
⊢ MeromorphicNFAt f y
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
n : ℤ
h'o : meromorphicOrderAt f x = ↑n
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)

Tactic:
lift n to ℕ using by simpa [h'o] using ho.le

Goal state after:
case coe
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
ho : 0 < meromorphicOrderAt f x
hf : MeromorphicAt f x
g : 𝕜 → E
g_an : AnalyticAt 𝕜 g x
gx : g x ≠ 0
n : ℕ
h'o : meromorphicOrderAt f x = ↑↑n
hg : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ ↑n • g z
⊢ Tendsto f (𝓝[≠] x) (𝓝 0)
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
rcases eq_or_ne (meromorphicOrderAt f x) 0 with ho | ho
  · simp [ho, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho]
  simp only [ne_eq, ho, iff_false, not_exists, not_and]
  intro c c_ne hc
  rcases ho.lt_or_gt with ho | ho
  · apply not_tendsto_atTop_of_tendsto_nhds hc.norm
    rw [tendsto_norm_atTop_iff_cobounded]
    exact tendsto_cobounded_of_meromorphicOrderAt_neg ho
  · apply c_ne
    exact tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)

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

Goal state before:
pp: R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ ‖(starRingEnd ℂ) w * z‖ < ‖↑R ^ 2‖

Tactic:
suffices ‖w‖ * ‖z‖ < R * R by simpa [sq]

Goal state after:
R : ℝ
w z : ℂ
h₂z : z ≠ w
hR : 0 < R
hzw : z - w ≠ 0
hw : ‖w‖ < R
h₁z : ‖z‖ ≤ R
⊢ ‖w‖ * ‖z‖ < R * R
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
by_cases h₁ : ¬MeromorphicAt f x
  · aesop
  rw [not_not] at h₁
  by_cases h₂ : meromorphicOrderAt f x = ⊤
  · rw [h₂, eq_comm]
    simp_all [meromorphicOrderAt_eq_top_iff]
  lift meromorphicOrderAt f x to ℤ using h₂ with n hn
  rw [eq_comm, meromorphicOrderAt_eq_int_iff (by fun_prop)] at *
  obtain ⟨g, hg⟩ := hn
  use -g
  simp_all

Goal state after:
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case neg
E : Type u_1
X : Type u_2
A : Type u_3
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace A
inst✝¹ : PathConnectedSpace A
inst✝ : LocallyPathConnectedSpace A
f : C(A, X)
a₀ : A
e₀ : E
Γ : (γ : C(↑I, A)) → γ 0 = a₀ → C(↑I, E)
Γ_0 : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), (Γ γ a) 0 = e₀
F : A → E := fun a ↦ (Γ (somePath a₀ a).toContinuousMap ⋯) 1
a : A
p : OpenPartialHomeomorph E X
hep : F a ∈ p.source
homeo : IsLocalHomeomorph ↑p
he : ↑p e₀ = f a₀
uniq :
  ∀ (γ γ' : C(↑I, A)) (Γ Γ' : C(↑I, E)),
    γ 0 = a₀ →
      γ' 0 = a₀ → Γ 0 = e₀ → Γ' 0 = e₀ → ↑p ∘ ⇑Γ = ⇑(f.comp γ) → ↑p ∘ ⇑Γ' = ⇑(f.comp γ') → γ 1 = γ' 1 → Γ 1 = Γ' 1
Γ_lifts : ∀ (γ : C(↑I, A)) (a : γ 0 = a₀), ↑p ∘ ⇑(Γ γ a) = ⇑(f.comp γ)
this : ∀ (a : A), ↑p (F a) = f a
hfap : f a ∈ p.target
U : Set A
haU : U ∈ 𝓝 a
U_conn : IsPathConnected U
hUp : id U ⊆ ⇑f ⁻¹' p.target
x : A
hxU : x ∈ U
γ : Path a x
hγ : ∀ (t : ↑I), γ t ∈ U
Γ' : Path e₀ ((↑p.symm ∘ ⇑f) a) :=
  { toContinuousMap := Γ (somePath a₀ a).toContinuousMap ⋯, source' := ⋯, target' := ⋯ }
x✝ : ↑I
h✝ : ¬↑x✝ ≤ 1 / 2
⊢ ↑p ((γ.map' ⋯) ⟨2 * ↑x✝ - 1, ⋯⟩) = f (γ ⟨2 * ↑x✝ - 1, ⋯⟩)

Tactic:
simp [Path.map', p.right_inv (hUp (hγ _))]

Goal state after: