mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hk :
  ContDiffOn ℝ (↑k) f s →
    DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y →
      HasDerivWithinAt (fun t ↦ taylorWithinEval f k s t x)
        (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt (fun t ↦ taylorWithinEval f (k + 0).succ s t x)
    (((↑(k + 0).succ !)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y

Tactic:
taylorWithinEval_succ

Goal state after:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
k : ℕ
hk :
  ContDiffOn ℝ (↑k) f s →
    DifferentiableWithinAt ℝ (iteratedDerivWithin k f s) s y →
      HasDerivWithinAt (fun t ↦ taylorWithinEval f k s t x)
        (((↑k !)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y) s' y
hf : ContDiffOn ℝ (↑(k + 1)) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ HasDerivWithinAt
    (fun t ↦ taylorWithinEval f k s t x + (((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s t)
    (((↑(k + 0).succ !)⁻¹ * (x - y) ^ (k + 0).succ) • iteratedDerivWithin ((k + 0).succ + 0).succ f s y) s' y
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s : ℝ
⊢ 0 < 2 * √(1 + s ^ 2) + 1

Tactic:
positivity

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

Goal state before:
pp: s : ℝ
⊢ 0 < 1 / (1 + s ^ 2)

Tactic:
positivity

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

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 0 < 1 + s ^ 2

Tactic:
positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
g_finsum_bound : ∀ (s : Finset ↑u), ∑ z ∈ s, g z ≤ r
hu₄ : HasSum g (∑' (b : ↑u), g b)
g_sum_bound : ∑' (x : ↑u), g x ≤ r
⊢ uIcc d b ⊆ uIcc a b

Tactic:
by grind [uIcc_of_le]

Goal state after:
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
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n : ℕ
| (1 - z) * ∑ x ∈ range n, ((l - s n) * z ^ x + (∑ k ∈ range n, f k - ∑ k ∈ range (x + 1), f k) * z ^ x)

Tactic:
enter [2, 2, 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
k :
  Tendsto (fun n ↦ (1 - z) * ∑ j ∈ range n, (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
this :
  Tendsto
    (fun x ↦
      (1 - z) * ∑ i ∈ range x, (l - s x) * z ^ i +
        (1 - z) * ∑ j ∈ range x, (∑ k ∈ range x, f k - ∑ k ∈ range (j + 1), f k) * z ^ j)
    atTop (𝓝 ((1 - z) * 0 + (l - ∑' (i : ℕ), f i * z ^ i)))
n i : ℕ
| (l - s n) * z ^ i + (∑ k ∈ range n, f k - ∑ k ∈ range (i + 1), f k) * z ^ i
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
⊢ ε / 4 / M > 0

Tactic:
positivity

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
⊢ ε / 4 / (F + 1) > 0

Tactic:
positivity

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
hm : ∀ ε > 0, ∃ N, ∀ n ≥ N, ‖∑ i ∈ range n, f i - l‖ < ε
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
p :
  ∀ ε > 0,
    ∃ N, ∀ n ≥ N, ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε
⊢ ε / 2 > 0

Tactic:
positivity

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 0 < x
y : ℝ
x✝ : y ∈ fun a ↦ Ioi 0 a
hxy : x < y
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖1 - z‖ * ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ + ‖1 - z‖ * ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ ≤
    ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i

Tactic:
by
      gcongr <;> simp_rw [← norm_pow, ← norm_mul, norm_sum_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
f : α → β
inst✝ : DecidablePred fun x ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
x : α
x✝ : x ∈ s
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x

Tactic:
by
        split_ifs with hx
        · simp [hx]
        linarith

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖1 - z‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ 0 < F + 1

Tactic:
positivity

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
x✝¹ : ℕ
x✝ : x✝¹ ∉ Ico B₁ (max B₁ B₂)
⊢ 0 ≤ ‖z‖ ^ x✝¹

Tactic:
positivity

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

Goal state before:
pp: 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
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
⊢ 0 ≤ ‖z‖

Tactic:
positivity

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

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)

Tactic:
by
      apply StrictMonoOn.exists_deriv_lt_slope_aux _ hwy _ _
      · refine hf.mono (Icc_subset_Icc hxw.le le_rfl)
      · exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
      · intro z hz
        rw [← hw]
        apply ne_of_gt
        exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1

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

Goal state before:
pp: case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

Tactic:
exact (sin_le_one x).trans_lt h'

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

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) ^ 2 = x ^ 2 / (1 + x ^ 2)

Tactic:
by
  rw [← tan_sq_div_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ x / 2 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ 0 ≤ x / 2

Tactic:
positivity

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

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ 0 ≤ x / π

Tactic:
positivity

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

Goal state before:
pp: case hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = π / 2 - arctan x

Tactic:
by
  rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]
  · simpa using (arctan_lt_pi_div_two x).trans (half_lt_self_iff.mpr pi_pos)
  · rw [sub_lt_self_iff, ← arctan_zero]
    exact tanOrderIso.symm.strictMono h

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * (π / 2)
ub : arctan x < π / 2
⊢ 0 < π / 2

Tactic:
positivity

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * (π / 2) < 1 * (π / 2)
⊢ 0 < π / 2

Tactic:
positivity

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
⊢ 0 ≤ (‖x‖ * ‖y‖) ^ 2

Tactic:
positivity

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

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 0 ≤ |θ|

Tactic:
positivity

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 0 < π / 2

Tactic:
positivity

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ 0 ≤ ‖z‖

Tactic:
positivity

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

Goal state before:
pp: M : ℝ
z : ℂ
x✝¹ : 0 < M
x✝ : z.re ≤ M
⊢ 0 ≤ ‖2 * ↑M - z‖

Tactic:
positivity

Goal state after:
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}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
x : ℂ
hx : x ∈ ball 0 R
⊢ 0 ≤ ‖2 * ↑M - f x‖

Tactic:
positivity

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

Goal state before:
pp: case funProp.discharger
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this✝ :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
this : ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
⊢ R₁ ≠ 0

Tactic:
positivity

Goal state after:
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
⊢ 0 < M + ‖f 0‖

Tactic:
positivity

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
⊢ 0 < ‖x‖⁻¹

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
⊢ IsCoveringMapOn (fun x ↦ x ^ n) {0}ᶜ

Tactic:
by
  convert! (X ^ n).isCoveringMapOn_eval.mono fun x' h ↦ _ with x
  · simp
  · assumption
  · simpa [derivative_X_pow, hn, show n ≠ 0 by aesop] using fun _ ↦ Ne.symm h

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ ↑n
⊢ Function.Surjective fun x ↦ x ^ n

Tactic:
simpa using surj

Goal state after:
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
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
heq : f z = f c
⊢ 0 ≤ R₂ * (dist z c / R₁) ^ (n + 1)

Tactic:
positivity

Goal state after:
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₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
⊢ 0 ≤ R₂ / R₁

Tactic:
positivity

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

Goal state before:
pp: E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this :
  ∀ (n : ℕ),
    ∃ N,
      a ∈ N ∧
        IsOpen[inst✝] N ∧
          ∃ g',
            ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
              p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 (t n_max) ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n_max, g' (t', a) = g (t', a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ g',
      ContinuousOn g' (Set.univ ×ˢ N) ∧
        p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : ↑I), g' (t, a) = g (t, a)

Tactic:
simp_rw [h_max _ le_rfl] at hN

Goal state after:
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
this :
  ∀ (n : ℕ),
    ∃ N,
      a ∈ N ∧
        IsOpen[inst✝] N ∧
          ∃ g',
            ContinuousOn g' (Set.Icc 0 (t n) ×ˢ N) ∧
              p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ t n, g' (t', a) = g (t', a)
N : Set A
haN : a ∈ N
N_open : IsOpen[inst✝] N
hN :
  ∃ g',
    ContinuousOn g' (Set.Icc 0 1 ×ˢ N) ∧
      p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ t' ≤ 1, g' (t', a) = g (t', a)
⊢ ∃ N ∈ 𝓝 a,
    ∃ g',
      ContinuousOn g' (Set.univ ×ˢ N) ∧
        p ∘ g' = ⇑f ∧ (∀ (a : A), g' (0, a) = g (0, a)) ∧ ∀ (t : ↑I), g' (t, a) = g (t, a)
Module: Mathlib.Analysis.Meromorphic.Divisor

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

Tactic:
simp [hn]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : n = 0
⊢ (divisor (f ^ n) U) z = (n • divisor f U) z

Tactic:
simp [hn]

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

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
⊢ meromorphicOrderAt f x = 0

Tactic:
have : n = 0 := by
        by_contra hContra
        have := h₃g.eq_of_nhds
        simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
        tauto

Goal state after:
case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
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
this : n = 0
⊢ meromorphicOrderAt f 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 : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
⊢ f =ᶠ[𝓝 x] g

Tactic:
have Z := (hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq cs.symm)).continuousAt

Goal state after:
case pos
𝕜 : 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₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
Z : ContinuousAt f x
⊢ f =ᶠ[𝓝 x] g
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
z₀ x : 𝕜
hx : x ≠ z₀
hu : x ∈ U
⊢ meromorphicOrderAt (fun x ↦ x - z₀) x = ↑0

Tactic:
exact (meromorphicOrderAt_eq_int_iff (by fun_prop)).mpr
      ⟨(· - z₀), analyticAt_id.fun_sub analyticAt_const, by simp [sub_ne_zero_of_ne hx]⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicNFAt (f i) x
h₂f : {σ | σ ∈ s ∧ f σ x = 0}.Subsingleton
⊢ MeromorphicNFAt (∏ i ∈ s, f i) x

Tactic:
by
  classical
  have h₃f {τ : ι} (h₁τ : τ ∈ s) (h₂τ : τ ∉ {σ ∈ s | f σ x = 0}) :
      AnalyticAt 𝕜 (f τ) x := by
    rw [← (h₁f τ h₁τ).meromorphicOrderAt_nonneg_iff_analyticAt]
    apply ((h₁f τ h₁τ).meromorphicOrderAt_eq_zero_iff.2 _).symm.le
    grind
  by_cases h₄f : {σ ∈ s | f σ x = 0} = ∅
  · exact (Finset.analyticAt_prod _ (fun σ hσ ↦ h₃f hσ (by aesop))).meromorphicNFAt
  rw [Finset.filter_eq_empty_iff] at h₄f
  push Not at h₄f
  obtain ⟨τ, h₁τ, h₂τ⟩ := h₄f
  have {μ : ι} (hμ : μ ∈ s.erase τ) : f μ x ≠ 0 := by
    by_contra
    have : τ = μ := h₂f (by aesop) (by aesop)
    aesop
  rw [← Finset.mul_prod_erase _ _ h₁τ, meromorphicNFAt_mul_iff_left]
  · apply h₁f τ h₁τ
  · apply Finset.analyticAt_prod _ (fun μ hμ ↦ h₃f (Finset.mem_of_mem_erase hμ) (by aesop))
  · rw [Finset.prod_apply, Finset.prod_ne_zero_iff]
    aesop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
x y : 𝕜
h : x = y
⊢ 1 ≠ 0

Tactic:
apply one_ne_zero

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 : 𝕜
hf : MeromorphicAt f x
m : ℕ
hm : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
h : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hfz : f z = 0
⊢ (z - x) ^ Exists.choose hf • f z = 0

Tactic:
rw [hfz, smul_zero]

Goal state after:
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₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x

Tactic:
rw [sub_eq_add_neg, hf₁.meromorphicTrailingCoeffAt_add_eq_add (by fun_prop)]
  · rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg]
  · rwa [← meromorphicOrderAt_neg]
  · rwa [meromorphicTrailingCoeffAt_neg, ← sub_eq_add_neg]

Goal state after: