awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
have h6 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y
Tactic: have h6 : ∀ᵐ t : ℝ ∂volume.restrict (Ioi 0),
      ∀ y : ℂ, y ∈ Metric.ball s v → HasDerivAt (fun z : ℂ => F z t) (F' y t) y := by
    refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht y _ => ?_
    have ht' : (t : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt ht)
    have u1 : HasDerivAt (fun z : ℂ => (t : ℂ) ^ (z - 1)) (t ^ (y - 1) * log t) y := by
      convert! ((hasDerivAt_id' y).sub_const 1).const_cpow (Or.inl ht') using 1
      rw [ofReal_log (le_of_lt ht)]
      ring
    exact u1.smul_const (f t)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
have 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
Tactic: have main :=
    hasDerivAt_integral_of_dominated_loc_of_deriv_le (Metric.ball_mem_nhds _ hv0) h1 h2 h3 h4 h5 h6
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) s (1 / s)
have aux1 : -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
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ s ≠ 0
have contrapose! : ∀ (hs : s = 0), s.re ≤ 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
⊢ s.re ≤ 0
have rw : re 0 ≤ 0
Tactic: rw [hs, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
rw : re 0 ≤ 0
⊢ s.re ≤ 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [hs, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) s (1 / s)
have aux2 : s ≠ 0
Tactic: have aux2 : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) s (1 / s)
have aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
Tactic: have aux3 : MeasurableSet (Ioc (0 : ℝ) 1) := measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
⊢ HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) s (1 / s)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
⊢ @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
have 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
Tactic: rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
have refine : (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
Tactic: refine ⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (α := ℝ) (Ioc 0 1)
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw : ∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₁ : ((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₂ : ((↑1 : ℂ) ^ s - (↑0 : ℂ) ^ s) / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₃ : ((↑1 : ℂ) ^ s - HPow.hPow (α := ℂ) 0 s) / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₄ : (HPow.hPow (α := ℂ) 1 s - HPow.hPow (α := ℂ) 0 s) / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₅ : (1 - HPow.hPow (α := ℂ) 0 s) / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₆ : HSub.hSub (α := ℂ) 1 0 / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1)) = 1 / s
have rw₇ : 1 / s = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
a s : ℂ
hs : 0 < s.re + a.re
⊢ HasMellin (indicator (Ioc 0 1) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) s (1 / (s + a))
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
a s : ℂ
hs : 0 < s.re + a.re
this : HasMellin (indicator (Ioc 0 1) fun (x : ℝ) ↦ 1) (s + a) (1 / (s + a))
⊢ HasMellin (indicator (Ioc 0 1) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) s (1 / (s + a))
have 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)
Tactic: simp_rw [HasMellin, ← MellinConvergent.cpow_smul, ← mellin_cpow_smul, ← indicator_smul,
    smul_eq_mul, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have 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
Tactic: obtain ⟨n, h⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have inl : ∀ (h₁ : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (z - z₀) ^ n • 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₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have inr : ∀ (h₂ : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, (z - z₀) ^ n • 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₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have inl : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0
have h₂ : ∀ (y : 𝕜) (h₁y : (y - z₀) ^ n • f y = 0) (h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y), f y = 0
Tactic: filter_upwards [nhdsWithin_le_nhds h₁, self_mem_nhdsWithin] with y h₁y h₂y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (hypothesis)
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
have h₂y₁ : ¬y - z₀ = 0
Tactic: rw [Set.mem_compl_iff, Set.mem_singleton_iff, ← sub_eq_zero] at h₂y
Cleared hypotheses: h₂y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ (∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have inr : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have h₁ : ∀ (y : 𝕜) (h₁y : (y - z₀) ^ n • f y ≠ 0) (h₂y : Membership.mem (γ := Set 𝕜) {z₀}ᶜ y), f y ≠ 0
Tactic: filter_upwards [h₂, self_mem_nhdsWithin] with y h₁y h₂y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicAt (f + g) x
have rcases : ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt (f + g) x
Tactic: rcases hf with ⟨m, hf⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ MeromorphicAt (f + g) x
have rcases : ∀ (n : ℕ) (hg : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • g z) x), MeromorphicAt (f + g) x
Tactic: rcases hg with ⟨n, hg⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
have refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ max m n • (f + g) z) x
Tactic: refine ⟨max m n, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Basic (goal)
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
⊢ 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
have 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
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]