awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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
⊢ (@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₀
have hf : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1) • P.f₀)
  (Measure.restrict volume (Ioc 0 1))
Tactic: rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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))
⊢ (@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₀
have hg : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀)
  (Measure.restrict volume (Ioc 0 1))
Tactic: rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 : ℝ) ↦ (↑x : ℂ) ^ (s - 1) • P.f₀)
    (Measure.restrict volume (Ioc 0 1))
have hf : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1))
  (Measure.restrict volume (Ioc 0 1))
Tactic: apply Integrable.smul_const
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioc 0 1))
have hf : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) volume 0 1
Tactic: rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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))
have hg : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1))
  (Measure.restrict volume (Ioc 0 1))
Tactic: refine (Integrable.smul_const ?_ _).smul _
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))
have hg : IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) volume 0 1
Tactic: rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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
⊢ 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw : HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
    P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₁ : (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
    P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₂ : (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
    P.ε •
      (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) • P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₂ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₃ : (((↑1 : ℂ) ^ (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
    P.ε •
      (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
          (s - (↑P.k : ℂ) - 1 + 1)) •
        P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₂ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₃ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₄ : ((HPow.hPow (α := ℂ) 1 (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
    P.ε •
      ((HPow.hPow (α := ℂ) 1 (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
          (s - (↑P.k : ℂ) - 1 + 1)) •
        P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₂ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₃ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₄ :
  ((HPow.hPow (α := ℂ) 1 (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        ((HPow.hPow (α := ℂ) 1 (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₅ : ((1 - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
    P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) • P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₂ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₃ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₄ :
  ((HPow.hPow (α := ℂ) 1 (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        ((HPow.hPow (α := ℂ) 1 (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₅ :
  ((1 - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₆ : ((1 - HPow.hPow (α := ℂ) 0 s) / s) • P.f₀ -
    P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ))) / (s - (↑P.k : ℂ))) • P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
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 :
  HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - 1)) P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₁ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • HSMul.hSMul (α := ℂ) (∫ (x : ℝ) in 0..1, (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1)) P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₂ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - (↑0 : ℂ) ^ (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - (↑0 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₃ :
  (((↑1 : ℂ) ^ (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        (((↑1 : ℂ) ^ (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₄ :
  ((HPow.hPow (α := ℂ) 1 (s - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε •
        ((HPow.hPow (α := ℂ) 1 (s - (↑P.k : ℂ) - 1 + 1) - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) /
            (s - (↑P.k : ℂ) - 1 + 1)) •
          P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₅ :
  ((1 - HPow.hPow (α := ℂ) 0 (s - 1 + 1)) / (s - 1 + 1)) • P.f₀ -
      P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ) - 1 + 1)) / (s - (↑P.k : ℂ) - 1 + 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
simp_rw₆ :
  ((1 - HPow.hPow (α := ℂ) 0 s) / s) • P.f₀ -
      P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ))) / (s - (↑P.k : ℂ))) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • 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₀ =
    (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have simp_rw₇ : (HSub.hSub (α := ℂ) 1 0 / s) • P.f₀ - P.ε • ((1 - HPow.hPow (α := ℂ) 0 (s - (↑P.k : ℂ))) / (s - (↑P.k : ℂ))) • P.g₀ =
  (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
Tactic: simp_rw [← intervalIntegral.integral_of_le zero_le_one,
      integral_cpow (Or.inl h_re1), integral_cpow (Or.inl h_re2), ofReal_zero, ofReal_one,
      one_cpow, sub_add_cancel, zero_cpow fun h ↦ lt_irrefl _ (P.hk.le.trans_lt (zero_re ▸ h ▸ hs)),
      zero_cpow (sub_ne_zero.mpr (fun h ↦ lt_irrefl _ ((ofReal_re _) ▸ h ▸ hs)) : s - P.k ≠ 0),
      sub_zero, sub_eq_add_neg (_ • _), ← mul_smul, ← neg_smul, mul_one_div, ← div_neg, neg_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ₀ s = P.Λ s + (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have 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₀
Tactic: unfold Λ Λ₀
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.symm.Λ₀ s = P.symm.Λ s + (1 / s) • P.g₀ + (P.ε⁻¹ / ((↑P.k : ℂ) - s)) • P.f₀
have 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₀
Tactic: rw [P.symm.Λ₀_eq]