awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∏ 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 : ℤ)) 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
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]
-- 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
⊢ ∏ 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 (↑(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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
⊢ ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0
have zero : ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m =
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (↑m : ℤ)) 2 / f 0
Tactic: induction N with
  | zero => simp [sq]
  | succ N ih =>
    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]
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
zero :
  ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (↑m : ℤ)) 2 / f 0
⊢ ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0
have succ : ∀ (N : ℕ)
  (ih : ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m = HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1), f (↑m : ℤ)) 2 / f 0),
  ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
Tactic: induction N with
  | zero => simp [sq]
  | succ N ih =>
    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]
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
N : ℕ
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m
have zero : ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1), f m =
  f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
Tactic: induction N
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
N : ℕ
zero :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * ∏ m ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f m
have succ : ∀ (n : ℕ),
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
      f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m →
    ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1), f m =
      f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
        ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m
Tactic: induction N
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
have zero : ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1, HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1}, f m =
  f (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) * ∏ m ∈ Icc (-(↑0 : ℤ)) (↑0 : ℤ), f m
Tactic: rw [Icc_succ_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
R : Type u_1
inst : CommGroup R
f : ℤ → R
n : ℕ
h :
  ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * ∏ m ∈ Icc (-(↑n : ℤ)) (↑n : ℤ), f m
⊢ ∏ m ∈ Icc (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1), f m =
    f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
      ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m
have succ : HMul.hMul (α := R) (∏ x ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f x)
    (∏ x ∈ {-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1, HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1}, f x) =
  f (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) * f (-HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) *
    ∏ m ∈ Icc (-(↑(n + 1) : ℤ)) (↑(n + 1) : ℤ), f m
Tactic: rw [Icc_succ_succ, prod_union (by simp)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
⊢ ∏ n ∈ Ico (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ), f n / f (n + 1) = f (-(↑(b + 1) : ℤ)) / f (↑(b + 1) : ℤ)
have succ : ∏ x ∈ Ico (-(↑b : ℤ)) (↑b : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1, (↑b : ℤ)}, f x / f (x + 1) =
  f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)
Tactic: simp only [Nat.cast_add_one, Ico_succ_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
α : Type u_1
inst : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
⊢ ∏ x ∈ Ico (-(↑b : ℤ)) (↑b : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1, (↑b : ℤ)}, f x / f (x + 1) =
    f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)
have succ : f (-(↑b : ℤ)) / f (↑b : ℤ) * (f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1 + 1)) *
      f (↑b : ℤ) /
    f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) =
  f (-HAdd.hAdd (α := ℤ) (↑b : ℤ) 1) / f (HAdd.hAdd (α := ℤ) (↑b : ℤ) 1)
Tactic: rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
b : ℕ
α : Type u_1
inst : CommGroup α
f : ℤ → α
⊢ ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
have zero : ∏ n ∈ Ico (-(↑0 : ℤ)) (↑0 : ℤ), f n / f (n + 1) = f (-(↑0 : ℤ)) / f (↑0 : ℤ)
Tactic: induction b with
  | zero => simp
  | succ b ihb =>
    simp only [Nat.cast_add_one, Ico_succ_succ]
    rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]
    simp [mul_comm, mul_div, ← mul_assoc]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Interval (goal)
Goal:
b : ℕ
α : Type u_1
inst : CommGroup α
f : ℤ → α
zero : ∏ n ∈ Ico (-(↑0 : ℤ)) (↑0 : ℤ), f n / f (n + 1) = f (-(↑0 : ℤ)) / f (↑0 : ℤ)
⊢ ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)
have succ : ∀ (b : ℕ) (ihb : ∏ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), f n / f (n + 1) = f (-(↑b : ℤ)) / f (↑b : ℤ)),
  ∏ n ∈ Ico (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ), f n / f (n + 1) = f (-(↑(b + 1) : ℤ)) / f (↑(b + 1) : ℤ)
Tactic: induction b with
  | zero => simp
  | succ b ihb =>
    simp only [Nat.cast_add_one, Ico_succ_succ]
    rw [prod_union (by simp), prod_insert (by grind), prod_singleton, ihb, ← mul_assoc, mul_div]
    simp [mul_comm, mul_div, ← mul_assoc]
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → κ → M
⊢ Subset.{u_2} (α := Set κ) (mulSupport.{u_2, u_3} (M := M) fun (x : κ) ↦ ∏ i ∈ s, f i x) (⋃ i ∈ s, mulSupport (f i))
have simp : ∀ (x : κ), (∀ (x_1 : ι) (x_2 : x_1 ∈ s), f x_1 x = 1) → Eq.{u_3 + 1} (α := M) (∏ i ∈ s, f i x) 1
Tactic: simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, notMem_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ IsSquare.{u_3} (α := M) (∏ i ∈ s, f i)
have rw : ∃ (r : M), ∏ i ∈ s, f i = HPow.hPow (β := ℕ) r 2
Tactic: rw [isSquare_iff_exists_sq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∃ (r : M), ∏ i ∈ s, f i = HPow.hPow (β := ℕ) r 2
have h₁ : ∏ i ∈ s, f i =
  HPow.hPow (α := M) (β := ℕ) (∏ x : ↥s, sorry.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)) 2
Tactic: use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i =
    HPow.hPow (α := M) (β := ℕ) (∏ x : ↥s, ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)) 2
have h₁ : Eq.{u_3 + 1} (α := M) (∏ i : ↥s, f (↑i : ι))
  (∏ x : ↥s,
    sorry.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
      sorry.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2))
Tactic: rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ Eq.{u_3 + 1} (α := M) (∏ i : ↥s, f (↑i : ι))
    (∏ x : ↥s,
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
        ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2))
have h₁ : Eq (α := ↥s → M) (fun (i : ↥s) ↦ f (↑i : ι)) fun (x : ↥s) ↦
  sorry.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
    sorry.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
⊢ Eq (α := ↥s → M) (fun (i : ↥s) ↦ f (↑i : ι)) fun (x : ↥s) ↦
    ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2) *
      ⋯.choose (p := fun (r : M) ↦ f (↑x : ι) = HPow.hPow (β := ℕ) r 2)
have h₁ : ∀ (i : ↥s),
  f (↑i : ι) =
    sorry.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2) *
      sorry.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Lemmas (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ c ∈ s, IsSquare (f c)
i : ↥s
⊢ f (↑i : ι) =
    ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2) *
      ⋯.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)
have h₁ : f (↑i : ι) = HPow.hPow (β := ℕ) (sorry.choose (p := fun (r : M) ↦ f (↑i : ι) = HPow.hPow (β := ℕ) r 2)) 2
Tactic: rw [← @sq]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Pi (goal)
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)
have hi : ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
  Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
    (fun (i : ι) ↦ a i sorry) ∈ Fintype.piFinset (δ := κ) t
Tactic: apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Pi (goal)
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
hi :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)
have hj : ∀ a ∈ Fintype.piFinset (δ := κ) t,
  Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
    fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i
Tactic: apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Pi (goal)
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
hi :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t
hj :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
      fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)
have left_inv : ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
  Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
    (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ (fun (i : ι) ↦ a i sorry) i) = a
Tactic: apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Pi (goal)
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
hi :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t
hj :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
      fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i
left_inv :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ (fun (i : ι) ↦ a i ⋯) i) = a
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)
have right_inv : ∀ a ∈ Fintype.piFinset (δ := κ) t,
  (fun (i : ι) ↦ (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i) i sorry) = a
Tactic: apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Pi (goal)
Goal:
ι : Type u_1
β : Type u_2
inst : CommMonoid β
inst_1 : DecidableEq ι
inst_2 : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → Membership.mem (γ := Finset ι) univ i → κ i) → β
hi :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) ↦ a i ⋯) ∈ Fintype.piFinset (δ := κ) t
hj :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t)
      fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i
left_inv :
  ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
    Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
      (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ (fun (i : ι) ↦ a i ⋯) i) = a
right_inv :
  ∀ a ∈ Fintype.piFinset (δ := κ) t,
    (fun (i : ι) ↦ (fun (i : ι) (x : Membership.mem (γ := Finset ι) univ i) ↦ a i) i ⋯) = a
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ pi (β := κ) univ t, f x)
    (∏ x ∈ Fintype.piFinset (δ := κ) t, f fun (a : ι) (x_1 : Membership.mem (γ := Finset ι) univ a) ↦ x a)
have h : ∀ (a : (a : ι) → Membership.mem (γ := Finset ι) univ a → κ a),
  Membership.mem (γ := Finset ((a : ι) → Membership.mem (γ := Finset ι) univ a → κ a)) (pi (β := κ) univ t) a →
    f a = f fun (a_2 : ι) (x : Membership.mem (γ := Finset ι) univ a_2) ↦ (fun (i : ι) ↦ a i sorry) a_2
Tactic: apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)
have refine_1 : ∀ (a : ι) (ha : a ∈ s),
  Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Piecewise (goal)
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)
have refine_2 : ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
  (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
Tactic: refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_