-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
lemma hf_modif_FE (x : ℝ) (hx : 0 < x) :
    P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Tactic:
rw [f_modif, Pi.add_apply, indicator_of_not_mem (not_mem_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_not_mem
  (not_mem_Ioo_of_ge hx'.le), add_zero, P.h_feq _ hx, smul_sub]

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Tactic:
rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this),
  indicator_of_not_mem (not_mem_Ioo_of_ge this.le), add_zero, g_modif, Pi.add_apply,
  indicator_of_not_mem (not_mem_Ioi.mpr hx'.le),
  indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩), zero_add, P.h_feq _ hx, smul_sub]

Result:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k)) • (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Tactic:
have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ 1 < 1 / x

Tactic:
rwa [lt_one_div one_pos hx, div_one]

Result:
no goals

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k)) • (P.ε⁻¹ * ↑(x ^ (-P.k))) • P.f₀

Tactic:
simp_rw [rpow_neg hx.le, ← mul_smul]

Result:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k) * (P.ε⁻¹ * ↑(x ^ P.k)⁻¹)) • P.f₀

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Tactic:
have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_one]

Result:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Proof state:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k) * (P.ε⁻¹ * ↑(x ^ P.k)⁻¹)) • P.f₀

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

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

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

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ P.f_modif (1 / 1) = (P.ε * ↑(1 ^ P.k)) • P.g_modif 1

case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ 1 / x < 1

Tactic:
rwa [one_div_lt hx one_pos, div_one]

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀

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

Result:
no goals

Proof state:
case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ P.f_modif (1 / 1) = (P.ε * ↑(1 ^ P.k)) • P.g_modif 1

Tactic:
simp [f_modif, g_modif]

Result:
no goals