awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
⊢ mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
have cons : j ∉ t i ∩ ⋃ x ∈ s, t x
Tactic: rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
⊢ mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
have cons : mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
have cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
have cons₂ : (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₂ : (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
have cons₃ : (t i).mulIndicator f j * mulIndicator (⋃ x ∈ s, t x) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₂ : (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₃ :
  (t i).mulIndicator f j * mulIndicator (⋃ x ∈ s, t x) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
have cons₄ : j ∉ t i ∩ ⋃ x ∈ s, t x
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s : Set ι).PairwiseDisjoint t ∧ ∀ j ∈ (↑s : Set ι), Disjoint (t i) (t j)
j : κ
cons : mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₁ : mulIndicator (⋃ i_1 ∈ insert i s, t i_1) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₂ : (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₃ :
  (t i).mulIndicator f j * mulIndicator (⋃ x ∈ s, t x) f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
cons₄ : j ∉ t i ∩ ⋃ x ∈ s, t x
⊢ mulIndicator (⋃ i_1 ∈ Finset.cons i s hi, t i_1) f j = ∏ i ∈ Finset.cons i s hi, (t i).mulIndicator f j
have cons₅ : (t i).mulIndicator f j * (fun (a : κ) ↦ (∏ i ∈ s, (t i).mulIndicator f a : β)) j =
  (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j
Tactic: classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
hs : (↑s : Set ι).PairwiseDisjoint t
⊢ mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
have empty : ∀ (hs : (↑∅ : Set ι).PairwiseDisjoint t),
  mulIndicator (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) f = fun (a : κ) ↦
    ∏ i ∈ ∅, (t i).mulIndicator f a
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih =>
    ext j
    rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
    classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
hs : (↑s : Set ι).PairwiseDisjoint t
empty :
  ∀ (hs : (↑∅ : Set ι).PairwiseDisjoint t),
    mulIndicator (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), t i) f = fun (a : κ) ↦
      ∏ i ∈ ∅, (t i).mulIndicator f a
⊢ mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a
have cons : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (ih :
    ∀ (hs : (↑s : Set ι).PairwiseDisjoint t),
      mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) ↦ ∏ i ∈ s, (t i).mulIndicator f a)
  (hs : (↑(cons i s hi) : Set ι).PairwiseDisjoint t),
  mulIndicator (⋃ i_1 ∈ cons i s hi, t i_1) f = fun (a : κ) ↦ ∏ i ∈ cons i s hi, (t i).mulIndicator f a
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons i s hi ih =>
    ext j
    rw [coe_cons, Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)] at hs
    classical
    rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_notMem_inter, ih hs.1]
    exact (Set.disjoint_iff.mp (Set.disjoint_iUnion₂_right.mpr hs.2) ·)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Group.Finset.Indicator (goal)
Goal:
ι : Type u_1
κ : Type u_2
β : Type u_4
inst : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
h : (↑s : Set ι).PairwiseDisjoint t
x : κ
⊢ mulIndicator (⋃ i ∈ s, t i) f x = ∏ i ∈ s, (t i).mulIndicator f x
have rw : Eq.{u_4 + 1} (α := β) ((fun (a : κ) ↦ (∏ i ∈ s, (t i).mulIndicator f a : β)) x) (∏ i ∈ s, (t i).mulIndicator f x)
Tactic: rw [mulIndicator_biUnion s t h]
-- 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
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have 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
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
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have 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
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
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have 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
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
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have 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
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
⊢ ∏ m ∈ Icc (-(↑(N + 1) : ℤ)) (↑(N + 1) : ℤ), f m =
    HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 2 / f 0
have 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
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
⊢ ∏ 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 / f 0 *
    (f (-HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) * f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) =
  HPow.hPow (α := α) (β := ℕ) (∏ m ∈ range (N + 1 + 1), f (↑m : ℤ)) 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
⊢ ∏ 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 / 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
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
⊢ ∏ 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 / 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
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
⊢ ∏ 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 / f 0 *
    HPow.hPow (β := ℕ) (f (HAdd.hAdd (α := ℤ) (↑N : ℤ) 1)) 2 =
  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]