-- 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₀
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₀
simp_rw₈ :
  (HSub.hSub (α := ℂ) 1 0 / s) • P.f₀ - P.ε • (HSub.hSub (α := ℂ) 1 0 / (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₉ : (1 / s) • P.f₀ - P.ε • (1 / (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]