awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun (z : ℂ) (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun (z : ℂ) (t : ℝ) ↦ ((↑t : ℂ) ^ (z - 1) * (↑(log t) : ℂ)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun (t : ℝ) ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 :
  ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
h6 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y
main :
  @Integrable _ _ _ _ Real.measurableSpace (F' s) (Measure.restrict volume (Ioi 0)) ∧
    HasDerivAt.{0, u_1} (F := E)
      (fun (n : ℂ) ↦ @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ F n a)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ F' s a) s
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s

Tactic:
simpa only [F', mul_smul] using main

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s.re
⊢ DifferentiableAt ℂ (mellin f) s

Tactic:
(mellin_hasDerivAt_of_isBigO_rpow hfc hf_top hs_top hf_bot hs_bot).2.differentiableAt

Premises used: mellin_hasDerivAt_of_isBigO_rpow, HasDerivAt.differentiableAt, And.right
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
ha : 0 < a
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (t : ℝ) ↦ rexp (-a * t)
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s.re
⊢ MellinConvergent f s

Tactic:
mellinConvergent_of_isBigO_rpow hfc (hf_top.trans (isLittleO_exp_neg_mul_rpow_atTop ha _).isBigO)
    (lt_add_one _) hf_bot hs_bot

Premises used: lt_add_one, isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, mellinConvergent_of_isBigO_rpow
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
ha : 0 < a
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (t : ℝ) ↦ rexp (-a * t)
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s.re
⊢ DifferentiableAt ℂ (mellin f) s

Tactic:
mellin_differentiableAt_of_isBigO_rpow hfc
    (hf_top.trans (isLittleO_exp_neg_mul_rpow_atTop ha _).isBigO) (lt_add_one _) hf_bot hs_bot

Premises used: lt_add_one, isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsBigO.trans, Asymptotics.IsLittleO.isBigO, mellin_differentiableAt_of_isBigO_rpow
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
⊢ -1 < (s - 1).re

Tactic:
simpa only [sub_re, one_re, sub_eq_add_neg] using lt_add_of_pos_left _ hs

Premises used: Complex.sub_re, sub_eq_add_neg, lt_add_of_pos_left, Complex.one_re
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
⊢ -1 < (s - 1).re

Tactic:
have aux1 : -1 < (s - 1).re := by
    simpa only [sub_re, one_re, sub_eq_add_neg] using lt_add_of_pos_left _ hs
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
contrapose! : ∀ (hs : s = 0), s.re ≤ 0
⊢ s ≠ 0

Tactic:
contrapose! hs
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
rw : re 0 ≤ 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ s.re ≤ 0

Tactic:
rw [hs, zero_re]

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ s ≠ 0

Tactic:
have aux2 : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
⊢ MeasurableSet (α := ℝ) (Ioc 0 1)

Tactic:
have aux3 : MeasurableSet (Ioc (0 : ℝ) 1) := measurableSet_Ioc
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
simp_rw :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioc 0 1)) ∧
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) =
      1 / s
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) s (1 / s)

Tactic:
simp_rw [HasMellin, mellin, MellinConvergent, ← indicator_smul, IntegrableOn,
    integrable_indicator_iff aux3, smul_eq_mul, integral_indicator aux3, mul_one, IntegrableOn,
    Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]

Premises used: MeasureTheory.integral_indicator, Set.indicator_smul, MeasureTheory.IntegrableOn, Set.Ioc_subset_Ioi_self, MeasureTheory.Measure.restrict_restrict_of_subset, MellinConvergent, smul_eq_mul, mul_one, mellin, HasMellin, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
rw :
  IntervalIntegrable (ε := ℂ) (fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) volume 0 1 ∧
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) =
      1 / s
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioc 0 1)) ∧
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) =
      1 / s

Tactic:
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, MeasureTheory.IntegrableOn, zero_le_one
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
⊢ IntervalIntegrable (ε := ℂ) (fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) volume 0 1 ∧
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) =
      1 / s

Tactic:
⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩

Premises used: And.intro, intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
refine :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
⊢ IntervalIntegrable (ε := ℂ) (fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) volume 0 1 ∧
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) =
      1 / s

Tactic:
refine ⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩
-- Module: Mathlib.Analysis.MellinTransform
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
rw : ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1) = 1 / s
rw₁ : ((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1) = 1 / s
rw₂ : ((↑1 : ℂ) ^ s - (↑0 : ℂ) ^ s) / s = 1 / s
rw₃ : ((↑1 : ℂ) ^ s - HPow.hPow (α := ℂ) 0 s) / s = 1 / s
rw₄ : (HPow.hPow (α := ℂ) 1 s - HPow.hPow (α := ℂ) 0 s) / s = 1 / s
rw₅ : (1 - HPow.hPow (α := ℂ) 0 s) / s = 1 / s
rw₆ : HSub.hSub (α := ℂ) 1 0 / s = 1 / s
rw₇ rw₈ : 1 / s = 1 / s
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s

Tactic:
rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl aux1), sub_add_cancel,
    ofReal_zero, ofReal_one, one_cpow, zero_cpow aux2, sub_zero]

Premises used: sub_zero, integral_cpow, Complex.ofReal_one, zero_le_one, Complex.zero_cpow, intervalIntegral.integral_of_le, Complex.ofReal_zero, Complex.one_cpow, Or.inl, sub_add_cancel
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a s : ℂ
hs rwa rwa₁ rwa₂ rwa₃ : 0 < s.re + a.re
⊢ 0 < (s + a).re

Tactic:
rwa [add_re]

Premises used: Complex.add_re
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a s : ℂ
hs : 0 < s.re + a.re
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) (s + a) (1 / (s + a))

Tactic:
have := hasMellin_one_Ioc (by rwa [add_re] : 0 < (s + a).re)
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a s : ℂ
hs : 0 < s.re + a.re
this : HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) (s + a) (1 / (s + a))
⊢ MellinConvergent (E := ℂ) (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s ∧
    mellin (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s = 1 / (s + a)

Tactic:
simp_rw [HasMellin, ← MellinConvergent.cpow_smul, ← mellin_cpow_smul, ← indicator_smul,
    smul_eq_mul, mul_one] at this

Premises used: Set.indicator_smul, smul_eq_mul, mul_one, MellinConvergent.cpow_smul, HasMellin, mellin_cpow_smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent (E := ℂ) (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s ∧
    mellin (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s = 1 / (s + a)
⊢ HasMellin (indicator (Ioc 0 1) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) s (1 / (s + a))

Tactic:
this

Premises used: HasMellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent (E := ℂ) (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s ∧
    mellin (indicator (Ioc 0 1) fun (a_1 : ℝ) ↦ (↑a_1 : ℂ) ^ a) s = 1 / (s + a)
⊢ HasMellin (indicator (Ioc 0 1) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) s (1 / (s + a))

Tactic:
exact this
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ HPow.hPow (β := ℕ) (z - x) 0 • f z) x

Tactic:
simpa only [pow_zero, one_smul]

Premises used: pow_zero, one_smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : MeromorphicAt f z₀
obtain :
  ∀ (n : ℕ) (h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀),
    (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
obtain ⟨n, h⟩ := hf
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
inl :
  ∀ (h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0), (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
inr :
  ∀ (h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0),
    (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
rcases h.eventually_eq_zero_or_eventually_ne_zero with h₁ | h₂

Premises used: AnalyticAt.eventually_eq_zero_or_eventually_ne_zero
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
inl : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
left
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
h₂ : ∀ (y : 𝕜) (h₁y : (y - z₀) ^ n • f y = 0) (h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y), f y = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0

Tactic:
filter_upwards [nhdsWithin_le_nhds h₁, self_mem_nhdsWithin] with y h₁y h₂y

Premises used: nhdsWithin_le_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y
⊢ ¬y - z₀ = 0

Tactic:
rw [Set.mem_compl_iff, Set.mem_singleton_iff, ← sub_eq_zero] at h₂y

Premises used: sub_eq_zero, Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0

Tactic:
smul_eq_zero_iff_right (pow_ne_zero n h₂y) |>.mp h₁y

Premises used: pow_ne_zero, smul_eq_zero_iff_right, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • f z = 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y = 0
h₂y : ¬y - z₀ = 0
⊢ f y = 0

Tactic:
exact smul_eq_zero_iff_right (pow_ne_zero n h₂y) |>.mp h₁y

Premises used: pow_ne_zero, smul_eq_zero_iff_right, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
inr : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
right
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
h₁ : ∀ (y : 𝕜) (h₁y : (y - z₀) ^ n • f y ≠ 0) (h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y), f y ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
filter_upwards [h₂, self_mem_nhdsWithin] with y h₁y h₂y

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y ≠ 0
h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y
⊢ f y ≠ 0

Tactic:
(smul_ne_zero_iff.1 h₁y).2

Premises used: smul_ne_zero_iff, And.right, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ n • f z) z₀
h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • f z ≠ 0
y : 𝕜
h₁y : (y - z₀) ^ n • f y ≠ 0
h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y
⊢ f y ≠ 0

Tactic:
exact (smul_ne_zero_iff.1 h₁y).2

Premises used: smul_ne_zero_iff, And.right, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ MeromorphicAt _root_.id x

Tactic:
analyticAt_id.meromorphicAt

Premises used: analyticAt_id, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
e : E
x : 𝕜
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (x : 𝕜) ↦ e) x

Tactic:
analyticAt_const.meromorphicAt

Premises used: analyticAt_const, AnalyticAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
rcases :
  ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f + g) x
⊢ MeromorphicAt (f + g) x

Tactic:
rcases hf with ⟨m, hf⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
rcases :
  ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f + g) x
⊢ MeromorphicAt (f + g) x

Tactic:
rcases hg with ⟨n, hg⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ MeromorphicAt (f + g) x

Tactic:
⟨max m n, ?_⟩

Premises used: Max.max, Exists.intro, MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) x
⊢ MeromorphicAt (f + g) x

Tactic:
refine ⟨max m n, ?_⟩
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
simp_rw :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    ((z - x) ^ (max m n - m) * (z - x) ^ m) • f z + ((z - x) ^ (max m n - n) * (z - x) ^ n) • g z
simp_rw₁ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m + m) • f z + (z - x) ^ (max m n - n + n) • g z
simp_rw₂ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ max m n • f z + (z - x) ^ (max m n - n + n) • g z
simp_rw₃ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ max m n • f z + (z - x) ^ max m n • g z
simp_rw₄ :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f z + g z)) fun (z : 𝕜) ↦
    (z - x) ^ max m n • f z + (z - x) ^ max m n • g z
⊢ Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z

Tactic:
simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]

Premises used: Nat.le_max_right, Nat.le_max_left, pow_add, Pi.add_apply, Nat.sub_add_cancel, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
⊢ Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z

Tactic:
have : (fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦ (z - x) ^ (max m n - m) •
      ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) := by
    simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _),
      Nat.sub_add_cancel (Nat.le_max_right _ _), Pi.add_apply, smul_add]
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
this :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
rw :
  AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) x

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
this :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x

Tactic:
(((analyticAt_id.sub analyticAt_const).pow _).smul hf).add
    (((analyticAt_id.sub analyticAt_const).pow _).smul hg)

Premises used: AnalyticAt.smul, analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.add, AnalyticAt.pow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
n : ℕ
hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x
this :
  Eq (α := (z : 𝕜) → E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) fun (z : 𝕜) ↦
    (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E)
    (fun (z : 𝕜) ↦ (z - x) ^ (max m n - m) • (z - x) ^ m • f z + (z - x) ^ (max m n - n) • (z - x) ^ n • g z) x

Tactic:
exact (((analyticAt_id.sub analyticAt_const).pow _).smul hf).add
    (((analyticAt_id.sub analyticAt_const).pow _).smul hg)

Premises used: AnalyticAt.smul, analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.add, AnalyticAt.pow