awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n
f : Fin (n + 1) → Fin m
succ :
  ∀ (ih : ∀ (f : Fin n → Fin 0), ∑ i : Fin n, (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 n)
    (f : Fin (n + 1) → Fin 0),
    ∑ i : Fin (n + 1), (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 (n + 1)
succ₁ :
  ∀ (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)), ∑ i : Fin (n + 1), (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ (n + 1)
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ (n + 1)

Tactic:
cases m
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i : Fin n, (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 n
f : Fin (n + 1) → Fin 0
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 (n + 1)

Tactic:
isEmptyElim (f <| Fin.last _)

Premises used: isEmptyElim, Fin.last
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
ih : ∀ (f : Fin n → Fin 0), ∑ i : Fin n, (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 n
f : Fin (n + 1) → Fin 0
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * HPow.hPow (α := ℕ) 0 (↑i : ℕ) < HPow.hPow (α := ℕ) 0 (n + 1)

Tactic:
exact isEmptyElim (f <| Fin.last _)
-- Module: Mathlib.Algebra.BigOperators.Fin
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 :
  ∑ x : Fin n, (↑(f x.castSucc) : ℕ) * (n_1 + 1) ^ (↑x : ℕ) + (↑(f (Fin.last n)) : ℕ) * (n_1 + 1) ^ n <
    (n_1 + 1) ^ (n + 1)
⊢ ∑ i : Fin (n + 1), (↑(f i) : ℕ) * (n_1 + 1) ^ (↑i : ℕ) < (n_1 + 1) ^ (n + 1)

Tactic:
simp_rw [Fin.sum_univ_castSucc, Fin.val_castSucc, Fin.val_last]

Premises used: Fin.sum_univ_castSucc, Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
⊢ ∑ x : Fin n, (↑(f x.castSucc) : ℕ) * (n_1 + 1) ^ (↑x : ℕ) + (↑(f (Fin.last n)) : ℕ) * (n_1 + 1) ^ n <
    (n_1 + 1) ^ (n + 1)

Tactic:
(Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_

Premises used: Nat.mul_le_mul_right, Fin.is_le, LT.lt.trans_eq, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)
⊢ ∑ x : Fin n, (↑(f x.castSucc) : ℕ) * (n_1 + 1) ^ (↑x : ℕ) + (↑(f (Fin.last n)) : ℕ) * (n_1 + 1) ^ n <
    (n_1 + 1) ^ (n + 1)

Tactic:
refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_

Premises used: Nat.mul_le_mul_right, Fin.is_le, LT.lt.trans_eq, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
succ₂ succ₃ : (n_1 + 1) * (n_1 + 1) ^ n = (n_1 + 1) * (n_1 + 1) ^ n
⊢ (n_1 + 1) ^ n + n_1 * (n_1 + 1) ^ n = (n_1 + 1) ^ (n + 1)

Tactic:
rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']

Premises used: add_comm, one_add_mul, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.Fin
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
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)
⊢ ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ) < m ^ n

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']

Premises used: Fin.sum_univ_castSucc, add_comm, one_add_mul, pow_succ', Fin.val_last, Fin.val_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ : ∀ (n : ℕ) (a : Fin (m ^ (n + 1))) (b : Fin (n + 1)), (↑a : ℕ) / m ^ (↑b : ℕ) % m < m
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m

Tactic:
rcases n with - | n
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (HPow.hPow (β := ℕ) m 0)
b : Fin 0
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m

Tactic:
b.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (HPow.hPow (β := ℕ) m 0)
b : Fin 0
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m

Tactic:
exact b.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ₁ : ∀ (m : ℕ) (a : Fin ((m + 1) ^ (n + 1))), (↑a : ℕ) / (m + 1) ^ (↑b : ℕ) % (m + 1) < m + 1
⊢ (↑a : ℕ) / m ^ (↑b : ℕ) % m < m

Tactic:
rcases m with - | m
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (HPow.hPow (α := ℕ) 0 (n + 1))
succ : ∀ (a_1 : Fin 0), (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0
⊢ (↑a : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0

Tactic:
rw [zero_pow n.succ_ne_zero] at a

Premises used: Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a_1 : Fin (HPow.hPow (α := ℕ) 0 (n + 1))
a : Fin 0
⊢ (↑a_1 : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0

Tactic:
a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a_1 : Fin (HPow.hPow (α := ℕ) 0 (n + 1))
a : Fin 0
⊢ (↑a_1 : ℕ) / HPow.hPow (α := ℕ) 0 (↑b : ℕ) % 0 < 0

Tactic:
exact a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
m : ℕ
a : Fin ((m + 1) ^ (n + 1))
⊢ (↑a : ℕ) / (m + 1) ^ (↑b : ℕ) % (m + 1) < m + 1

Tactic:
Nat.mod_lt _ m.succ_pos

Premises used: Nat.mod_lt, Nat.succ_pos
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
m : ℕ
a : Fin ((m + 1) ^ (n + 1))
⊢ (↑a : ℕ) / (m + 1) ^ (↑b : ℕ) % (m + 1) < m + 1

Tactic:
exact Nat.mod_lt _ m.succ_pos

Premises used: Nat.mod_lt, Nat.succ_pos
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
m : ℕ
a : Fin (HPow.hPow (β := ℕ) m 0)
⊢ ⟨∑ i : Fin 0, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a

Tactic:
subsingleton [(finCongr <| pow_zero _).subsingleton]

Premises used: finCongr, pow_zero, Equiv.subsingleton
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ) (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

Premises used: Fin.ext_iff, Fin.forall_iff
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : (↑(⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ : Fin (m ^ (n + 1))) : ℕ) = (↑a : ℕ)
⊢ ⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = a

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Fin
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 * ∑ i : Fin n, (↑a : ℕ) / m / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ) = (↑a : ℕ)
⊢ (↑(⟨∑ i : Fin (n + 1), (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ : Fin (m ^ (n + 1))) : ℕ) = (↑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]

Premises used: Finset.mul_sum, Nat.div_one, Fin.val_succ, mul_left_comm, pow_zero, mul_one, Fin.val_zero, pow_succ', Fin.sum_univ_succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ℕ)
succ₁ succ₂ : (↑a : ℕ) = (↑a : ℕ)
⊢ (↑a : ℕ) % m + m * ∑ i : Fin n, (↑a : ℕ) / m / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ) = (↑a : ℕ)

Tactic:
rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]

Premises used: Fin.is_lt, LT.lt.trans_eq, Nat.div_lt_of_lt_mul, Nat.mod_add_div, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ :
  ∀ (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
⊢ ⟨∑ i : Fin n, (↑a : ℕ) / m ^ (↑i : ℕ) % m * m ^ (↑i : ℕ), ⋯⟩ = 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]

Premises used: Finset.mul_sum, Fin.ext_iff, finCongr, Nat.div_one, Fin.val_succ, mul_left_comm, pow_zero, Nat.mod_add_div, Fin.forall_iff, mul_one, Equiv.subsingleton, Fin.val_zero, pow_succ', Fin.sum_univ_succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
m n : ℕ
f : Fin n → Fin m
⊢ (↑((finFunctionFinEquiv : (a : Fin n → Fin m) → Fin (m ^ n)) f) : ℕ) = ∑ i : Fin n, (↑(f i) : ℕ) * m ^ (↑i : ℕ)

Tactic:
rfl

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

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

Premises used: Pi.single_eq_same, finFunctionFinEquiv_apply, Fintype.sum_eq_single
-- Module: Mathlib.Algebra.BigOperators.Fin
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
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ (↑(Pi.single (M := fun (a : Fin n) ↦ Fin m) i j x) : ℕ) * m ^ (↑x : ℕ) = 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 m → ℕ
simp_rw : ∏ i : Fin m, Fintype.card (Fin (n i)) = Fintype.card (Fin (∏ i : Fin m, n i))
⊢ Fintype.card ((i : Fin m) → Fin (n i)) = Fintype.card (Fin (∏ i : Fin m, n i))

Tactic:
simp_rw [Fintype.card_pi, Fintype.card_fin]

Premises used: Fintype.card_pi, Fintype.card_fin
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
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)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
succ :
  ∑ 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)
⊢ LT.lt (α := ℕ) (∑ i : Fin (m + 1), (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin (m + 1), n i)

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

Premises used: Fin.sum_univ_castSucc, Fin.prod_univ_castSucc
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
this :
  ∀ (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
⊢ ∑ 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)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
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 ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
      (∏ i : Fin m, n i) * nn
⊢ ∑ 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)

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
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ₁ :
  ∀ (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)
⊢ ∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j) + (↑fn : ℕ) * ∏ j : Fin m, n j <
    (∏ i : Fin m, n i) * nn

Tactic:
cases nn
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
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

Tactic:
isEmptyElim fn

Premises used: isEmptyElim
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
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

Tactic:
exact isEmptyElim fn
-- Module: Mathlib.Algebra.BigOperators.Fin
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)

Tactic:
(Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_

Premises used: Nat.mul_le_mul_right, Fin.is_le, LT.lt.trans_eq, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.BigOperators.Fin
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 : ∏ i : Fin m, n i + n_2 * ∏ j : Fin m, n j = (∏ i : Fin m, n i) * (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)

Tactic:
refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_

Premises used: Nat.mul_le_mul_right, Fin.is_le, LT.lt.trans_eq, Nat.add_lt_add_of_lt_of_le
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
succ₂ succ₃ : (∏ i : Fin m, n i) * (n_2 + 1) = (∏ 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)

Tactic:
rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]

Premises used: add_comm, mul_comm, one_add_mul
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
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 ⋯ 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)
⊢ LT.lt (α := ℕ) (∑ i : Fin m, (↑(f i) : ℕ) * ∏ j : Fin (↑i : ℕ), n (Fin.castLE ⋯ j)) (∏ i : Fin m, 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]

Premises used: Fin.sum_univ_castSucc, Fin.prod_univ_castSucc, add_comm, mul_comm, one_add_mul
-- Module: Mathlib.Algebra.BigOperators.Fin
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
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 ⋯ j)) % n_1 b < n_1 b
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
cases m
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
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

Tactic:
b.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
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

Tactic:
exact b.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ₁ : ∀ (nb : ℕ) (h : n b = nb + 1), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % (nb + 1) < nb + 1
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % n b < n b

Tactic:
rcases h : n b with nb | nb
-- Module: Mathlib.Algebra.BigOperators.Fin
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
succ : ∀ (a_1 : Fin 0) (b : Fin (n_1 + 1)) (h : n b = 0), ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0

Tactic:
rw [prod_eq_zero (Finset.mem_univ _) h] at a

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n_1 : ℕ
n : Fin (n_1 + 1) → ℕ
a_1 : Fin (∏ i : Fin (n_1 + 1), n i)
a : Fin 0
b : Fin (n_1 + 1)
h : n b = 0
⊢ ((↑a_1 : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0

Tactic:
isEmptyElim a

Premises used: isEmptyElim
-- Module: Mathlib.Algebra.BigOperators.Fin
Goal:
ι : Type u_1
M : Type u_2
n_1 : ℕ
n : Fin (n_1 + 1) → ℕ
a_1 : Fin (∏ i : Fin (n_1 + 1), n i)
a : Fin 0
b : Fin (n_1 + 1)
h : n b = 0
⊢ ((↑a_1 : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % 0 < 0

Tactic:
exact isEmptyElim a
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
nb : ℕ
h : n b = nb + 1
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % (nb + 1) < nb + 1

Tactic:
Nat.mod_lt _ nb.succ_pos

Premises used: Nat.mod_lt, Nat.succ_pos
-- Module: Mathlib.Algebra.BigOperators.Fin
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)
nb : ℕ
h : n b = nb + 1
⊢ ((↑a : ℕ) / ∏ j : Fin (↑b : ℕ), n (Fin.castLE ⋯ j)) % (nb + 1) < nb + 1

Tactic:
exact Nat.mod_lt _ nb.succ_pos

Premises used: Nat.mod_lt, Nat.succ_pos