awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
⊢ HSMul.hSMul (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0)⁻¹ ((↑(Fintype.card ι) : M) * f i) = f i
have ha : Ne (α := ℚ≥0) (↑(Fintype.card ι) : ℚ≥0) 0
Tactic: rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
inst_2 : Fintype ι
inst_3 : Nonempty ι
inst_4 : DecidableEq ι
f : ι → M
i : ι
⊢ 𝔼 j : ι, (if j = i then (↑(Fintype.card ι) : M) else 0) * f j = f i
have simp_rw : 𝔼 i_1 : ι, (if i = i_1 then (↑(Fintype.card ι) : M) else 0) * f i_1 = f i
Tactic: simp_rw [@eq_comm _ _ i, expect_boole_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
have rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
Tactic: rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
have rw₁ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
Tactic: rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₁ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
have rw₂ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
Tactic: rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₁ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₂ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
have rw₃ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0) : M)⁻¹ (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
Tactic: rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
rw : HSMul.hSMul (α := ℚ≥0) (β := M) (↑(#s) : ℚ≥0)⁻¹ (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₁ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
rw₂ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0)⁻¹ : M) (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
rw₃ : HMul.hMul (α := M) (↑(↑(#s) : ℚ≥0) : M)⁻¹ (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
⊢ 𝔼 i ∈ s, f i = HDiv.hDiv (α := M) (∑ i ∈ s, f i) (↑(#s) : M)
have rw₄ : HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i) = HMul.hMul (α := M) (↑(#s) : M)⁻¹ (∑ i ∈ s, f i)
Tactic: rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Expect (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Semifield M
inst_1 : CharZero M
s : Finset ι
f : ι → M
a : M
⊢ (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a
have simp_rw : (𝔼 i ∈ s, f i) * a⁻¹ = 𝔼 i ∈ s, f i * a⁻¹
Tactic: simp_rw [div_eq_mul_inv, expect_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Field (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
⊢ (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens
have simp : HDiv.hDiv (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
  HDiv.hDiv (α := ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0)) (↑(Fintype.card β) : ℚ≥0)
Tactic: simp only [dens, ← sum_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Field (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Fintype β
s : Finset α
t : α → Finset β
inst_1 : DecidableEq β
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (↑(Fintype.card β) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0)) (↑(Fintype.card β) : ℚ≥0)
have hab : LE.le (α := ℚ≥0) (↑(#(s.biUnion t)) : ℚ≥0) (∑ i ∈ s, (↑(#(t i)) : ℚ≥0))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
⊢ ∏ i : Fin n, f i = (List.map f (List.finRange n)).prod
have rw : ∏ i : Fin n, f i = (List.ofFn f).prod
Tactic: rw [← List.ofFn_eq_map, prod_ofFn]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
rw : ∏ i : Fin n, f i = (List.ofFn f).prod
⊢ ∏ i : Fin n, f i = (List.map f (List.finRange n)).prod
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ i : Fin n, f i) (∏ i : Fin n, f i)
Tactic: rw [← List.ofFn_eq_map, prod_ofFn]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
have rw : ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) sorry, f i = f x * ∏ i : Fin n, f (x.succAbove i)
Tactic: rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
rw : ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) ⋯, f i = f x * ∏ i : Fin n, f (x.succAbove i)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
have rw₁ : f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i : Fin n, f (x.succAbove i)
Tactic: rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
rw : ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) ⋯, f i = f x * ∏ i : Fin n, f (x.succAbove i)
rw₁ : f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i : Fin n, f (x.succAbove i)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
have rw₂ : f x * ∏ x_1 : Fin n, f ((x.succAboveEmb : (a : Fin n) → Fin (n + 1)) x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
Tactic: rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
rw : ∏ i ∈ Finset.cons x (map x.succAboveEmb univ) ⋯, f i = f x * ∏ i : Fin n, f (x.succAbove i)
rw₁ : f x * ∏ x ∈ map x.succAboveEmb univ, f x = f x * ∏ i : Fin n, f (x.succAbove i)
rw₂ : f x * ∏ x_1 : Fin n, f ((x.succAboveEmb : (a : Fin n) → Fin (n + 1)) x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
⊢ ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)
have rw₃ : f x * ∏ x_1 : Fin n, f (x.succAbove x_1) = f x * ∏ i : Fin n, f (x.succAbove i)
Tactic: rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i : Fin n.succ, cons (α := fun (a : Fin n.succ) ↦ M) x f i = x * ∏ i : Fin n, f i
have simp_rw : HMul.hMul (α := M) (β := M) (cons (α := fun (a : Fin n.succ) ↦ M) x f 0 : M)
    (∏ i : Fin n, cons (α := fun (a : Fin n.succ) ↦ M) x f i.succ : M) =
  x * ∏ i : Fin n, f i
Tactic: simp_rw [prod_univ_succ, cons_zero, cons_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
x : M
f : Fin n → M
simp_rw :
  HMul.hMul (α := M) (β := M) (cons (α := fun (a : Fin n.succ) ↦ M) x f 0 : M)
      (∏ i : Fin n, cons (α := fun (a : Fin n.succ) ↦ M) x f i.succ : M) =
    x * ∏ i : Fin n, f i
⊢ ∏ i : Fin n.succ, cons (α := fun (a : Fin n.succ) ↦ M) x f i = x * ∏ i : Fin n, f i
have simp_rw₁ : x * ∏ i : Fin n, cons (α := fun (a : Fin n.succ) ↦ M) x f i.succ = x * ∏ i : Fin n, f i
Tactic: simp_rw [prod_univ_succ, cons_zero, cons_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 3 → M
⊢ ∏ i : Fin 3, f i = f 0 * f 1 * f 2
have rw : f (castSucc 0) * f (castSucc 1) * f (last 2) = f 0 * f 1 * f 2
Tactic: rw [prod_univ_castSucc, prod_univ_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 4 → M
⊢ ∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3
have rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
Tactic: rw [prod_univ_castSucc, prod_univ_three]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 5 → M
⊢ ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4
have rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (last 4) = f 0 * f 1 * f 2 * f 3 * f 4
Tactic: rw [prod_univ_castSucc, prod_univ_four]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 6 → M
⊢ ∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
have rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (last 5) =
  f 0 * f 1 * f 2 * f 3 * f 4 * f 5
Tactic: rw [prod_univ_castSucc, prod_univ_five]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 7 → M
⊢ ∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
have rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) =
  f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
Tactic: rw [prod_univ_castSucc, prod_univ_six]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 8 → M
⊢ ∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
have rw : f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (castSucc 6) *
    f (last 7) =
  f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
Tactic: rw [prod_univ_castSucc, prod_univ_seven]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (Fin.cast h i)) (∏ i : Fin b, f i)
have subst : ∀ (f : Fin a → M), Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (Fin.cast sorry i)) (∏ i : Fin a, f i)
Tactic: subst h
Cleared hypotheses: b, f, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ i : Fin (a + b), f i = HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i))
have rw : ∏ x : Fin a ⊕ Fin b, f (Equiv.toFun finSumFinEquiv x) =
  HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i))
Tactic: rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
rw :
  ∏ x : Fin a ⊕ Fin b, f (Equiv.toFun finSumFinEquiv x) =
    HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i))
⊢ ∏ i : Fin (a + b), f i = HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i))
have rw₁ : ∀ (x : Fin (a + b)),
  f x = f (Equiv.toFun finSumFinEquiv ((Equiv.symm finSumFinEquiv : (a_1 : Fin (a + b)) → Fin a ⊕ Fin b) x))
Tactic: rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin (a + b), f i) (∏ i : Fin a, f (castAdd b i))
have rw : HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i)) = ∏ i : Fin a, f (castAdd b i)
Tactic: rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
rw : HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i)) = ∏ i : Fin a, f (castAdd b i)
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin (a + b), f i) (∏ i : Fin a, f (castAdd b i))
have rw₁ : HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) 1 = ∏ i : Fin a, f (castAdd b i)
Tactic: rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
rw : HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin b, f (natAdd a i)) = ∏ i : Fin a, f (castAdd b i)
rw₁ : HMul.hMul (α := M) (∏ i : Fin a, f (castAdd b i)) 1 = ∏ i : Fin a, f (castAdd b i)
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin (a + b), f i) (∏ i : Fin a, f (castAdd b i))
have rw₂ : Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (castAdd b i)) (∏ i : Fin a, f (castAdd b i))
Tactic: rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x : M
p : Fin (n + 1) → M
⊢ ∏ j : Fin (n + 1 + 1), (⟨i + 1, h⟩ : Fin (n + 1 + 1)).insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x p j =
    x * ∏ j : Fin (n + 1), p j
have obtain : ∀ (hd : M) (tl : (i : Fin n) → M),
  ∏ j : Fin (n + 1 + 1),
      (⟨i + 1, h⟩ : Fin (n + 1 + 1)).insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x
        (cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl) j =
    x * ∏ j : Fin (n + 1), cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl j
Tactic: obtain ⟨hd, tl, rfl⟩ := exists_cons p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : (i : Fin n) → M
⊢ ∏ j : Fin (n + 1 + 1),
      (⟨i + 1, h⟩ : Fin (n + 1 + 1)).insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x
        (cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl) j =
    x * ∏ j : Fin (n + 1), cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl j
have i_lt : i < n + 1
Tactic: have i_lt := Nat.lt_of_succ_lt_succ h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : (i : Fin n) → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ ∏ j : Fin (n + 1 + 1),
      (⟨i + 1, h⟩ : Fin (n + 1 + 1)).insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x
        (cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl) j =
    x * ∏ j : Fin (n + 1), cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl j
have rw : ∏ j : Fin (n + 1 + 1),
    i_fin.succ.insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x (cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl) j =
  x * ∏ j : Fin (n + 1), cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl j
Tactic: rw [show ⟨i + 1, h⟩ = i_fin.succ from rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : (i : Fin n) → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ ∏ j : Fin (n + 1 + 1),
      i_fin.succ.insertNth (α := fun (a : Fin (n + 1 + 1)) ↦ M) x (cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl) j =
    x * ∏ j : Fin (n + 1), cons (α := fun (i : Fin (n + 1)) ↦ M) hd tl j
have simp : hd * ∏ i : Fin (n + 1), i_fin.insertNth (α := fun (i : Fin (n + 1)) ↦ M) x tl i = x * (hd * ∏ i : Fin n, tl i)
Tactic: simp only [insertNth_succ_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : (i : Fin n) → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ hd * ∏ i : Fin (n + 1), i_fin.insertNth (α := fun (i : Fin (n + 1)) ↦ M) x tl i = x * (hd * ∏ i : Fin n, tl i)
have rw : hd * (x * ∏ j : Fin n, tl j) = x * (hd * ∏ i : Fin n, tl i)
Tactic: rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : (i : Fin n) → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
rw : hd * (x * ∏ j : Fin n, tl j) = x * (hd * ∏ i : Fin n, tl i)
⊢ hd * ∏ i : Fin (n + 1), i_fin.insertNth (α := fun (i : Fin (n + 1)) ↦ M) x tl i = x * (hd * ∏ i : Fin n, tl i)
have rw₁ : x * (hd * ∏ j : Fin n, tl j) = x * (hd * ∏ i : Fin n, tl i)
Tactic: rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
i : Fin (n + 1)
f : Fin (n + 1) → M
⊢ f i * ∏ j : Fin n, i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) f j = ∏ j : Fin (n + 1), f j
have rw : Eq.{u_2 + 1} (α := M)
  (∏ j : Fin (n + 1),
    i.insertNth (α := fun (a : Fin (n + 1)) ↦ M) (f i) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) f) j)
  (∏ j : Fin (n + 1), f j)
Tactic: rw [← prod_insertNth, insertNth_self_removeNth]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
i : Fin (n + 1)
f : Fin (n + 1) → M
rw :
  Eq.{u_2 + 1} (α := M)
    (∏ j : Fin (n + 1),
      i.insertNth (α := fun (a : Fin (n + 1)) ↦ M) (f i) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) f) j)
    (∏ j : Fin (n + 1), f j)
i₁ : Fin (n + 1)
⊢ f i * ∏ j : Fin n, i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) f j = ∏ j : Fin (n + 1), f j
have rw₁ : Eq.{u_2 + 1} (α := M) (∏ j : Fin (n + 1), f j) (∏ j : Fin (n + 1), f j)
Tactic: rw [← prod_insertNth, insertNth_self_removeNth]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ HMul.hMul (α := M) (∏ i : Fin (n + 1), ∏ j : Fin n with i ≤ j.castSucc, f i j)
      (∏ i : Fin (n + 1), ∏ j : Fin n with j.castSucc < i, f i j) =
    HMul.hMul (α := M) (∏ i : Fin n, ∏ j ∈ Ici i, f i.castSucc j) (∏ i : Fin n, ∏ j ∈ Iic i, f i.succ j)
have rw : HMul.hMul (α := M) (∏ i : Fin n, ∏ j : Fin n with i.castSucc ≤ j.castSucc, f i.castSucc j)
      (∏ j : Fin n with last n ≤ j.castSucc, f (last n) j) *
    HMul.hMul (α := M) (∏ j : Fin n with j.castSucc < 0, f 0 j)
      (∏ i : Fin n, ∏ j : Fin n with j.castSucc < i.succ, f i.succ j) =
  HMul.hMul (α := M) (∏ i : Fin n, ∏ j ∈ Ici i, f i.castSucc j) (∏ i : Fin n, ∏ j ∈ Iic i, f i.succ j)
Tactic: rw [Fin.prod_univ_castSucc, Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ HMul.hMul (α := M) (∏ i : Fin n, ∏ j ∈ Ici i, f i.castSucc j) (∏ i : Fin n, ∏ j ∈ Iic i, f i.succ j) =
    HMul.hMul (α := M) (∏ i : Fin n, ∏ j ∈ Ici i, f i.castSucc j) (∏ i : Fin n, ∏ j ∈ Ici i, f j.succ i)
have e_a : Eq.{u_2 + 1} (α := M) (∏ i : Fin n, ∏ j ∈ Iic i, f i.succ j) (∏ i : Fin n, ∏ j ∈ Ici i, f j.succ i)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin n, ∏ j ∈ Iic i, f i.succ j) (∏ i : Fin n, ∏ j ∈ Ici i, f j.succ i)
have e_a : ∀ (x y : Fin n),
  Membership.mem (γ := Finset (Fin n)) univ x ∧ y ∈ Iic x ↔ x ∈ Ici y ∧ Membership.mem (γ := Finset (Fin n)) univ y
Tactic: apply Finset.prod_comm'
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
⊢ Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin (n + 1), HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even (n + 1) then 0 else 1)
have succ : (if Even n then 0 else 1) + HPow.hPow (α := R) (-1) n = if Even n then 1 else 0
Tactic: simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
⊢ (if Even n then 0 else 1) + HPow.hPow (α := R) (-1) n = if Even n then 1 else 0
have pos : ∀ (h : Even n), 0 + HPow.hPow (α := R) (-1) n = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
R : Type u_3
inst : Ring R
n : ℕ
IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)
pos : ∀ (h : Even n), 0 + HPow.hPow (α := R) (-1) n = 1
⊢ (if Even n then 0 else 1) + HPow.hPow (α := R) (-1) n = if Even n then 1 else 0
have neg : ∀ (h : ¬Even n), 1 + HPow.hPow (α := R) (-1) n = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
R : Type u_3
inst : Ring R
m : ℕ
⊢ Eq.{u_3 + 1} (α := R) (∑ n : Fin m, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even m then 0 else 1)
have zero : Eq.{u_3 + 1} (α := R) (∑ n : Fin 0, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even (α := ℕ) 0 then 0 else 1)
Tactic: induction m with
  | zero => simp
  | succ n IH =>
    simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
R : Type u_3
inst : Ring R
m : ℕ
zero : Eq.{u_3 + 1} (α := R) (∑ n : Fin 0, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even (α := ℕ) 0 then 0 else 1)
⊢ Eq.{u_3 + 1} (α := R) (∑ n : Fin m, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even m then 0 else 1)
have succ : ∀ (n : ℕ) (IH : Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin n, HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even n then 0 else 1)),
  Eq.{u_3 + 1} (α := R) (∑ n_1 : Fin (n + 1), HPow.hPow (α := R) (-1) (↑n_1 : ℕ)) (if Even (n + 1) then 0 else 1)
Tactic: induction m with
  | zero => simp
  | succ n IH =>
    simp only [Fin.sum_univ_castSucc, Fin.val_castSucc, IH, Fin.val_last, Nat.even_add_one, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : Monoid M
n : ℕ
f : Fin (n + 1) → M
j : Fin (n + 1)
⊢ partialProd f j.succ = f 0 * partialProd (tail (α := fun (i : Fin (n + 1)) ↦ M) f) j
have simp : f 0 * List.prod (List.take (↑j : ℕ) (List.ofFn (n := n) fun (i : Fin n) ↦ f i.succ)) =
  f 0 * (List.take (↑j : ℕ) (List.ofFn (tail (α := fun (i : Fin (n + 1)) ↦ M) f))).prod
Tactic: simp [partialProd]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : ℕ
G : Type u_3
inst : Group G
f : Fin (n + 1) → G
x_1 : Fin (n + 1)
x : Fin n
hx :
  HSMul.hSMul (β := (i : Fin (n + 1)) → G) (f 0) (partialProd fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ)
      x.castSucc =
    f x.castSucc
⊢ HSMul.hSMul (β := (i : Fin (n + 1)) → G) (f 0) (partialProd fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ =
    f x.succ
have simp : f 0 * partialProd (fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ
Tactic: simp only [Pi.smul_apply, smul_eq_mul] at hx ⊢