awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin m, n i)
revert :
  ∀ (a : Fin (∏ i : Fin m, n i)),
    (fun (f : (i : Fin m) → Fin (n i)) ↦
          (⟨∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j), ⋯⟩ : Fin (∏ i : Fin m, n i)))
        ((fun (a : Fin (∏ i : Fin m, n i)) (b : Fin m) ↦
            (⟨((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b, ⋯⟩ : Fin (n b)))
          a) =
      a
⊢ (fun (f : (i : Fin m) → Fin (n i)) ↦
        (⟨∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j), ⋯⟩ : Fin (∏ i : Fin m, n i)))
      ((fun (a : Fin (∏ i : Fin m, n i)) (b : Fin m) ↦
          (⟨((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b, ⋯⟩ : Fin (n b)))
        a) =
    a

Tactic:
revert a
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i : Fin m, n i)),
    ⟨∑ i : Fin m, ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) % n i * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j),
        ⋯⟩ =
      a

Tactic:
Fin.consInduction ?_ ?_ n

Premises used: Fin.consInduction
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
refine_1 :
  ∀ (a : Fin (∏ i : Fin 0, i.elim0)),
    ⟨∑ i : Fin 0,
          ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), (Fin.castLE ⋯ j).elim0) % i.elim0 *
            ∏ j : Fin (↑i : ℕ), (Fin.castLE ⋯ j).elim0,
        ⋯⟩ =
      a
refine_2 :
  ∀ {n : ℕ} (x₀ : ℕ) (x : Fin n → ℕ),
    (∀ (a : Fin (∏ i : Fin n, x i)),
        ⟨∑ i : Fin n,
              ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), x (Fin.castLE ⋯ j)) % x i * ∏ j : Fin (↑i : ℕ), x (Fin.castLE ⋯ j),
            ⋯⟩ =
          a) →
      ∀ (a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x i)),
        ⟨∑ i : Fin (n + 1),
              HMod.hMod (β := ℕ)
                  ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x (Fin.castLE ⋯ j))
                  (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x i : ℕ) *
                ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x (Fin.castLE ⋯ j),
            ⋯⟩ =
          a
⊢ ∀ (a : Fin (∏ i : Fin m, n i)),
    ⟨∑ i : Fin m, ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) % n i * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j),
        ⋯⟩ =
      a

Tactic:
refine Fin.consInduction ?_ ?_ n
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin 0, i.elim0)
⊢ Subsingleton (Fin (∏ i : Fin 0, i.elim0))

Tactic:
have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin 0, i.elim0)
this : Subsingleton (Fin (∏ i : Fin 0, i.elim0))
⊢ ⟨∑ i : Fin 0,
        ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), (Fin.castLE ⋯ j).elim0) % i.elim0 * ∏ j : Fin (↑i : ℕ), (Fin.castLE ⋯ j).elim0,
      ⋯⟩ =
    a

Tactic:
subsingleton
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
ih :
  ∀ (a : Fin (∏ i : Fin n, xs i)),
    ⟨∑ i : Fin n, ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), xs (Fin.castLE ⋯ j)) % xs i * ∏ j : Fin (↑i : ℕ), xs (Fin.castLE ⋯ j),
        ⋯⟩ =
      a
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
⊢ ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i

Tactic:
simp_rw [Fin.forall_iff, Fin.ext_iff] at ih

Premises used: Fin.ext_iff, Fin.forall_iff
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
refine_2 :
  (↑(⟨∑ i : Fin (n + 1),
              HMod.hMod (β := ℕ)
                  ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j))
                  (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i : ℕ) *
                ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j),
            ⋯⟩ :
          Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)) :
      ℕ) =
    (↑a : ℕ)
⊢ ⟨∑ i : Fin (n + 1),
        HMod.hMod (β := ℕ)
            ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j))
            (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i : ℕ) *
          ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j),
      ⋯⟩ =
    a

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
refine_2 :
  HMod.hMod (β := ℕ) ((↑a : ℕ) / ∏ j : Fin (↑0 : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j))
          (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs 0 : ℕ) *
        ∏ j : Fin (↑0 : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j) +
      ∑ x_1 : Fin n,
        ((↑a : ℕ) / ∏ j : Fin (↑x_1.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j)) %
            xs x_1 *
          ∏ j : Fin (↑x_1.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j) =
    (↑a : ℕ)
⊢ (↑(⟨∑ i : Fin (n + 1),
              HMod.hMod (β := ℕ)
                  ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j))
                  (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i : ℕ) *
                ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j),
            ⋯⟩ :
          Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)) :
      ℕ) =
    (↑a : ℕ)

Tactic:
simp_rw [Fin.sum_univ_succ, Fin.cons_succ]

Premises used: Fin.cons_succ, Fin.sum_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
⊢ ∀ (i : Fin n),
    Eq (α := ℕ) (∏ x_1 : Fin (↑i.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ x_1))
      (∏ x_1 : Fin ((↑i : ℕ) + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ x_1))

Tactic:
have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
refine_2 :
  (↑a : ℕ) % x +
      x *
        ∑ i : Fin n,
          ((↑a : ℕ) / x /
                ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ)) %
              xs i *
            ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ) =
    (↑a : ℕ)
⊢ HMod.hMod (β := ℕ) ((↑a : ℕ) / ∏ j : Fin (↑0 : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j))
          (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs 0 : ℕ) *
        ∏ j : Fin (↑0 : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ j) +
      ∑ x_1 : Fin n,
        ((↑a : ℕ) / ∏ x_2 : Fin ((↑x_1 : ℕ) + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ x_2)) %
            xs x_1 *
          ∏ x_2 : Fin ((↑x_1 : ℕ) + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ x_2) =
    (↑a : ℕ)

Tactic:
simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
          Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
          mul_left_comm (_ % _ : ℕ), ← mul_sum]

Premises used: Finset.mul_sum, Nat.div_one, mul_left_comm, Fin.castLE_zero, HMod.hMod, Fin.prod_univ_succ, mul_one, Fintype.prod_empty, Fin.val_zero, Nat.div_div_eq_div_mul, Fin.cons_zero
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
⊢ (↑a : ℕ) % x + x * ((↑a : ℕ) / x) = (↑a : ℕ)

Tactic:
Nat.mod_add_div _ _

Premises used: Nat.mod_add_div
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
h :
  ∑ i : Fin n,
      ((↑a : ℕ) / x / ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ)) %
          xs i *
        ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ) =
    (↑a : ℕ) / x
⊢ (↑a : ℕ) % x +
      x *
        ∑ i : Fin n,
          ((↑a : ℕ) / x /
                ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ)) %
              xs i *
            ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ) =
    (↑a : ℕ)

Tactic:
convert! Nat.mod_add_div _ _

Premises used: Nat.mod_add_div
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
⊢ ∑ i : Fin n,
      ((↑a : ℕ) / x / ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ)) %
          xs i *
        ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ) =
    (↑a : ℕ) / x

Tactic:
ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _))

Premises used: Fin.cons, Fin.induction.go, Fin.is_lt, HDiv.hDiv, LT.lt.trans_eq, Fin.val, Nat.div_lt_of_lt_mul, Fin.prod_univ_succ, Fin.induction, Fin.cases
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n_1 : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)
ih :
  ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
    ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE ⋯ j) = i
⊢ ∑ i : Fin n,
      ((↑a : ℕ) / x / ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ)) %
          xs i *
        ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE ⋯ i_1.succ) =
    (↑a : ℕ) / x

Tactic:
exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _))

Premises used: Fin.is_lt, HDiv.hDiv, LT.lt.trans_eq, Fin.val, Nat.div_lt_of_lt_mul, Fin.prod_univ_succ
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
⊢ (↑((finPiFinEquiv : (a : (i : Fin m) → Fin (n i)) → Fin (∏ i : Fin m, n i)) f) : ℕ) =
    ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
n : Fin m → ℕ
inst : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
rw :
  ∀ (x : Fin m),
    x ≠ i → (↑(Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j x) : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0
⊢ (↑((finPiFinEquiv : (a : (i : Fin m) → Fin (n i)) → Fin (∏ i : Fin m, n i))
          (Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j)) :
      ℕ) =
    (↑j : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)

Tactic:
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]

Premises used: finPiFinEquiv_apply, Pi.single_eq_same, Fintype.sum_eq_single
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
n : Fin m → ℕ
inst : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
x : Fin m
hx : x ≠ i
rw : (↑0 : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0
rw₁ : HMul.hMul (α := ℕ) 0 (∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j)) = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ (↑(Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j x) : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0

Tactic:
rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.single_eq_of_ne, Fin.val_zero
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin 0 → ℕ
⊢ IsEmpty (Fin (∑ i : Fin 0, n i))

Tactic:
simpa using Fin.isEmpty'

Premises used: Fin.isEmpty'
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : Fin 0 → ℕ
k : (i : Fin 0) × Fin (n i)
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin 0) × Fin (n i)) → Fin (∑ i : Fin 0, n i)) k) : ℕ) =
    ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin 0) ↦ Fin (n i))) : ℕ)

Tactic:
k.fst.elim0

Premises used: Sigma.fst, Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
n : Fin 0 → ℕ
k : (i : Fin 0) × Fin (n i)
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin 0) × Fin (n i)) → Fin (∑ i : Fin 0, n i)) k) : ℕ) =
    ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin 0) ↦ Fin (n i))) : ℕ)

Tactic:
exact k.fst.elim0

Premises used: Sigma.fst, Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)
n : Fin (m + 1) → ℕ
k : (i : Fin (m + 1)) × Fin (n i)
succ :
  ∀ (iv : ℕ) (hi : iv < m + 1) (j : Fin (n ⟨iv, hi⟩)),
    (↑((finSigmaFinEquiv : (a : (i : Fin (m + 1)) × Fin (n i)) → Fin (∑ i : Fin (m + 1), n i))
            (Sigma.mk (β := fun (i : Fin (m + 1)) ↦ Fin (n i)) (⟨iv, hi⟩ : Fin (m + 1)) j)) :
        ℕ) =
      ∑ i : Fin (↑⟨⟨iv, hi⟩, j⟩.fst : ℕ), n (Fin.castLE ⋯ i) +
        (↑(Sigma.snd (β := fun (i : Fin (m + 1)) ↦ Fin (n i))
              (Sigma.mk (β := fun (i : Fin (m + 1)) ↦ Fin (n i)) (⟨iv, hi⟩ : Fin (m + 1)) j)) :
          ℕ)
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin (m + 1)) × Fin (n i)) → Fin (∑ i : Fin (m + 1), n i)) k) : ℕ) =
    ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin (m + 1)) ↦ Fin (n i))) : ℕ)

Tactic:
rcases k with ⟨⟨iv, hi⟩, j⟩
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ Eq (α := (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
    (Sigma.mk (β := fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
        (Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr (⟨iv, hi⟩ : Fin (m + 1)))
        (@Eq.rec _ ⟨iv, hi⟩ (fun (x : Fin (m + 1)) (h : (⟨iv, hi⟩ : Fin (m + 1)) = x) ↦ Fin (n x)) j
          (Sum.elim (Fin.castAdd 1) (Fin.natAdd m)
            (Fin.addCases (motive := fun (x : Fin (m + 1)) ↦ Fin m ⊕ Fin 1) Sum.inl Sum.inr (⟨iv, hi⟩ : Fin (m + 1))))
          ⋯) :
      (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
    (Sigma.mk (β := fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a))) (Sum.inl ⟨iv, him⟩)
        j :
      (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))

Tactic:
simp [Fin.addCases, him]
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ (↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i : Fin m, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv
                (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))) :
              (a :
                  (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))) →
                Fin (∑ i : Fin m, n i.castSucc) ⊕ Fin (n (Fin.last m)))
            ((Equiv.sumSigmaDistrib fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)) :
                  (a : (a : Fin m ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a))) →
                    (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                      (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i))))
                (Sigma.mk (β := fun (a : Fin m ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
                  (Sum.inl (⟨iv, him⟩ : Fin m)) j) :
              (i : Fin m) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inl i))) ⊕
                (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)

Tactic:
simpa using ih _
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin m) × Fin (n i)) → Fin (∑ i : Fin m, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ)
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ iv = m

Tactic:
replace him := Nat.eq_of_lt_succ_of_not_lt hi him
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin iv) × Fin (n i)) → Fin (∑ i : Fin iv, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin iv) ↦ Fin (n i))) : ℕ)
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ Eq (α := (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
    (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
        (Fin.addCases (motive := fun (x : Fin (iv + 1)) ↦ Fin iv ⊕ Fin 1) Sum.inl Sum.inr (⟨iv, hi⟩ : Fin (iv + 1)))
        (@Eq.rec _ ⟨iv, hi⟩ (fun (x : Fin (iv + 1)) (h : (⟨iv, hi⟩ : Fin (iv + 1)) = x) ↦ Fin (n x)) j
          (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv)
            (Fin.addCases (motive := fun (x : Fin (iv + 1)) ↦ Fin iv ⊕ Fin 1) Sum.inl Sum.inr
              (⟨iv, hi⟩ : Fin (iv + 1))))
          ⋯) :
      (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
    (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) (Sum.inr 0) j :
      (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))

Tactic:
simp [Fin.addCases, Fin.natAdd]

Premises used: Fin.natAdd
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
iv : ℕ
ih :
  ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)),
    (↑((finSigmaFinEquiv : (a : (i : Fin iv) × Fin (n i)) → Fin (∑ i : Fin iv, n i)) k) : ℕ) =
      ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE ⋯ i) + (↑(k.snd (β := fun (i : Fin iv) ↦ Fin (n i))) : ℕ)
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
neg :
  (↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i : Fin iv, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Fin.natAdd iv i))) :
              (a : (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i))) →
                Fin (∑ i : Fin iv, n i.castSucc) ⊕ Fin (n (Fin.last iv)))
            ((Equiv.sumSigmaDistrib fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)) :
                  (a : (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) →
                    (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i)))
                (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
                  (Sum.inr 0) j) :
              (i : Fin iv) × Fin (n (Fin.castAdd 1 i)) ⊕ (i : Fin 1) × Fin (n (Fin.natAdd iv i))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)
⊢ (↑(Sum.elim (Fin.castAdd (n (Fin.last iv))) (Fin.natAdd (∑ i : Fin iv, n i.castSucc))
          ((Equiv.sumCongr finSigmaFinEquiv
                (Equiv.uniqueSigma fun (i : Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) :
              (a :
                  (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                    (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))) →
                Fin (∑ i : Fin iv, n i.castSucc) ⊕ Fin (n (Fin.last iv)))
            ((Equiv.sumSigmaDistrib fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)) :
                  (a : (a : Fin iv ⊕ Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a))) →
                    (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                      (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i))))
                (Sigma.mk (β := fun (a : Fin iv ⊕ Fin 1) ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) a)))
                  (Sum.inr 0) j) :
              (i : Fin iv) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inl i))) ⊕
                (i : Fin 1) × Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd iv) (Sum.inr i)))))) :
      ℕ) =
    ∑ x : Fin iv, n (Fin.castLE ⋯ x) + (↑j : ℕ)

Tactic:
simp