awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
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 : 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
have ih₁ : ∀ (i : ℕ) (h : i < ∏ i : Fin n, xs i),
  ∑ x : Fin n, (i / ∏ j : Fin (↑x : ℕ), xs (Fin.castLE sorry j)) % xs x * ∏ j : Fin (↑x : ℕ), xs (Fin.castLE sorry j) = i
Tactic: simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 + 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
have refine_2 : (↑(⟨∑ i : Fin (n + 1),
            HMod.hMod (β := ℕ)
                ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry 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 sorry j),
          sorry⟩ :
        Fin (∏ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs i)) :
    ℕ) =
  (↑a : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 + 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 : ℕ)
have refine_2 : HMod.hMod (β := ℕ) ((↑a : ℕ) / ∏ j : Fin (↑0 : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry 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 sorry j) +
    ∑ x_1 : Fin n,
      ((↑a : ℕ) / ∏ j : Fin (↑x_1.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry j)) % xs x_1 *
        ∏ j : Fin (↑x_1.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry j) =
  (↑a : ℕ)
Tactic: simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
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
⊢ 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 : ℕ)
have this : ∀ (i : Fin n),
  Eq (α := ℕ) (∏ x_1 : Fin (↑i.succ : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry x_1))
    (∏ x_1 : Fin ((↑i : ℕ) + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry 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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ 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 : ℕ)
have 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 sorry i_1.succ)) %
            xs i *
          ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry i_1.succ) =
  (↑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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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 *
        ∑ 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 : ℕ)
have h : ∑ i : Fin n,
    ((↑a : ℕ) / x / ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry i_1.succ)) %
        xs i *
      ∏ i_1 : Fin (↑i : ℕ), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x xs (Fin.castLE sorry i_1.succ) =
  (↑a : ℕ) / x
Tactic: convert! Nat.mod_add_div _ _
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
m : ℕ
n : Fin m → ℕ
inst : ∀ (i : Fin m), NeZero (n i)
i : Fin m
j : Fin (n i)
⊢ (↑((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)
have 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 sorry j) = 0
Tactic: rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ (↑(Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j x) : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0
have rw : (↑0 : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE sorry j) = 0
Tactic: rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ (↑(Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j x) : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0
have rw₁ : HMul.hMul (α := ℕ) 0 (∏ j : Fin (↑x : ℕ), n (Fin.castLE sorry j)) = 0
Tactic: rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ (↑(Pi.single (M := fun (i : Fin m) ↦ Fin (n i)) i j x) : ℕ) * ∏ j : Fin (↑x : ℕ), n (Fin.castLE ⋯ j) = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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)
⊢ (↑((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))) : ℕ)
have 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 sorry 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)) :
        ℕ)
Tactic: rcases k with ⟨⟨iv, hi⟩, j⟩
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
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)))
                    (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⟩ : Fin (m + 1))
                      (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))) :
              (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 : ℕ)
have him₁ : iv = m
Tactic: replace him := Nat.eq_of_lt_succ_of_not_lt hi him
Cleared hypotheses: him
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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⟩)
⊢ (↑(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 : ℕ)
have 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 sorry x) + (↑j : ℕ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
m : ℕ
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))) : ℕ)
have zero : ∀ {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 sorry i) + (↑(k.snd (β := fun (i : Fin 0) ↦ Fin (n i))) : ℕ)
Tactic: induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
  rcases k with ⟨⟨iv, hi⟩, j⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using ih _
  · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl
Cleared hypotheses: m, n, k
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
m : ℕ
n : Fin m → ℕ
k : (i : Fin m) × Fin (n i)
zero :
  ∀ {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))) : ℕ)
⊢ (↑((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))) : ℕ)
have succ : ∀ (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 sorry i) + (↑(k.snd (β := fun (i : Fin m) ↦ Fin (n i))) : ℕ))
  {n : Fin (m + 1) → ℕ} (k : (i : Fin (m + 1)) × Fin (n i)),
  (↑((finSigmaFinEquiv : (a : (i : Fin (m + 1)) × Fin (n i)) → Fin (∑ i : Fin (m + 1), n i)) k) : ℕ) =
    ∑ i : Fin (↑k.fst : ℕ), n (Fin.castLE sorry i) + (↑(k.snd (β := fun (i : Fin (m + 1)) ↦ Fin (n i))) : ℕ)
Tactic: induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
  rcases k with ⟨⟨iv, hi⟩, j⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using ih _
  · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl
Cleared hypotheses: m, n, k
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ (↑((finSigmaFinEquiv : (a : (i : Fin 1) × Fin (n i)) → Fin (∑ i : Fin 1, n i)) ij) : ℕ) =
    (↑(ij.snd (β := fun (i : Fin 1) ↦ Fin (n i))) : ℕ)
have rw : Eq (α := ℕ) (∑ i : Fin (↑ij.fst : ℕ), n (Fin.castLE sorry i)) 0
Tactic: rw [finSigmaFinEquiv_apply, add_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have pos : ∀ (h : i < n), (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
pos : ∀ (h : i < n), (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have neg : ∀ (h : ¬i < n), (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
Tactic: by_cases h : i < n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have this : i < (ofFn f).length
Tactic: have : i < length (ofFn f) := by rwa [length_ofFn]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have pos : (take i (ofFn f)).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (ofFn f) i this =
  ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
Tactic: rw [prod_take_succ _ _ this]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : i < n
this : i < (ofFn f).length
⊢ (take i (ofFn f)).prod * getElem (valid := fun (as : List M) (i : ℕ) ↦ i < as.length) (ofFn f) i this =
    ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have A : Eq (α := Finset (Fin n)) {j : Fin n | (↑j : ℕ) < i + 1} (insert (⟨i, h⟩ : Fin n) {j : Fin n | (↑j : ℕ) < i})
Tactic: have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
⊢ take i (ofFn f) = take i.succ (ofFn f)
have h₁ : ¬i < (ofFn f).length
Tactic: rw [← length_ofFn (f := f)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < (ofFn f).length
⊢ take i (ofFn f) = take i.succ (ofFn f)
have this : (ofFn f).length ≤ i
Tactic: have : length (ofFn f) ≤ i := not_lt.mp h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ take i (ofFn f) = take i.succ (ofFn f)
have rw : ofFn f = take i.succ (ofFn f)
Tactic: rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
rw : ofFn f = take i.succ (ofFn f)
⊢ take i (ofFn f) = take i.succ (ofFn f)
have rw₁ : ofFn f = ofFn f
Tactic: rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i + 1, f j
have A : take i (ofFn f) = take i.succ (ofFn f)
Tactic: have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j : Fin n with (↑j : ℕ) < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
⊢ ((↑j : ℕ) < i.succ) = ((↑j : ℕ) < i)
have this : (↑j : ℕ) < i
Tactic: have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)