-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
lemma hf_modif_int :
    LocallyIntegrableOn P.f_modif (Ioi 0)

Proof state:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableOn (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioo 0 1 ∩ s) volume

Tactic:
exact hs'.mono_set Set.inter_subset_right

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) x

Tactic:
refine (continuousAt_const.mul ?_).smul continuousAt_const

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt (fun x => ↑(x ^ (-P.k))) x

Proof state:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ IntegrableAtFilter ((Ioi 1).indicator fun x => P.f x - P.f₀) (𝓝[Ioi 0] x) volume

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

Result:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableAtFilter ((Ioi 1).indicator fun x => P.f x - P.f₀) (𝓝[Ioi 0] x) volume

Proof state:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableOn ((Ioi 1).indicator fun x => P.f x - P.f₀) s volume

Tactic:
rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioi, IntegrableOn,
  Measure.restrict_restrict measurableSet_Ioi, ← IntegrableOn]

Result:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableOn (fun x => P.f x - P.f₀) (Ioi 1 ∩ s) volume

Proof state:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableOn ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume

Tactic:
rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioo, IntegrableOn,
  Measure.restrict_restrict measurableSet_Ioo, ← IntegrableOn]

Result:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableOn (fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioo 0 1 ∩ s) volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
⊢ LocallyIntegrableOn P.f_modif (Ioi 0) volume

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

Result:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ IntegrableAtFilter ((Ioi 1).indicator fun x => P.f x - P.f₀) (𝓝[Ioi 0] x) volume

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ IntegrableAtFilter ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume

Proof state:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableAtFilter ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (𝓝[Ioi 0] x) volume

Tactic:
refine ⟨s, hs, ?_⟩

Result:
case refine_2.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume
⊢ IntegrableOn ((Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) s volume

Proof state:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableAtFilter ((Ioi 1).indicator fun x => P.f x - P.f₀) (𝓝[Ioi 0] x) volume

Tactic:
refine ⟨s, hs, ?_⟩

Result:
case refine_1.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
this : LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
s : Set ℝ
hs : s ∈ 𝓝[Ioi 0] x
hs' : IntegrableOn (P.f - fun x => ?m.84581) s volume
⊢ IntegrableOn ((Ioi 1).indicator fun x => P.f x - P.f₀) s volume

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0)

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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ ContinuousAt (fun x => ↑(x ^ (-P.k))) x

Tactic:
exact continuous_ofReal.continuousAt.comp (continuousAt_rpow_const _ _ (Or.inl hx.ne'))

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ LocallyIntegrableOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0) volume

Tactic:
refine ContinuousOn.locallyIntegrableOn ?_ measurableSet_Ioi

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ContinuousOn (fun x => (P.ε * ↑(x ^ (-P.k))) • P.g₀) (Ioi 0)