mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ∈ Ioo a b
⊢ Tendsto (fun n ↦ G (↑n)⁻¹ x) atTop (𝓝 (deriv f x))

Tactic:
hfg hx₂

Goal state after:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ∈ Ioo a b
⊢ Tendsto (fun n ↦ G (↑n)⁻¹ x) atTop (𝓝 (deriv g x))
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
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
hv : ∀ t ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t
⊢ (((↑(n + 1)!)⁻¹ • (iteratedFDeriv ℝ (n + 1) f x) fun x ↦ y) +
      (↑(n + 1)!)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ (n + 1) • (iteratedFDeriv ℝ (n + 1 + 1) f (x + t • y)) fun x ↦ y) =
    (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y

Tactic:
have hv' : ContinuousOn (v (n + 1 + 1)) (Set.uIcc 0 1) := by
      intro t ht
      have h_cont : ContinuousAt (iteratedFDeriv ℝ (n + 1 + 1) f) (x + t • y) :=
        ((hf t ht).iteratedFDeriv_right (i := n + 1 + 1) (m := 0) (by simp)).continuousAt
      exact (h_cont.comp (x := t) (by fun_prop)).continuousWithinAt.eval_const _

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
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
hv : ∀ t ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t
hv' : ContinuousOn (v (n + 1 + 1)) (Set.uIcc 0 1)
⊢ (((↑(n + 1)!)⁻¹ • (iteratedFDeriv ℝ (n + 1) f x) fun x ↦ y) +
      (↑(n + 1)!)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ (n + 1) • (iteratedFDeriv ℝ (n + 1 + 1) f (x + t • y)) fun x ↦ y) =
    (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
have g_ae_deriv_zero : ∀ᵐ x, x ∈ uIcc a b → HasDerivAt g 0 x := by
    filter_upwards [hf.ae_differentiableAt, hf.intervalIntegrable_deriv.ae_hasDerivAt_integral]
      with x hx₁ hx₂ hx₃
    convert! (hx₁ hx₃).hasDerivAt.sub (hx₂ hx₃ a (by simp))
    abel

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
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
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:
rw [norm_mul, norm_mul]

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

Goal state before:
pp: case inl
x y : ℂ
h1 : ∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2
h2 : ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑π / 2
⊢ (sin x * cos y / (cos x * cos y) + cos x * sin y / (cos x * cos y)) /
      (cos x * cos y / (cos x * cos y) - sin x * sin y / (cos x * cos y)) =
    (tan x + tan y) / (1 - tan x * tan y)

Tactic:
simp only [← div_mul_div_comm, tan, mul_one, one_mul, div_self (cos_ne_zero_iff.mpr h1),
      div_self (cos_ne_zero_iff.mpr h2)]

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

Goal state before:
pp: case neg
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 : ℝ
hb : deriv f b < (f y - f w) / (y - w)
hwb : w < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

Tactic:
refine ⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩

Goal state after:
case neg
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 : ℝ
hb : deriv f b < (f y - f w) / (y - w)
hwb : w < b
hby : b < y
⊢ deriv f a < (f y - f x) / (y - x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ ∑ i ∈ Finset.range n, 2 * sin (a / 2) * cos (a * ↑i + b) =
    ∑ x ∈ Finset.range n, (sin (a * (↑(x + 1) - 1 / 2) + b) - sin (a * (↑x - 1 / 2) + b))

Tactic:
congr! 1 with x hx
      rw [sin_sub_sin]
      push_cast
      ring_nf

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

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

Tactic:
rw [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

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

Goal state before:
pp: x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun y ↦ tan y - y) (1 / cos x ^ 2 - 1) x

Tactic:
by simpa using! (hasDerivAt_tan h).add (hasDerivAt_id x).neg

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

Goal state before:
pp: a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (a * x) (a * y) = angle x y

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0 <;> obtain rfl | hy := eq_or_ne y 0 <;>
    simp [angle_eq_abs_arg, mul_div_mul_left, *]

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 : V
⊢ arccos (⟪x, 0⟫ / (‖x‖ * ‖0‖)) = π / 2

Tactic:
inner_zero_right,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (0 / (‖x‖ * ‖0‖)) = π / 2
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 (r • x) y = angle (-x) y

Tactic:
rw [angle_comm, angle_smul_right_of_neg y x hr, angle_comm]

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
⊢ sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)

Tactic:
← sin_angle_mul_norm_mul_norm

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ sin (angle x y) = sin (angle 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
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π

Tactic:
rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_angle_eq_pi]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
n : ℕ
⊢ divisor (OfNat.ofNat n) U = 0

Tactic:
convert! divisor_const (n : 𝕜)
  simp [Semiring.toGrindSemiring_ofNat 𝕜 n]

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 : 𝕜
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
⊢ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0

Tactic:
have hf : MeromorphicAt f x := by
        apply MeromorphicAt.congr _ (h₃g.filter_mono nhdsWithin_le_nhds).symm
        fun_prop
      have : meromorphicOrderAt f x = n := by
        rw [meromorphicOrderAt_eq_int_iff hf]
        use g, h₁g, h₂g
        exact eventually_nhdsWithin_of_eventually_nhds h₃g
      by_cases! hn : 0 ≤ n
      · left
        rw [analyticAt_congr h₃g]
        apply (AnalyticAt.zpow_nonneg (by fun_prop) hn).smul h₁g
      · right
        use hf
        simp [this, WithTop.coe_lt_zero.2 hn, h₃g.eq_of_nhds,
          zero_zpow n hn.ne]

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

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

Tactic:
rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
⊢ f x = g x
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 : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
n : ℤ
h : 𝕜 → E
h₁h : AnalyticAt 𝕜 h x
h₂h : h x ≠ 0
h₃h : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • h
⊢ MeromorphicNFAt g x

Tactic:
exact .inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g) y
⊢ f⁻¹ y = ((fun x_1 ↦ x_1 - x) ^ (-n) • g⁻¹) y

Tactic:
simp only [Pi.inv_apply, hy, Pi.smul_apply', Pi.pow_apply, smul_eq_mul, mul_inv_rev, zpow_neg]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
f : 𝕜 → 𝕜
n : ℤ
g : 𝕜 → 𝕜
h₁ : AnalyticAt 𝕜 g x
h₂ : g x ≠ 0
h₃ : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
y : 𝕜
hy : f y = ((fun x_1 ↦ x_1 - x) ^ n • g) y
⊢ (g y)⁻¹ * ((y - x) ^ n)⁻¹ = ((y - x) ^ n)⁻¹ * (g y)⁻¹
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
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
⊢ MeromorphicNFAt (f ∘ g) x

Tactic:
by_cases hord : analyticOrderAt (g · - g x) x = ⊤

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicNFAt (f ∘ g) x

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
x : 𝕜
hg : AnalyticAt 𝕜 g x
n : ℤ
q : 𝕜 → E
hq_an : AnalyticAt 𝕜 q (g x)
hq_ne : q (g x) ≠ 0
hf : f =ᶠ[𝓝 (g x)] (fun x_1 ↦ x_1 - g x) ^ n • q
hord : ¬analyticOrderAt (fun x_1 ↦ g x_1 - g x) x = ⊤
⊢ MeromorphicNFAt (f ∘ g) x
Module: Mathlib.Analysis.Meromorphic.Order

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

Tactic:
obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := hf.choose_spec.analyticOrderAt_eq_natCast.mp h.symm

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
n : ℤ
hf : MeromorphicAt f x
h✝ : ¬analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x = ⊤
m : ℕ
h : ↑m = analyticOrderAt (fun z ↦ (z - x) ^ Exists.choose hf • f z) x
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ Exists.choose hf • f z = (z - x) ^ m • g z
⊢ ↑m - ↑(Exists.choose ⋯) = n ↔ ∃ g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖canonicalFactor R w z‖ = 1

Tactic:
canonicalFactor,

Goal state after:
R : ℝ
w z : ℂ
hw : w ∈ ball 0 R
hz : z ∈ sphere 0 R
hR : 0 < R
hzw : z - w ≠ 0
⊢ ‖(↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))‖ = 1
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
⊢ ∃ u, meromorphicOrderAt (canonicalFactor R w) u ≠ ⊤

Tactic:
use 0

Goal state after:
case h
z : ℂ
R : ℝ
w : ℂ
hR : 0 < R
⊢ meromorphicOrderAt (canonicalFactor R w) 0 ≠ ⊤
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
⊢ meromorphicOrderAt f⁻¹ x = -meromorphicOrderAt f x

Tactic:
by_cases hf : MeromorphicAt f x; swap
  · have : ¬ MeromorphicAt (f⁻¹) x := by
      contrapose hf
      simpa using hf.inv
    simp [hf, this]
  by_cases h₂f : meromorphicOrderAt f x = ⊤
  · rw [h₂f, ← LinearOrderedAddCommGroupWithTop.neg_top, neg_neg]
    rw [meromorphicOrderAt_eq_top_iff] at *
    filter_upwards [h₂f]
    simp
  lift meromorphicOrderAt f x to ℤ using h₂f with a ha
  apply (meromorphicOrderAt_eq_int_iff hf.inv).2
  obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 ha.symm
  use g⁻¹, h₁g.inv h₂g, inv_eq_zero.not.2 h₂g
  rw [eventually_nhdsWithin_iff] at *
  filter_upwards [h₃g]
  intro _ h₁a h₂a
  simp [h₁a h₂a, Algebra.smul_def, mul_comm]

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

Goal state before:
pp: f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).re * (f z).re + (f z).im * (f z).im = normSq z
⊢ (f z).im = z.im ∨ (f z).im = -z.im

Tactic:
normSq_apply z,

Goal state after:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (f z).re = z.re
z : ℂ
h₁ : (f z).re * (f z).re + (f z).im * (f z).im = z.re * z.re + z.im * z.im
⊢ (f z).im = z.im ∨ (f z).im = -z.im
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toContinuousLinearMap) ∘SL ↑conjCLE

Tactic:
obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li :=
    ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩

Goal state after:
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL ↑conjCLE
Module: Mathlib.Analysis.Complex.Conformal

Goal state before:
pp: case h₁
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z

Tactic:
differentiableAt_iff_restrictScalars ℝ h_diff

Goal state after:
case h₁
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ ∃ g', restrictScalars ℝ g' = fderiv ℝ f z
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
⊢ f =ᶠ[codiscreteWithin (closedBall 0 R)]
    ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
        ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
      h

Tactic:
filter_upwards [D.eventuallyEq, h₃h] with a h₁a h₂a

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
f : ℂ → E
h₁f : MeromorphicOn f (closedBall 0 R)
h₂f : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt f ↑u ≠ ⊤
hR : 0 < R
g : ℂ → E
D : CanonicalDecomp f g R
h₄g : ∀ (u : ↑(closedBall 0 R)), meromorphicOrderAt g ↑u ≠ ⊤
h : ℂ → E
h₁h : AnalyticOnNhd ℂ h (closedBall 0 R)
h₂h : ∀ (u : ↑(closedBall 0 R)), h ↑u ≠ 0
h₃h : g =ᶠ[codiscreteWithin (closedBall 0 R)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h
a : ℂ
h₁a : f a = ((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) • g) a
h₂a : g a = ((∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor g (closedBall 0 R)) u) • h) a
⊢ f a =
    (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f (ball 0 R)) u)) *
          ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f (sphere 0 R)) v) •
        h)
      a
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ h w =
    ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f (ball 0 R)) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f (sphere 0 R)) i) •
      meromorphicTrailingCoeffAt f w

Tactic:
rw [Eq.comm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f (ball 0 R)) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f (sphere 0 R)) i) •
      meromorphicTrailingCoeffAt f w =
    h w
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ ↑3 - 1 < rexp 1

Tactic:
exact_mod_cast exp_one_gt_two

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

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
a : A
⊢ Continuous[_, inst✝²] fun x ↦ (cov.liftHomotopy H f H_0) (x, a)

Tactic:
simp_rw [liftHomotopy_apply]

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
cov : IsCoveringMap p
H : C(↑I × A, X)
f : C(A, E)
H_0 : ∀ (a : A), H (0, a) = p (f a)
a : A
⊢ Continuous[_, inst✝²] fun x ↦
    (cov.liftPath (H.comp ((ContinuousMap.id ↑I).prodMk (ContinuousMap.const (↑I) a))) (f a) ⋯) x
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: t : |4 / 5| = 4 / 5
z : |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / (↑i + 1) + log (1 - 4 / 5)| ≤ (4 / 5) ^ (130 + 1) / (1 - 4 / 5)
⊢ |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)

Tactic:
show (1 - (4 : ℝ) / 5) = (1 / 5 : ℝ) by norm_num,

Goal state after:
t : |4 / 5| = 4 / 5
z : |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / (↑i + 1) + log (1 / 5)| ≤ (4 / 5) ^ (130 + 1) / (1 / 5)
⊢ |log 5 - 160943791243 / 100000000000| ≤ (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹)
Module: Mathlib.Analysis.Meromorphic.Order

Goal state before:

Tactic:
deriv f z = deriv (fun z ↦ (z - x) ^ n • g z) z :=
      hz
    _ = (z - x) ^ n • deriv g z + deriv ((· ^ n) ∘ (· - x)) z • g z :=
      deriv_fun_smul (by fun_prop (disch := grind)) hgz.differentiableAt
    _ = (z - x) ^ n • deriv g z + (n * (z - x) ^ (n - 1)) • g z := by
      rw [deriv_comp _ (by fun_prop (disch := grind)) (by fun_prop)]
      simp [deriv_zpow]
    _ = (z - x) ^ (n - 1) • ((n : 𝕜) • g z + (z - x) • deriv g z) := by
      simp [smul_smul, ← zpow_add_one₀ hzx, add_comm, mul_comm]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove
    ((fun a ↦ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
      verticalClosedStrip 0 1)

Tactic:
bddAbove_def

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
ε : ℝ
hε : ε > 0
hB : ∃ x, ∀ y ∈ norm ∘ f '' verticalClosedStrip 0 1, y ≤ x
⊢ ∃ x,
    ∀
      y ∈
        (fun a ↦ ‖((↑ε + ↑(sSupNormIm f 0)) ^ (a - 1) * (↑ε + ↑(sSupNormIm f 1)) ^ (-a)) • f a‖) ''
          verticalClosedStrip 0 1,
      y ≤ x