awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n n_1 : ℕ
ih : ∀ (f : Fin n → Fin (n_1 + 1)), ∑ i : Fin n, (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ n
f : Fin (n + 1) → Fin (n_1 + 1)
succ : (1 + n_1) * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
succ₁ : (n_1 + 1) * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
⊢ (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
have succ₂ : (n_1 + 1) * (n_1 + 1) ^ n = (n_1 + 1) * (n_1 + 1) ^ n
Tactic: rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
f : Fin n → Fin m
⊢ ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n
have zero : ∀ (f : Fin 0 → Fin m), ∑ i : Fin 0, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < HPow.hPow (β := ℕ) m 0
Tactic: induction n with
      | zero => simp
      | succ n ih =>
        cases m
        · exact isEmptyElim (f <| Fin.last _)
        simp_rw [Fin.sum_univ_castSucc, Fin.val_castSucc, Fin.val_last]
        refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_
        rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
f : Fin n → Fin m
zero : ∀ (f : Fin 0 → Fin m), ∑ i : Fin 0, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < HPow.hPow (β := ℕ) m 0
⊢ ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n
have succ : ∀ (n : ℕ) (ih : ∀ (f : Fin n → Fin m), ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n) (f : Fin (n + 1) → Fin m),
  ∑ i : Fin (n + 1), (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ (n + 1)
Tactic: induction n with
      | zero => simp
      | succ n ih =>
        cases m
        · exact isEmptyElim (f <| Fin.last _)
        simp_rw [Fin.sum_univ_castSucc, Fin.val_castSucc, Fin.val_last]
        refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_
        rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
have zero : ∀ (a : Fin (HPow.hPow (β := ℕ) m 0)) (b : Fin 0), (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
b : Fin n
zero : ∀ (a : Fin (HPow.hPow (β := ℕ) m 0)) (b : Fin 0), (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
have succ : ∀ (n : ℕ) (a : Fin (m ^ (n + 1))) (b : Fin (n + 1)), (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
Tactic: rcases n with - | n
Cleared hypotheses: n, a, b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
have succ : ∀ (a : Fin (HPow.hPow (α := ℕ) 0 (n + 1))), (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0
Tactic: rcases m with - | m
Cleared hypotheses: m, a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
b : Fin (n + 1)
succ : ∀ (a : Fin (HPow.hPow (α := ℕ) 0 (n + 1))), (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
have succ₁ : ∀ (m : ℕ) (a : Fin ((m + 1) ^ (n + 1))), (↑a : ℕ) / (m + 1) ^ (↑b : ℕ) % (m + 1) < m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m, a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (HPow.hPow (α := ℕ) 0 (n + 1))
⊢ (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0
have succ : ∀ (a_1 : Fin 0), (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0
Tactic: rw [zero_pow n.succ_ne_zero] at a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (a : Fin (m ^ n)), ⟨∑ i : Fin n, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
a : Fin (m ^ (n + 1))
⊢ ⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
have ih₁ : ∀ (i : ℕ) (h : i < m ^ n), ∑ x : Fin n, i / m ^ (↑x : ℕ) % m * m ^ (↑x : ℕ) = 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 : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ (i : ℕ) (h : i < m ^ n), ∑ x : Fin n, i / m ^ (↑x : ℕ) % m * m ^ (↑x : ℕ) = i
⊢ ⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
have succ : (↑(⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), sorry⟩ : Fin (m ^ (n + 1))) : ℕ) = (↑a : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ (i : ℕ) (h : i < m ^ n), ∑ x : Fin n, i / m ^ (↑x : ℕ) % m * m ^ (↑x : ℕ) = i
⊢ (↑(⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ : Fin (m ^ (n + 1))) : ℕ) = (↑a : ℕ)
have succ : (↑a : ℕ) % m + m * ∑ i : Fin n, (↑a : ℕ) / m / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ) = (↑a : ℕ)
Tactic: simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ (i : ℕ) (h : i < m ^ n), ∑ x : Fin n, i / m ^ (↑x : ℕ) % m * m ^ (↑x : ℕ) = i
⊢ (↑a : ℕ) % m + m * ∑ i : Fin n, (↑a : ℕ) / m / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ) = (↑a : ℕ)
have succ : (↑a : ℕ) % m + m * ((↑a : ℕ) / m) = (↑a : ℕ)
Tactic: rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ (i : ℕ) (h : i < m ^ n), ∑ x : Fin n, i / m ^ (↑x : ℕ) % m * m ^ (↑x : ℕ) = i
succ : (↑a : ℕ) % m + m * ((↑a : ℕ) / m) = (↑a : ℕ)
⊢ (↑a : ℕ) % m + m * ∑ i : Fin n, (↑a : ℕ) / m / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ) = (↑a : ℕ)
have succ₁ : (↑a : ℕ) = (↑a : ℕ)
Tactic: rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
⊢ ⟨∑ i : Fin n, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
have zero : ∀ (a : Fin (HPow.hPow (β := ℕ) m 0)), ⟨∑ i : Fin 0, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), sorry⟩ = a
Tactic: induction n with
      | zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
      | succ n ih =>
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
        rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ n)
zero : ∀ (a : Fin (HPow.hPow (β := ℕ) m 0)), ⟨∑ i : Fin 0, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
⊢ ⟨∑ i : Fin n, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a
have succ : ∀ (n : ℕ) (ih : ∀ (a : Fin (m ^ n)), ⟨∑ i : Fin n, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), sorry⟩ = a)
  (a : Fin (m ^ (n + 1))), ⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), sorry⟩ = a
Tactic: induction n with
      | zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
      | succ n ih =>
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
        rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]
Cleared hypotheses: n, a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
m n : ℕ
inst : NeZero m
i : Fin n
j : Fin m
⊢ (↑((finFunctionFinEquiv : (a : Fin n → Fin m) → Fin (m ^ n)) (Pi.single (M := fun (a : Fin n) ↦ Fin m) i j)) : ℕ) =
    (↑j : ℕ) * m ^ (↑i : ℕ)
have rw : ∀ (x : Fin n), x ≠ i → (↑(Pi.single (M := fun (a : Fin n) ↦ Fin m) i j x) : ℕ) * m ^ (↑x : ℕ) = 0
Tactic: rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
m n : ℕ
inst : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ (↑(Pi.single (M := fun (a : Fin n) ↦ Fin m) i j x) : ℕ) * m ^ (↑x : ℕ) = 0
have rw : (↑0 : ℕ) * m ^ (↑x : ℕ) = 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 : ℕ
inst : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
rw : (↑0 : ℕ) * m ^ (↑x : ℕ) = 0
⊢ (↑(Pi.single (M := fun (a : Fin n) ↦ Fin m) i j x) : ℕ) * m ^ (↑x : ℕ) = 0
have rw₁ : 0 * m ^ (↑x : ℕ) = 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 : ℕ
inst : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
rw : (↑0 : ℕ) * m ^ (↑x : ℕ) = 0
rw₁ : 0 * m ^ (↑x : ℕ) = 0
⊢ (↑(Pi.single (M := fun (a : Fin n) ↦ Fin m) i j x) : ℕ) * m ^ (↑x : ℕ) = 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:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Fintype.card ((i : Fin m) → Fin (n i)) = Fintype.card (Fin (∏ i : Fin m, n i))
have simp_rw : ∏ i : Fin m, Fintype.card (Fin (n i)) = Fintype.card (Fin (∏ i : Fin m, n i))
Tactic: simp_rw [Fintype.card_pi, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ LT.lt (α := ℕ) (∑ i : Fin (m + 1), (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin (m + 1), n i)
have succ : ∑ i : Fin m, (↑(f i.castSucc) : ℕ) * ∏ j : Fin (↑i.castSucc : ℕ), n (Fin.castLE sorry j) +
    (↑(f (Fin.last m)) : ℕ) * ∏ j : Fin (↑(Fin.last m) : ℕ), n (Fin.castLE sorry j) <
  (∏ i : Fin m, n i.castSucc) * n (Fin.last m)
Tactic: rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i : Fin m, (↑(f i.castSucc) : ℕ) * ∏ j : Fin (↑i.castSucc : ℕ), n (Fin.castLE ⋯ j) +
      (↑(f (Fin.last m)) : ℕ) * ∏ j : Fin (↑(Fin.last m) : ℕ), n (Fin.castLE ⋯ j) <
    (∏ i : Fin m, n i.castSucc) * n (Fin.last m)
have succ : ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
  ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * nn
Tactic: suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin nn
⊢ ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * nn
have succ : ∀ (fn : Fin 0),
  ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    HMul.hMul (α := ℕ) (∏ i : Fin m, n i) 0
Tactic: cases nn
Cleared hypotheses: nn, fn
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
nn : ℕ
f : (i : Fin m) → Fin (n i)
fn : Fin nn
succ :
  ∀ (fn : Fin 0),
    ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
      HMul.hMul (α := ℕ) (∏ i : Fin m, n i) 0
⊢ ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * nn
have succ₁ : ∀ (n_2 : ℕ) (fn : Fin (n_2 + 1)),
  ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * (n_2 + 1)
Tactic: cases nn
Cleared hypotheses: nn, fn
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n_2 : ℕ
fn : Fin (n_2 + 1)
⊢ ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * (n_2 + 1)
have succ : ∏ i : Fin m, n i + n_2 * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * (n_2 + 1)
Tactic: refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n_2 : ℕ
fn : Fin (n_2 + 1)
⊢ ∏ i : Fin m, n i + n_2 * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * (n_2 + 1)
have succ : (1 + n_2) * ∏ i : Fin m, n i = (∏ i : Fin m, n i) * (n_2 + 1)
Tactic: rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n_2 : ℕ
fn : Fin (n_2 + 1)
succ : (1 + n_2) * ∏ i : Fin m, n i = (∏ i : Fin m, n i) * (n_2 + 1)
⊢ ∏ i : Fin m, n i + n_2 * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * (n_2 + 1)
have succ₁ : (∏ i : Fin m, n i) * (1 + n_2) = (∏ i : Fin m, n i) * (n_2 + 1)
Tactic: rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
ih :
  ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
n_1 : Fin (m + 1) → ℕ
f_1 : (i : Fin (m + 1)) → Fin (n_1 i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n_2 : ℕ
fn : Fin (n_2 + 1)
succ : (1 + n_2) * ∏ i : Fin m, n i = (∏ i : Fin m, n i) * (n_2 + 1)
succ₁ : (∏ i : Fin m, n i) * (1 + n_2) = (∏ i : Fin m, n i) * (n_2 + 1)
⊢ ∏ i : Fin m, n i + n_2 * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * (n_2 + 1)
have succ₂ : (∏ i : Fin m, n i) * (n_2 + 1) = (∏ i : Fin m, n i) * (n_2 + 1)
Tactic: rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
⊢ LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
have zero : ∀ {n : Fin 0 → ℕ} (f : (i : Fin 0) → Fin (n i)),
  LT.lt (α := ℕ) (∑ i : Fin 0, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j)) (∏ i : Fin 0, n i)
Tactic: induction m with
      | zero => simp
      | succ m ih =>
      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
      suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim
      intro n nn f fn
      cases nn
      · exact isEmptyElim fn
      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
Cleared hypotheses: m, n, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
zero :
  ∀ {n : Fin 0 → ℕ} (f : (i : Fin 0) → Fin (n i)),
    LT.lt (α := ℕ) (∑ i : Fin 0, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin 0, n i)
⊢ LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, n i)
have succ : ∀ (m : ℕ)
  (ih :
    ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)),
      LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j)) (∏ i : Fin m, n i))
  {n : Fin (m + 1) → ℕ} (f : (i : Fin (m + 1)) → Fin (n i)),
  LT.lt (α := ℕ) (∑ i : Fin (m + 1), (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE sorry j)) (∏ i : Fin (m + 1), n i)
Tactic: induction m with
      | zero => simp
      | succ m ih =>
      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
      suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim
      intro n nn f fn
      cases nn
      · exact isEmptyElim fn
      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]
Cleared hypotheses: m, n, f
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin m, n i)
b : Fin m
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b
have zero : ∀ {n : Fin 0 → ℕ} (a : Fin (∏ i : Fin 0, n i)) (b : Fin 0),
  ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE sorry j)) % n b < n b
Tactic: cases m
Cleared hypotheses: m, n, a, b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i : Fin m, n i)
b : Fin m
zero :
  ∀ {n : Fin 0 → ℕ} (a : Fin (∏ i : Fin 0, n i)) (b : Fin 0),
    ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b
have succ : ∀ (n : ℕ) {n_1 : Fin (n + 1) → ℕ} (a : Fin (∏ i : Fin (n + 1), n_1 i)) (b : Fin (n + 1)),
  ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n_1 (Fin.castLE sorry j)) % n_1 b < n_1 b
Tactic: cases m
Cleared hypotheses: m, n, a, b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n_1 : ℕ
n : Fin (n_1 + 1) → ℕ
a : Fin (∏ i : Fin (n_1 + 1), n i)
b : Fin (n_1 + 1)
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b
have succ : ∀ (h : n b = 0), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE sorry j)) % 0 < 0
Tactic: rcases h : n b with nb | nb
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n_1 : ℕ
n : Fin (n_1 + 1) → ℕ
a : Fin (∏ i : Fin (n_1 + 1), n i)
b : Fin (n_1 + 1)
succ : ∀ (h : n b = 0), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b
have succ₁ : ∀ (nb : ℕ) (h : n b = nb + 1), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE sorry j)) % (nb + 1) < nb + 1
Tactic: rcases h : n b with nb | nb
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
n_1 : ℕ
n : Fin (n_1 + 1) → ℕ
a : Fin (∏ i : Fin (n_1 + 1), n i)
b : Fin (n_1 + 1)
h : n b = 0
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0
have succ : ∀ (a_1 : Fin 0) (b : Fin (n_1 + 1)) (h : n b = 0), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE sorry j)) % 0 < 0
Tactic: rw [prod_eq_zero (Finset.mem_univ _) h] at a
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
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
have 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 sorry j), sorry⟩ : Fin (∏ i : Fin m, n i)))
      ((fun (a : Fin (∏ i : Fin m, n i)) (b : Fin m) ↦
          (⟨((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE sorry j)) % n b, sorry⟩ : Fin (n b)))
        a) =
    a
Tactic: revert a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
have refine_1 : ∀ (a : Fin (∏ i : Fin 0, i.elim0)),
  ⟨∑ i : Fin 0,
        ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), (Fin.castLE sorry j).elim0) % i.elim0 * ∏ j : Fin (↑i : ℕ), (Fin.castLE sorry j).elim0,
      sorry⟩ =
    a
Tactic: refine Fin.consInduction ?_ ?_ n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (goal)
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
⊢ ∀ (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
have refine_2 : ∀ {n : ℕ} (x₀ : ℕ) (x : Fin n → ℕ),
  (∀ (a : Fin (∏ i : Fin n, x i)),
      ⟨∑ i : Fin n, ((↑a : ℕ) / ∏ j : Fin (↑i : ℕ), x (Fin.castLE sorry j)) % x i * ∏ j : Fin (↑i : ℕ), x (Fin.castLE sorry j),
          sorry⟩ =
        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 sorry 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 sorry j),
          sorry⟩ =
        a
Tactic: refine Fin.consInduction ?_ ?_ n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Fin (hypothesis)
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
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
have this : Subsingleton (Fin (∏ i : Fin 0, i.elim0))
Tactic: have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton