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
this : LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (𝓝[Ioi 0] x) volume
have refine_2 : ∀ (s : Set ℝ) (hs : s ∈ 𝓝[Ioi 0] x)
  (hs' : IntegrableOn (mα := Real.measurableSpace) (P.f - fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) s volume),
  IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace)
    (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (𝓝[Ioi 0] x) volume
Tactic: obtain ⟨s, hs, hs'⟩ := P.hf_int.sub this 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
x : ℝ
hx : 0 < x
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have inl : ∀ (hx' : 1 < x), P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
Tactic: rcases lt_trichotomy 1 x with hx' | rfl | 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
x : ℝ
hx : 0 < x
inl : ∀ (hx' : 1 < x), P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have inr : ∀ (hx : LT.lt (α := ℝ) 0 1), P.f_modif (1 / 1) = (P.ε * (↑(HPow.hPow (α := ℝ) 1 P.k) : ℂ)) • P.g_modif 1
Tactic: rcases lt_trichotomy 1 x with hx' | rfl | hx'
Cleared hypotheses: 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
x : ℝ
hx : 0 < x
inl : ∀ (hx' : 1 < x), P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
inr : ∀ (hx : LT.lt (α := ℝ) 0 1), P.f_modif (1 / 1) = (P.ε * (↑(HPow.hPow (α := ℝ) 1 P.k) : ℂ)) • P.g_modif 1
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have inr₁ : ∀ (hx' : x < 1), P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
Tactic: rcases lt_trichotomy 1 x with hx' | rfl | 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
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ 1 / x < 1
have rwa : 1 / 1 < x
Tactic: rwa [one_div_lt hx one_pos, div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have this : 1 / x < 1
Tactic: have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_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
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have inl : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ (-P.k)) : ℂ)) • P.g₀ =
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
Tactic: rw [f_modif, Pi.add_apply, indicator_of_notMem (notMem_Ioi.mpr this.le),
      zero_add, indicator_of_mem (mem_Ioo.mpr ⟨div_pos one_pos hx, this⟩), g_modif, Pi.add_apply,
      indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem
      (notMem_Ioo_of_ge hx'.le), add_zero, P.h_feq _ hx, smul_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
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ (-P.k)) : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
have inl : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ P.k)⁻¹ : ℂ)) • P.g₀ =
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
Tactic: simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]
-- 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
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
inl :
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ P.k)⁻¹ : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ (-P.k)) : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
have inl₁ : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x⁻¹ ^ P.k)⁻¹ : ℂ)) • P.g₀ =
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
Tactic: simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]
-- 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
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
inl :
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ P.k)⁻¹ : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
inl₁ :
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x⁻¹ ^ P.k)⁻¹ : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑((1 / x) ^ (-P.k)) : ℂ)) • P.g₀ =
    (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
have inl₂ : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k)⁻¹⁻¹ : ℂ)) • P.g₀ =
  (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - (P.ε * (↑(x ^ P.k) : ℂ)) • P.g₀
Tactic: simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]
-- 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
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ 1 < 1 / x
have rwa : x < 1 / 1
Tactic: rwa [lt_one_div one_pos hx, div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have this : 1 < 1 / x
Tactic: have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_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
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x
have inr : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - P.f₀ + 0 =
  (P.ε * (↑(x ^ P.k) : ℂ)) • (0 + (P.g x - (P.ε⁻¹ * (↑(x ^ (-P.k)) : ℂ)) • P.f₀))
Tactic: rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this),
      indicator_of_notMem (notMem_Ioo_of_ge this.le), g_modif, Pi.add_apply,
      indicator_of_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩), P.h_feq _ 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
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - P.f₀ + 0 =
    (P.ε * (↑(x ^ P.k) : ℂ)) • (0 + (P.g x - (P.ε⁻¹ * (↑(x ^ (-P.k)) : ℂ)) • P.f₀))
have inr : (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - P.f₀ + 0 =
  (P.ε * (↑(x ^ P.k) : ℂ)) • (0 + (P.g x - (P.ε⁻¹ * (↑(x ^ P.k)⁻¹ : ℂ)) • P.f₀))
Tactic: simp_rw [rpow_neg hx.le]
-- 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
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - P.f₀ + 0 =
    (P.ε * (↑(x ^ P.k) : ℂ)) • (0 + (P.g x - (P.ε⁻¹ * (↑(x ^ P.k)⁻¹ : ℂ)) • P.f₀))
have match_scalars : P.ε * (↑(x ^ P.k) : ℂ) * 1 = P.ε * (↑(x ^ P.k) : ℂ) * 1
Tactic: match_scalars
-- 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
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / x
match_scalars : P.ε * (↑(x ^ P.k) : ℂ) * 1 = P.ε * (↑(x ^ P.k) : ℂ) * 1
⊢ (P.ε * (↑(x ^ P.k) : ℂ)) • P.g x - P.f₀ + 0 =
    (P.ε * (↑(x ^ P.k) : ℂ)) • (0 + (P.g x - (P.ε⁻¹ * (↑(x ^ P.k)⁻¹ : ℂ)) • P.f₀))
have match_scalars₁ : -1 = P.ε * (↑(x ^ P.k) : ℂ) * -(P.ε⁻¹ * (↑(x ^ P.k) : ℂ)⁻¹ * 1)
Tactic: match_scalars
-- 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
r : ℝ
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (x : ℝ) ↦ P.f_modif x - 0) fun (x : ℝ) ↦ x ^ r
have refine : EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ P.f_modif x - 0
Tactic: refine (P.hf_top r).congr' ?_ (by rfl)
-- 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
r : ℝ
⊢ EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ P.f_modif x - 0
have h : ∀ (x : ℝ) (hx : 1 < x), P.f x - P.f₀ = P.f_modif x - 0
Tactic: filter_upwards [eventually_gt_atTop 1] with 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
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x →
    (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) x =
      HAdd.hAdd (α := (x : ℝ) → E) (β := (x : ℝ) → E)
        (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀)
        (indicator {1} fun (x : ℝ) ↦ P.f₀ - P.f 1) x
have this : ∀ (hx : 0 < x),
  (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) x =
    HAdd.hAdd (α := (x : ℝ) → E) (β := (x : ℝ) → E)
      (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀)
      (indicator {1} fun (x : ℝ) ↦ P.f₀ - P.f 1) x
Tactic: (hx : 0 < x)
-- 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
x : ℝ
hx : 0 < x
⊢ (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) x =
    HAdd.hAdd (α := (x : ℝ) → E) (β := (x : ℝ) → E)
      (indicator (Ioo 0 1) fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀)
      (indicator {1} fun (x : ℝ) ↦ P.f₀ - P.f 1) x
have simp_rw : 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 [f_modif, Pi.add_apply]
-- 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
x : ℝ
hx : 0 < x
⊢ 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)
have inl : ∀ (hx' : x < 1),
  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: rcases lt_trichotomy x 1 with hx' | rfl | 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
x : ℝ
hx : 0 < x
inl :
  ∀ (hx' : x < 1),
    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)
⊢ 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)
have inr : ∀ (hx : LT.lt (α := ℝ) 0 1),
  HAdd.hAdd (α := E) (indicator (Ioi 1) (fun (x : ℝ) ↦ P.f x - P.f₀) 1)
          (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) 1) -
        P.f 1 +
      P.f₀ =
    HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) 1)
      (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) 1)
Tactic: rcases lt_trichotomy x 1 with hx' | rfl | hx'
Cleared hypotheses: 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
x : ℝ
hx : 0 < x
inl :
  ∀ (hx' : x < 1),
    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)
inr :
  ∀ (hx : LT.lt (α := ℝ) 0 1),
    HAdd.hAdd (α := E) (indicator (Ioi 1) (fun (x : ℝ) ↦ P.f x - P.f₀) 1)
            (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) 1) -
          P.f 1 +
        P.f₀ =
      HAdd.hAdd (α := E) (indicator (Ioo 0 1) (fun (x : ℝ) ↦ P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) 1)
        (indicator {1} (fun (x : ℝ) ↦ P.f₀ - P.f 1) 1)
⊢ 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)
have inr₁ : ∀ (hx' : 1 < x),
  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: rcases lt_trichotomy x 1 with hx' | rfl | 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
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ 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)
have inl : 0 + (P.f x - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) - P.f x + P.f₀ = P.f₀ - (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀ + 0
Tactic: simp_rw [indicator_of_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]
-- 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
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ 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)
have inr : P.f x - P.f₀ + 0 - P.f x + P.f₀ = HAdd.hAdd (α := E) 0 0
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')]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
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
⊢ mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have h_re1 : -1 < (s - 1).re
Tactic: have h_re1 : -1 < re (s - 1) := by simpa using P.hk.trans hs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.AbstractFuncEq (hypothesis)
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
⊢ mellin (fun (x : ℝ) ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / ((↑P.k : ℂ) - s)) • P.g₀
have h_re2 : -1 < (s - (↑P.k : ℂ) - 1).re
Tactic: have h_re2 : -1 < re (s - P.k - 1) := by simpa using hs
-- 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 (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))
have 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)
Tactic: refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (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 : ℝ
hx : Membership.mem (γ := Set ℝ) {1}ᶜ x
h : 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)
have 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)
Tactic: rw [indicator_of_notMem hx, add_zero]
-- 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 : ℝ
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)
⊢ (↑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)
have 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)
Tactic: rw [indicator_of_notMem hx, add_zero]
-- 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 (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))
    (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₀))
Tactic: simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]