-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0
succ :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑N : ℤ) (↑1 : ℤ)) (HAdd.hAdd (α := ℤ) (↑N : ℤ) (↑1 : ℤ)), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₁ :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₂ :
  ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1, HAdd.hAdd (α := ℤ) (↑N : ℤ) 1}, f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₃ :
  HMul.hMul (α := α) (∏ x ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f x)
      (∏ x ∈ {-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1, HAdd.hAdd (α := ℤ) (↑N : ℤ) 1}, f x) =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₄ :
  (∏ x ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f x) * (f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₅ :
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0 *
      (f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
succ₆ :
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0 *
      (f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) =
    HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (↑(N + 1) : ℤ)) 2 / f 0
succ₇ :
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0 *
      (f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) =
    HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (↑(N + 1) : ℤ)) 2 / f 0
succ₈ :
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0 *
      HPow.hPow (β := ℕ) (f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 =
    HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (↑(N + 1) : ℤ)) 2 / f 0
succ₉ :
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 *
        HPow.hPow (β := ℕ) (f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 /
      f 0 =
    HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (↑(N + 1) : ℤ)) 2 / f 0
succ₁₀ :
  HPow.hPow (β := ℕ) ((∏ m ∈ range (N + 1), f (↑m : ℤ)) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 / f 0 =
    HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (↑(N + 1) : ℤ)) 2 / f 0
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have succ₁₁ : HPow.hPow (β := ℕ) ((∏ m ∈ range (N + 1), f (↑m : ℤ)) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 / f 0 =
  HPow.hPow (β := ℕ) ((∏ x ∈ range (N + 1), f (↑x : ℤ)) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 / f 0
Tactic: rw [Nat.cast_add, Nat.cast_one, Icc_succ_succ, prod_union (by simp), prod_pair (by lia), ih,
      prod_range_succ _ (N + 1), hf, ← pow_two, div_mul_eq_mul_div, ← mul_pow, Nat.cast_succ]