Theorem: foo (EulerProducts/LSeriesUnique.lean)

State before:
m n : ℕ
z : ℂ
x : ℝ
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
have Hm : (0 : ℝ) ≤ m := m.cast_nonneg
State after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
have Hn : (0 : ℝ) ≤ (n + 1 : ℝ)⁻¹ := by positivity
State after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x
Tactic:
rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]
State after:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Tactic:
congr
State after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹

State before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Tactic:
simp_rw [div_eq_mul_inv]
State after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹

State before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹
Tactic:
rw [show (n + 1 : ℂ)⁻¹ = (n + 1 : ℝ)⁻¹ by
      simp only [ofReal_inv, ofReal_add, ofReal_natCast, ofReal_one],
  show (n + 1 : ℂ) = (n + 1 : ℝ) by norm_cast, show (m : ℂ) = (m : ℝ) by norm_cast,
  mul_cpow_ofReal_nonneg Hm Hn, mul_inv, mul_comm]
State after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

State before:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑↑m ^ ↑x)⁻¹ * ↑(↑n + 1) ^ ↑x = (↑↑m ^ ↑x)⁻¹ * (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Tactic:
congr
State after:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

State before:
case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹
Tactic:
rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp only [ofReal_neg, ofReal_one,
  neg_mul, one_mul], cpow_mul_ofReal_nonneg Hn, Real.rpow_neg_one, inv_inv]
State after:
no goals

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
⊢ 0 ≤ (↑n + 1)⁻¹
Tactic:
positivity
State after:
no goals

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1)⁻¹ = ↑(↑n + 1)⁻¹
Tactic:
simp only [ofReal_inv, ofReal_add, ofReal_natCast, ofReal_one]
State after:
no goals

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑n + 1 = ↑(↑n + 1)
Tactic:
norm_cast
State after:
no goals

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑m = ↑↑m
Tactic:
norm_cast
State after:
no goals

State before:
m n : ℕ
z : ℂ
x : ℝ
Hm : 0 ≤ ↑m
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ -↑x = ↑(-1) * ↑x
Tactic:
simp only [ofReal_neg, ofReal_one,
neg_mul, one_mul]
State after:
no goals