awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
inr : P.f x - P.f₀ + 0 - P.f x + P.f₀ = HAdd.hAdd (α := E) 0 0
⊢ HAdd.hAdd (α := E) (indicator (Ioi 1) (fun (x : ℝ) ↦ P.f x - P.f₀) x)
          (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x) -
        P.f x +
      P.f₀ =
    HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x)
      (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x)

Tactic:
simp_rw [indicator_of_mem (mem_Ioi.mpr hx'),
      indicator_of_notMem (notMem_Ioo_of_ge hx'.le),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne')]

Premises used: Iff.mpr, Set.mem_Ioi, Iff.not, LT.lt.le, LT.lt.ne', Set.notMem_Ioo_of_ge, Set.indicator_of_mem, Set.mem_singleton_iff, Set.indicator_of_notMem
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ P.f x - P.f₀ + 0 - P.f x + P.f₀ = HAdd.hAdd (α := E) 0 0

Tactic:
abel
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ -1 < (s - 1).re

Tactic:
simpa using P.hk.trans hs

Premises used: WeakFEPair.hk, LT.lt.trans
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ -1 < (s - 1).re

Tactic:
have h_re1 : -1 < re (s - 1) := by simpa using P.hk.trans hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ -1 < (s - (↑P.k : ℂ) - 1).re

Tactic:
simpa using hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ -1 < (s - (↑P.k : ℂ) - 1).re

Tactic:
have h_re2 : -1 < re (s - P.k - 1) := by simpa using hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1)) ((fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) x) =
    (↑x : ℂ) ^ (s - 1) •
      HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
        (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x)

Tactic:
simp [f_modif_aux1 P hx]

Premises used: WeakFEPair.f_modif_aux1
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) •
        HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
          (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
        (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x))

Tactic:
setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))

Premises used: Iff.mpr, MeasureTheory.setIntegral_congr_ae, measurableSet_Ioi, Set.subsingleton_singleton, Filter.eventually_of_mem, Set.Subsingleton.measure_zero, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {1}ᶜ x),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      (↑x : ℂ) ^ (s - 1) •
          HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
            (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x) =
        HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
          (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) •
        HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
          (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
        (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x))

Tactic:
refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))

Premises used: Iff.mpr, MeasureTheory.setIntegral_congr_ae, measurableSet_Ioi, Set.subsingleton_singleton, Filter.eventually_of_mem, Set.Subsingleton.measure_zero, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
x : ℝ
hx : Membership.mem (γ := Set ℝ) {1}ᶜ x
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (↑x : ℂ) ^ (s - 1) •
      HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x) 0 =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
      (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
rw₁ rw₂ :
  HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
      (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
      (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
⊢ (↑x : ℂ) ^ (s - 1) •
      HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)
        (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) x) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
      (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x)

Tactic:
rw [indicator_of_notMem hx, add_zero]

Premises used: Set.indicator_of_notMem, add_zero
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
simp_rw :
  Eq.{u_1 + 1} (α := E)
    (@integral ℝ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0))
      (indicator (Ioo 0 1) fun (a : ℝ) ↦ (↑a : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(a ^ (-P.k)) : ℂ)) • P.g₀)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))
simp_rw₁ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0 ∩ Ioo 0 1)) fun (a : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(a ^ (-P.k)) : ℂ)) • P.g₀))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))
simp_rw₂ :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      (↑a : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(a ^ (-P.k)) : ℂ)) • P.g₀))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑x : ℂ) ^ (s - 1))
        (indicator (Ioo 0 1) (fun (t : ℝ) ↦ P.f₀ - (P.ε * (↑(t ^ (-P.k)) : ℂ)) • P.g₀) x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))

Tactic:
simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]

Premises used: Iff.mpr, Set.indicator_smul, MeasureTheory.setIntegral_indicator, Set.inter_eq_right, MeasureTheory.integral_Ioc_eq_integral_Ioo, measurableSet_Ioo, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀)

Tactic:
setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)

Premises used: _private.0.WeakFEPair.f_modif_aux2.match_1, HMul.hMul, HSub.hSub, WeakFEPair.ε, WeakFEPair.g₀, WeakFEPair.f₀, Complex.ofReal, MeasureTheory.setIntegral_congr_fun, HPow.hPow, WeakFEPair.k, HSMul.hSMul, measurableSet_Ioc, OfNat.ofNat, Eq, Neg.neg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioc 0 1) x →
      ∀ (hx : 0 < x),
        x ≤ 1 →
          (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
            (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx : 0 < x
right : x ≤ 1
rw :
  (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑x : ℂ) ^ (↑(-P.k) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₁ :
  (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑x : ℂ) ^ (-(↑P.k : ℂ))) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₂ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - (↑x : ℂ) ^ (s - 1) • (P.ε * (↑x : ℂ) ^ (-(↑P.k : ℂ))) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₃ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - ((↑x : ℂ) ^ (s - 1) * (P.ε * (↑x : ℂ) ^ (-(↑P.k : ℂ)))) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₄ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - (P.ε * (↑x : ℂ) ^ (-(↑P.k : ℂ)) * (↑x : ℂ) ^ (s - 1)) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₅ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - (P.ε * ((↑x : ℂ) ^ (-(↑P.k : ℂ)) * (↑x : ℂ) ^ (s - 1))) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₆ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • ((↑x : ℂ) ^ (-(↑P.k : ℂ)) * (↑x : ℂ) ^ (s - 1)) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₇ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • ((↑x : ℂ) ^ (s - 1) * (↑x : ℂ) ^ (-(↑P.k : ℂ))) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₈ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - 1 + -(↑P.k : ℂ)) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₉ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - 1 - (↑P.k : ℂ)) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
rw₁₀ rw₁₁ :
  (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀ =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀

Tactic:
rw [ofReal_cpow hx.le, ofReal_neg, smul_sub, ← mul_smul, mul_comm, mul_assoc, mul_smul,
      mul_comm, ← cpow_add _ _ (ofReal_ne_zero.mpr hx.ne'), ← sub_eq_add_neg, sub_right_comm]

Premises used: Iff.mpr, Complex.ofReal_cpow, mul_assoc, sub_eq_add_neg, Complex.ofReal_neg, Complex.ofReal_ne_zero, LT.lt.le, sub_right_comm, LT.lt.ne', smul_sub, Complex.cpow_add, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
hf :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1) • P.f₀)
    (Measure.restrict volume (Ioc 0 1))
hg :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀) (Measure.restrict volume (Ioc 0 1))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀) =
    HSMul.hSMul (α := ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1))
        P.f₀ -
      P.ε •
        HSMul.hSMul (α := ℂ)
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
            (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1))
          P.g₀

Tactic:
rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]

Premises used: integral_smul_const, MeasureTheory.integral_smul, MeasureTheory.integral_sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
hf :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioc 0 1))
⊢ @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1) • P.f₀)
    (Measure.restrict volume (Ioc 0 1))

Tactic:
apply Integrable.smul_const

Premises used: MeasureTheory.Integrable.smul_const
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 1
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioc 0 1))

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.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 1

Tactic:
intervalIntegral.intervalIntegrable_cpow' h_re1

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 1

Tactic:
exact intervalIntegral.intervalIntegrable_cpow' h_re1

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀) (Measure.restrict volume (Ioc 0 1))

Tactic:
(Integrable.smul_const ?_ _).smul _

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.smul_const
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
hg :
  @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))
⊢ @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀) (Measure.restrict volume (Ioc 0 1))

Tactic:
refine (Integrable.smul_const ?_ _).smul _

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.smul_const
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
hg : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) volume 0 1
⊢ @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))

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.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) volume 0 1

Tactic:
intervalIntegral.intervalIntegrable_cpow' h_re2

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
inst_2 : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) volume 0 1

Tactic:
exact intervalIntegral.intervalIntegrable_cpow' h_re2

Premises used: intervalIntegral.intervalIntegrable_cpow'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
unfold :
  mellin P.f_modif s =
    mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀ + (1 / s) • P.f₀ +
      (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
⊢ P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

Tactic:
unfold Λ Λ₀

Premises used: WeakFEPair.Λ₀, WeakFEPair.Λ
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ mellin P.f_modif s =
    mellin P.f_modif s - (1 / s) • P.f₀ - (P.ε / ((↑P.k : ℂ) - s)) • P.g₀ + (1 / s) • P.f₀ +
      (P.ε / ((↑P.k : ℂ) - s)) • P.g₀

Tactic:
abel
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
rw :
  P.symm.Λ s + (1 / s) • P.symm.f₀ + (P.symm.ε / ((↑P.symm.k : ℂ) - s)) • P.symm.g₀ =
    P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀
⊢ P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀

Tactic:
rw [P.symm.Λ₀_eq]

Premises used: WeakFEPair.Λ₀_eq, WeakFEPair.symm
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ s + (1 / s) • P.symm.f₀ + (P.symm.ε / ((↑P.symm.k : ℂ) - s)) • P.symm.g₀ =
    P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ Differentiable ℂ P.Λ₀

Tactic:
P.toStrongFEPair.differentiable_Λ

Premises used: WeakFEPair.Λ₀, StrongFEPair.differentiable_Λ, WeakFEPair.toStrongFEPair, WeakFEPair.f_modif
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ P.Λ s

Tactic:
((P.differentiable_Λ₀ s).sub ?_).sub ?_

Premises used: WeakFEPair.Λ, DifferentiableAt.sub, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_1 : DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
refine_2 : DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (P.ε / ((↑P.k : ℂ) - s)) • P.g₀) s
⊢ DifferentiableAt ℂ P.Λ s

Tactic:
refine ((P.differentiable_Λ₀ s).sub ?_).sub ?_

Premises used: DifferentiableAt.sub, WeakFEPair.differentiable_Λ₀
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
refine_1 : ∀ (hs : s ≠ 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
refine_1₁ : ∀ (hs : P.f₀ = 0), DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s

Tactic:
rcases hs with hs | hs
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s

Tactic:
simpa using (differentiableAt_inv hs).smul_const _

Premises used: DifferentiableAt.smul_const, differentiableAt_inv
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ (↑P.k : ℂ) ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt.{0, 0, u_1} ℂ (F := E) (fun (s : ℂ) ↦ (1 / s) • P.f₀) s

Tactic:
simp [hs]