awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 5 → M
⊢ 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:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 6 → M
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
⊢ ∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
rw [prod_univ_castSucc, prod_univ_five]

Premises used: Fin.prod_univ_five, Fin.prod_univ_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 6 → M
⊢ 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:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 7 → M
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
⊢ ∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
rw [prod_univ_castSucc, prod_univ_six]

Premises used: Fin.prod_univ_castSucc, Fin.prod_univ_six
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 7 → M
⊢ 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:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 8 → M
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
⊢ ∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Tactic:
rw [prod_univ_castSucc, prod_univ_seven]

Premises used: Fin.prod_univ_castSucc, Fin.prod_univ_seven
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
f : Fin 8 → M
⊢ 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:
rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
x : M
⊢ ∏ _i : Fin n, x = x ^ n

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin b → M
h : a = b
subst : ∀ (f : Fin a → M), Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (Fin.cast ⋯ i)) (∏ i : Fin a, f i)
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (Fin.cast h i)) (∏ i : Fin b, f i)

Tactic:
subst h
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
a : ℕ
f : Fin a → M
⊢ Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (Fin.cast ⋯ i)) (∏ i : Fin a, f i)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Fin
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))
rw₁ :
  ∀ (x : Fin (a + b)),
    f x = f (Equiv.toFun finSumFinEquiv ((Equiv.symm finSumFinEquiv : (a_1 : Fin (a + b)) → Fin a ⊕ Fin b) x))
⊢ ∏ i : Fin (a + b), f i = 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)]

Premises used: Fintype.prod_equiv, Equiv.toFun, finSumFinEquiv, Equiv.symm
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ 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:
apply Fintype.prod_sum_type

Premises used: Fintype.prod_sum_type
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (Equiv.toFun finSumFinEquiv ((Equiv.symm finSumFinEquiv : (a_1 : Fin (a + b)) → Fin a ⊕ Fin b) x))

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.toFun_as_coe
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
rw₂ rw₃ : Eq.{u_2 + 1} (α := M) (∏ i : Fin a, f (castAdd b 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))

Tactic:
rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]

Premises used: Fintype.prod_eq_one, Fin.prod_univ_add, mul_one
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
h : 0 < n + 1
x : M
p : Fin n → M
⊢ ∏ j : Fin (n + 1), (⟨0, h⟩ : Fin (n + 1)).insertNth (α := fun (a : Fin (n + 1)) ↦ M) x p j = x * ∏ j : Fin n, p j

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
i : ℕ
h : i < HAdd.hAdd (α := ℕ) 0 1
x : M
p : Fin 0 → M
⊢ ∏ j : Fin (0 + 1),
      (⟨i, h⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)).insertNth (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ M) x p j =
    x * ∏ j : Fin 0, p j

Tactic:
simp [fin_one_eq_zero ⟨i, h⟩]

Premises used: Fin.fin_one_eq_zero, Fin.mk
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x : M
p : Fin (n + 1) → M
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
⊢ ∏ 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

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons p

Premises used: Fin.exists_cons, rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
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 < n + 1

Tactic:
have i_lt := Nat.lt_of_succ_lt_succ h
-- Module: Mathlib.Algebra.BigOperators.Fin
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 :
  ∏ 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
⊢ ∏ 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:
rw [show ⟨i + 1, h⟩ = i_fin.succ from rfl]

Premises used: rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
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⟩
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)
⊢ ∏ 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:
simp only [insertNth_succ_cons, prod_cons]

Premises used: Fin.insertNth_succ_cons, Fin.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
rw₁ rw₂ : x * (hd * ∏ 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)

Tactic:
rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
i : Fin (n + 1)
x : M
p : Fin n → M
⊢ ∏ j : Fin (n + 1), i.insertNth (α := fun (a : Fin (n + 1)) ↦ M) x p j = x * ∏ j : Fin n, p j

Tactic:
prod_insertNth_go n i.val i.isLt x p

Premises used: Fin.isLt, _private.0.Fin.prod_insertNth_go, Fin.val
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) (∏ j : Fin (n + 1), f j) (∏ j : Fin (n + 1), f j)
⊢ f i * ∏ j : Fin n, i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) f j = ∏ j : Fin (n + 1), f j

Tactic:
rw [← prod_insertNth, insertNth_self_removeNth]

Premises used: Fin.insertNth_self_removeNth, Fin.prod_insertNth
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Icc (Fin.cast h a) (Fin.cast h b), f i) (∏ i ∈ Icc a b, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Icc]

Premises used: Fin.map_finCongr_Icc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ico (Fin.cast h a) (Fin.cast h b), f i) (∏ i ∈ Ico a b, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Ico]

Premises used: Fin.map_finCongr_Ico
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioc (Fin.cast h a) (Fin.cast h b), f i) (∏ i ∈ Ioc a b, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Ioc]

Premises used: Fin.map_finCongr_Ioc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioo (Fin.cast h a) (Fin.cast h b), f i) (∏ i ∈ Ioo a b, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Ioo]

Premises used: Fin.map_finCongr_Ioo
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ uIcc (Fin.cast h a) (Fin.cast h b), f i) (∏ i ∈ uIcc a b, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_uIcc]

Premises used: Fin.map_finCongr_uIcc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ici (Fin.cast h a), f i) (∏ i ∈ Ici a, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Ici]

Premises used: Fin.map_finCongr_Ici
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioi (Fin.cast h a), f i) (∏ i ∈ Ioi a, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Ioi]

Premises used: Fin.map_finCongr_Ioi
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iic (Fin.cast h a), f i) (∏ i ∈ Iic a, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Iic]

Premises used: Fin.map_finCongr_Iic
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iio (Fin.cast h a), f i) (∏ i ∈ Iio a, f (Fin.cast h i))

Tactic:
simp [← map_finCongr_Iio]

Premises used: Fin.map_finCongr_Iio
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Icc (castLE h a) (castLE h b), f i) (∏ i ∈ Icc a b, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Icc]

Premises used: Fin.map_castLEEmb_Icc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ico (castLE h a) (castLE h b), f i) (∏ i ∈ Ico a b, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Ico]

Premises used: Fin.map_castLEEmb_Ico
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioc (castLE h a) (castLE h b), f i) (∏ i ∈ Ioc a b, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Ioc]

Premises used: Fin.map_castLEEmb_Ioc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioo (castLE h a) (castLE h b), f i) (∏ i ∈ Ioo a b, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Ioo]

Premises used: Fin.map_castLEEmb_Ioo
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ uIcc (castLE h a) (castLE h b), f i) (∏ i ∈ uIcc a b, f (castLE h i))

Tactic:
simp [← map_castLEEmb_uIcc]

Premises used: Fin.map_castLEEmb_uIcc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iic (castLE h a), f i) (∏ i ∈ Iic a, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Iic]

Premises used: Fin.map_castLEEmb_Iic
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
h : n ≤ m
f : Fin m → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iio (castLE h a), f i) (∏ i ∈ Iio a, f (castLE h i))

Tactic:
simp [← map_castLEEmb_Iio]

Premises used: Fin.map_castLEEmb_Iio
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Icc (castAdd m a) (castAdd m b), f i) (∏ i ∈ Icc a b, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Icc]

Premises used: Fin.map_castAddEmb_Icc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ico (castAdd m a) (castAdd m b), f i) (∏ i ∈ Ico a b, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Ico]

Premises used: Fin.map_castAddEmb_Ico
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioc (castAdd m a) (castAdd m b), f i) (∏ i ∈ Ioc a b, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Ioc]

Premises used: Fin.map_castAddEmb_Ioc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioo (castAdd m a) (castAdd m b), f i) (∏ i ∈ Ioo a b, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Ioo]

Premises used: Fin.map_castAddEmb_Ioo
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ uIcc (castAdd m a) (castAdd m b), f i) (∏ i ∈ uIcc a b, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_uIcc]

Premises used: Fin.map_castAddEmb_uIcc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iic (castAdd m a), f i) (∏ i ∈ Iic a, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Iic]

Premises used: Fin.map_castAddEmb_Iic
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n m : ℕ
f : Fin (n + m) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iio (castAdd m a), f i) (∏ i ∈ Iio a, f (castAdd m i))

Tactic:
simp [← map_castAddEmb_Iio]

Premises used: Fin.map_castAddEmb_Iio
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Icc a.castSucc b.castSucc, f i) (∏ i ∈ Icc a b, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Icc]

Premises used: Fin.map_castSuccEmb_Icc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ico a.castSucc b.castSucc, f i) (∏ i ∈ Ico a b, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Ico]

Premises used: Fin.map_castSuccEmb_Ico
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioc a.castSucc b.castSucc, f i) (∏ i ∈ Ioc a b, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Ioc]

Premises used: Fin.map_castSuccEmb_Ioc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioo a.castSucc b.castSucc, f i) (∏ i ∈ Ioo a b, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Ioo]

Premises used: Fin.map_castSuccEmb_Ioo
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ uIcc a.castSucc b.castSucc, f i) (∏ i ∈ uIcc a b, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_uIcc]

Premises used: Fin.map_castSuccEmb_uIcc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iic a.castSucc, f i) (∏ i ∈ Iic a, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Iic]

Premises used: Fin.map_castSuccEmb_Iic
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Iio a.castSucc, f i) (∏ i ∈ Iio a, f i.castSucc)

Tactic:
simp [← map_castSuccEmb_Iio]

Premises used: Fin.map_castSuccEmb_Iio
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Icc a.succ b.succ, f i) (∏ i ∈ Icc a b, f i.succ)

Tactic:
simp [← map_succEmb_Icc]

Premises used: Fin.map_succEmb_Icc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ico a.succ b.succ, f i) (∏ i ∈ Ico a b, f i.succ)

Tactic:
simp [← map_succEmb_Ico]

Premises used: Fin.map_succEmb_Ico
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioc a.succ b.succ, f i) (∏ i ∈ Ioc a b, f i.succ)

Tactic:
simp [← map_succEmb_Ioc]

Premises used: Fin.map_succEmb_Ioc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioo a.succ b.succ, f i) (∏ i ∈ Ioo a b, f i.succ)

Tactic:
simp [← map_succEmb_Ioo]

Premises used: Fin.map_succEmb_Ioo
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ uIcc a.succ b.succ, f i) (∏ i ∈ uIcc a b, f i.succ)

Tactic:
simp [← map_succEmb_uIcc]

Premises used: Fin.map_succEmb_uIcc
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ici a.succ, f i) (∏ i ∈ Ici a, f i.succ)

Tactic:
simp [← map_succEmb_Ici]

Premises used: Fin.map_succEmb_Ici
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioi a.succ, f i) (∏ i ∈ Ioi a, f i.succ)

Tactic:
simp [← map_succEmb_Ioi]

Premises used: Fin.map_succEmb_Ioi
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ Ioi 0, f i) (∏ j : Fin n, f j.succ)

Tactic:
simp [Ioi_zero_eq_map]

Premises used: Fin.Ioi_zero_eq_map
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∏ i : Fin (n + 1), ∏ j : Fin n, f i j =
    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)

Tactic:
simp only [← Finset.prod_mul_distrib, ← not_le, Finset.prod_filter_mul_prod_filter_not]

Premises used: not_le, Finset.prod_mul_distrib, Finset.prod_filter_mul_prod_filter_not
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
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)
⊢ 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)

Tactic:
rw [Fin.prod_univ_castSucc, Fin.prod_univ_succ]

Premises used: Fin.prod_univ_castSucc, Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ 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:
simp [Finset.filter_le_eq_Ici, Finset.filter_ge_eq_Iic]

Premises used: Finset.filter_ge_eq_Iic, Finset.filter_le_eq_Ici
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
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)
⊢ 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)

Tactic:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
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
⊢ 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:
apply Finset.prod_comm'

Premises used: Finset.prod_comm'
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∀ (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:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
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 ∈ Ici i, f j.succ i) =
    ∏ i : Fin n, ∏ j ∈ Ici i, f i.castSucc j * f j.succ i

Tactic:
simp only [Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : ℕ
R : Type u_3
inst : CommSemiring R
a b : R
⊢ ∑ s : Finset (Fin n), a ^ #s * b ^ (n - #s) = (a + b) ^ n

Tactic:
simpa using Fintype.sum_pow_mul_eq_add_pow (Fin n) a b

Premises used: Fintype.sum_pow_mul_eq_add_pow, Fin
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
R : Type u_3
inst : Ring R
⊢ Eq.{u_3 + 1} (α := R) (∑ n : Fin 0, HPow.hPow (α := R) (-1) (↑n : ℕ)) (if Even (α := ℕ) 0 then 0 else 1)

Tactic:
simp