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 : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (↑P.k : ℂ) ≠ 0

Tactic:
simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'

Premises used: Real.rpow_pos_of_pos, Complex.ofReal_cpow, LT.lt.le, LT.lt.ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (↑P.k : ℂ) ≠ 0

Tactic:
have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : StrongFEPair E
s : ℂ
step1 : mellin (fun (t : ℝ) ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = mellin P.g s
step3 : mellin (fun (t : ℝ) ↦ P.ε • (↑t : ℂ) ^ (-(↑P.k : ℂ)) • P.g (1 / t)) ((↑P.k : ℂ) - s) = P.ε • mellin P.g s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
this : (↑t : ℂ) ^ (↑P.k : ℂ) ≠ 0
⊢ (↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) • P.f t =
    ((↑t : ℂ) ^ ((↑P.k : ℂ) - s - 1) * (P.ε * (((↑t : ℂ) ^ (↑P.k : ℂ))⁻¹ * (P.ε⁻¹ * (↑t : ℂ) ^ (↑P.k : ℂ))))) • P.f t

Tactic:
field_simp [P.hε]

Premises used: StrongFEPair.toWeakFEPair, WeakFEPair.hε
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume

Tactic:
ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi

Premises used: measurableSet_Ioi, ContinuousOn.locallyIntegrableOn
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0)
⊢ LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume

Tactic:
refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi

Premises used: measurableSet_Ioi, ContinuousOn.locallyIntegrableOn
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0)

Tactic:
continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
refine : ∀ (x : ℝ) (hx : 0 < x), ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ x ≠ 0 ∨ 0 ≤ -P.k

Tactic:
have : x ≠ 0 ∨ 0 ≤ -P.k := Or.inl hx.ne'
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
this funProp : x ≠ 0 ∨ 0 ≤ -P.k
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn.{0, u_1} (ε := E) (fun (x : ℝ) ↦ (P.ε * (↑(x ^ (-P.k)) : ℂ)) • P.g₀) (Ioi 0) volume

Tactic:
have : LocallyIntegrableOn (fun x : ℝ ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) := by
    refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi
    refine continuousOn_of_forall_continuousAt (fun x (hx : 0 < x) ↦ ?_)
    have : x ≠ 0 ∨ 0 ≤ -P.k := Or.inl hx.ne'
    fun_prop
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume

Tactic:
LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: MeasureTheory.LocallyIntegrableOn.add, WeakFEPair.f_modif
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
refine_1 :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
      (𝓝[Ioi 0] x) volume
refine_2 :
  ∀ (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
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume

Tactic:
refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: MeasureTheory.LocallyIntegrableOn.add
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
refine_1 :
  ∀ (s : Set ℝ) (hs : s ∈ 𝓝[Ioi 0] x)
    (hs' : IntegrableOn (mα := Real.measurableSpace) (P.f - fun (x : ℝ) ↦ P.f₀) s volume),
    IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
      (𝓝[Ioi 0] x) volume
⊢ IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume

Tactic:
obtain ⟨s, hs, hs'⟩ := P.hf_int.sub (locallyIntegrableOn_const _) x hx

Premises used: MeasureTheory.locallyIntegrableOn_const, WeakFEPair.hf_int, MeasureTheory.LocallyIntegrableOn.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (mα := Real.measurableSpace) (P.f - fun (x : ℝ) ↦ P.f₀) s volume
⊢ IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume

Tactic:
⟨s, hs, hs'.indicator measurableSet_Ioi⟩

Premises used: MeasureTheory.IntegrableOn.indicator, measurableSet_Ioi, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (mα := Real.measurableSpace) (P.f - fun (x : ℝ) ↦ P.f₀) s volume
⊢ IntegrableAtFilter.{0, u_1} (ε := E) (mα := Real.measurableSpace) (indicator (Ioi 1) fun (x : ℝ) ↦ P.f x - P.f₀)
    (𝓝[Ioi 0] x) volume

Tactic:
exact ⟨s, hs, hs'.indicator measurableSet_Ioi⟩
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
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
⊢ 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

Premises used: WeakFEPair.hf_int, MeasureTheory.LocallyIntegrableOn.sub
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
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:
⟨s, hs, hs'.indicator measurableSet_Ioo⟩

Premises used: MeasureTheory.IntegrableOn.indicator, MeasureTheory.IntegrableAtFilter, measurableSet_Ioo, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
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:
exact ⟨s, hs, hs'.indicator measurableSet_Ioo⟩
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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
inr₁ : ∀ (hx' : x < 1), 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

Tactic:
rcases lt_trichotomy 1 x with hx' | rfl | hx'

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- 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
rwa : 1 / 1 < x
rwa₁ rwa₂ rwa₃ rwa₄ : 1 < x
⊢ 1 / x < 1

Tactic:
rwa [one_div_lt hx one_pos, div_one]

Premises used: one_div_lt, div_one, one_pos
-- 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
⊢ 1 / x < 1

Tactic:
have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]
-- 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
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.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x

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]

Premises used: Iff.mpr, Set.notMem_Ioi, Set.mem_Ioo, WeakFEPair.h_feq, WeakFEPair.g_modif, Set.mem_Ioi, LT.lt.le, zero_add, Pi.add_apply, Set.notMem_Ioo_of_ge, smul_sub, Set.indicator_of_mem, And.intro, div_pos, Set.indicator_of_notMem, add_zero, one_pos, WeakFEPair.f_modif
-- 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
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₀
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₀

Tactic:
simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]

Premises used: Iff.mpr, Real.inv_rpow, LT.lt.le, inv_inv, one_div, one_div_pos, Real.rpow_neg
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
hx : LT.lt (α := ℝ) 0 1
⊢ P.f_modif (1 / 1) = (P.ε * (↑(HPow.hPow (α := ℝ) 1 P.k) : ℂ)) • P.g_modif 1

Tactic:
simp [f_modif, g_modif]

Premises used: WeakFEPair.g_modif, WeakFEPair.f_modif
-- 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' : x < 1
rwa : x < 1 / 1
rwa₁ rwa₂ rwa₃ rwa₄ : x < 1
⊢ 1 < 1 / x

Tactic:
rwa [lt_one_div one_pos hx, div_one]

Premises used: lt_one_div, div_one, one_pos
-- 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' : x < 1
⊢ 1 < 1 / x

Tactic:
have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_one]
-- 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' : x < 1
this : 1 < 1 / x
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₀))
⊢ P.f_modif (1 / x) = (P.ε * (↑(x ^ P.k) : ℂ)) • P.g_modif x

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]

Premises used: Iff.mpr, Set.notMem_Ioi, Set.mem_Ioo, WeakFEPair.h_feq, WeakFEPair.g_modif, Set.mem_Ioi, LT.lt.le, Pi.add_apply, Set.notMem_Ioo_of_ge, Set.indicator_of_mem, And.intro, Set.indicator_of_notMem, WeakFEPair.f_modif
-- 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' : x < 1
this : 1 < 1 / x
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₀))
⊢ (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]

Premises used: LT.lt.le, Real.rpow_neg
-- 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' : x < 1
this : 1 < 1 / x
match_scalars : P.ε * (↑(x ^ P.k) : ℂ) * 1 = P.ε * (↑(x ^ P.k) : ℂ) * 1
match_scalars₁ : -1 = P.ε * (↑(x ^ P.k) : ℂ) * -(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₀))

Tactic:
match_scalars
-- 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' : x < 1
this : 1 < 1 / x
⊢ P.ε * (↑(x ^ P.k) : ℂ) * 1 = P.ε * (↑(x ^ P.k) : ℂ) * 1

Tactic:
field [(rpow_pos_of_pos hx P.k).ne', P.hε]

Premises used: Real.rpow_pos_of_pos, LT.lt.ne', WeakFEPair.hε, WeakFEPair.k
-- 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' : x < 1
this : 1 < 1 / x
⊢ -1 = P.ε * (↑(x ^ P.k) : ℂ) * -(P.ε⁻¹ * (↑(x ^ P.k) : ℂ)⁻¹ * 1)

Tactic:
field [(rpow_pos_of_pos hx P.k).ne', P.hε]

Premises used: Real.rpow_pos_of_pos, LT.lt.ne', WeakFEPair.hε, WeakFEPair.k
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦ x ^ r

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
refine : EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ P.f_modif x - 0
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (x : ℝ) ↦ P.f_modif x - 0) fun (x : ℝ) ↦ x ^ r

Tactic:
refine (P.hf_top r).congr' ?_ (by rfl)

Premises used: Asymptotics.IsBigO.congr', WeakFEPair.hf_top
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
h : ∀ (x : ℝ) (hx : 1 < x), P.f x - P.f₀ = P.f_modif x - 0
⊢ EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ P.f x - P.f₀) fun (x : ℝ) ↦ P.f_modif x - 0

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
r x : ℝ
hx : 1 < x
⊢ P.f x - P.f₀ = P.f_modif x - 0

Tactic:
simp [f_modif, mem_Ioi.mpr hx, notMem_Ioo_of_ge hx.le]

Premises used: Iff.mpr, Set.mem_Ioi, LT.lt.le, Set.notMem_Ioo_of_ge, WeakFEPair.f_modif
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
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
⊢ 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

Tactic:
(hx : 0 < x)
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
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)
⊢ (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:
simp_rw [f_modif, Pi.add_apply]

Premises used: Pi.add_apply, WeakFEPair.f_modif
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
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)
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)
⊢ 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'

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- 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' : x < 1
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
⊢ 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_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]

Premises used: Iff.mpr, Set.notMem_Ioi, Set.mem_Ioo, Iff.not, LT.lt.le, Set.indicator_of_mem, Set.mem_singleton_iff, And.intro, Set.indicator_of_notMem, LT.lt.ne
-- 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' : x < 1
⊢ 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:
abel
-- Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
P : WeakFEPair E
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:
simp [add_comm, sub_eq_add_neg]

Premises used: sub_eq_add_neg, add_comm