Theorem: riemannZeta_ne_zero_of_one_le_re (EulerProducts/PNT.lean)

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
⊢ ζ z ≠ 0
Tactic:
refine hz'.eq_or_lt.elim (fun h Hz ↦ ?_) riemannZeta_ne_zero_of_one_lt_re
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ False
Tactic:
have hz₀ : z.im ≠ 0 := by
  rw [← re_add_im z, ← h, ofReal_one] at hz
  simpa only [ne_eq, add_right_eq_self, mul_eq_zero, ofReal_eq_zero, I_ne_zero, or_false]
    using hz
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ False
Tactic:
have hzeq : z = 1 + I * z.im := by
  rw [mul_comm I, ← re_add_im z, ← h]
  push_cast
  simp only [add_im, one_im, mul_im, ofReal_re, I_im, mul_one, ofReal_im, I_re, mul_zero,
    add_zero, zero_add]
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
⊢ False
Tactic:
have H₀ : (fun _ : ℝ ↦ (1 : ℝ)) =O[𝓝[>] 0]
    (fun x ↦ ζ (1 + x) ^ 3 * ζ (1 + x + I * z.im) ^ 4 * ζ (1 + x + 2 * I * z.im)) :=
  IsBigO.of_bound' <| eventually_nhdsWithin_of_forall
    fun _ hx ↦ (norm_one (α := ℝ)).symm ▸ (norm_zeta_product_ge_one hx z.im).le
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
⊢ False
Tactic:
have H := (riemannZeta_isBigO_near_one_horizontal.pow 3).mul
  ((riemannZeta_isBigO_near_root_horizontal hz₀ (hzeq ▸ Hz)).pow 4)|>.mul <|
  riemannZeta_isBigO_of_ne_one_horizontal <| mul_ne_zero two_ne_zero hz₀
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
conv at H => enter [3, x]; rw [help]
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
conv at H =>
  enter [2, x]; rw [show 1 + x + I * ↑(2 * z.im) = 1 + x + 2 * I * z.im by simp; ring]
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
replace H := (H₀.trans H).norm_right
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False
Tactic:
simp only [norm_eq_abs, abs_ofReal] at H
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ False

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ False
Tactic:
refine isLittleO_irrefl ?_ <| H.of_abs_right.trans_isLittleO <|
  isLittleO_id_nhdsWithin (Set.Ioi 0)
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ ∃ᶠ (x : ℝ) in 𝓝[>] 0, 1 ≠ 0

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ ∃ᶠ (x : ℝ) in 𝓝[>] 0, 1 ≠ 0
Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, frequently_true_iff_neBot]
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ (𝓝[>] 0).NeBot

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ (𝓝[>] 0).NeBot
Tactic:
exact mem_closure_iff_nhdsWithin_neBot.mp <| closure_Ioi (0 : ℝ) ▸ Set.left_mem_Ici
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0
Tactic:
rw [← re_add_im z, ← h, ofReal_one] at hz
State after:
z : ℂ
hz : 1 + ↑z.im * I ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0

State before:
z : ℂ
hz : 1 + ↑z.im * I ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0
Tactic:
simpa only [ne_eq, add_right_eq_self, mul_eq_zero, ofReal_eq_zero, I_ne_zero, or_false]
  using hz
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ z = 1 + I * ↑z.im
Tactic:
rw [mul_comm I, ← re_add_im z, ← h]
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ ↑1 + ↑z.im * I = 1 + ↑(↑1 + ↑z.im * I).im * I

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ ↑1 + ↑z.im * I = 1 + ↑(↑1 + ↑z.im * I).im * I
Tactic:
push_cast
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ 1 + ↑z.im * I = 1 + ↑(1 + ↑z.im * I).im * I

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ 1 + ↑z.im * I = 1 + ↑(1 + ↑z.im * I).im * I
Tactic:
simp only [add_im, one_im, mul_im, ofReal_re, I_im, mul_one, ofReal_im, I_re, mul_zero,
  add_zero, zero_add]
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Tactic:
rcases eq_or_ne x 0 with rfl | h
State after:
case inl
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0

case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x

State before:
case inl
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0
Tactic:
rw [ofReal_zero, zero_pow (by norm_num), mul_zero, mul_one]
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ 4 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Tactic:
field_simp [h]
State after:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ ↑x ^ 4 = ↑x * ↑x ^ 3

State before:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ ↑x ^ 4 = ↑x * ↑x ^ 3
Tactic:
ring
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ 1 + ↑x + I * ↑(2 * z.im) = 1 + ↑x + 2 * I * ↑z.im
Tactic:
simp
State after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ I * (2 * ↑z.im) = 2 * I * ↑z.im

State before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ I * (2 * ↑z.im) = 2 * I * ↑z.im
Tactic:
ring
State after:
no goals