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
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₀))
⊢ 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₀))
have 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₀))
Tactic: simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]
-- 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 :
  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₀))
⊢ 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₀))
have 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₀))
Tactic: simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]
-- 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
⊢ 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₀)
have 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₀
Tactic: refine setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)
-- 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
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx : 0 < x
right : 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₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]
-- 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
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₀
⊢ (↑x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) =
    (↑x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (↑x : ℂ) ^ (s - (↑P.k : ℂ) - 1) • P.g₀
have 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₀
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]