awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
n : ℕ
rw : (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1)!
rw₁ : (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1) * n !
rw₂ : n ! * n.succ = (n + 1) * n !
rw₃ : n ! * (n + 1) = (n + 1) * n !
rw₄ rw₅ : (n + 1) * n ! = (n + 1) * n !
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!

Tactic:
rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ,
      prod_Ico_id_eq_factorial n, Nat.succ_eq_add_one, mul_comm]

Premises used: Nat.zero_le, Nat.succ_eq_add_one, Nat.factorial_succ, Finset.prod_Ico_succ_top, mul_comm, Nat.succ_le_succ
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
n : ℕ
rw : HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ j ∈ range n, j)
rw₁ rw₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, i) = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ j ∈ range n, j)
⊢ HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, (n - 1 - i))

Tactic:
rw [sum_range_reflect (fun i => i) n, mul_two]

Premises used: Finset.sum_range_reflect, mul_two
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
n : ℕ
rw : #(range n) • (n - 1) = n * (n - 1)
rw₁ : n • (n - 1) = n * (n - 1)
rw₂ rw₃ : n * (n - 1) = n * (n - 1)
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)

Tactic:
rw [sum_const, card_range, Nat.nsmul_eq_mul]

Premises used: Nat.nsmul_eq_mul, Finset.card_range, Finset.sum_const
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
n : ℕ
rw : ∑ i ∈ range n, i = HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 / 2
rw₁ rw₂ : Eq (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, i)
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2

Tactic:
rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]

Premises used: Nat.mul_div_cancel, Finset.sum_range_id_mul_two, Nat.zero_lt_two
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
rw :
  Eq.{u_3 + 1} (α := M)
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ) - x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m),
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
⊢ Eq.{u_3 + 1} (α := M) (∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k)) (∏ m ∈ range n, ∏ k ∈ range (n - m), f m k)

Tactic:
rw [prod_sigma', prod_sigma']

Premises used: Finset.prod_sigma'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ Eq.{u_3 + 1} (α := M)
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ) - x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∏ x ∈ (range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m),
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))

Tactic:
prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_

Premises used: HSub.hSub, Sigma.fst, HAdd.hAdd, Sigma.mk, Finset.prod_nbij', Sigma.snd
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
refine_1 : ∀ (a b : ℕ), a < n → b ≤ a → b < n
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m))
        ((fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)

Tactic:
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Premises used: le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, Sigma.forall, add_tsub_cancel_left, Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff, implies_true, add_tsub_cancel_of_le, lt_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1))
        ((fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)

Tactic:
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Premises used: le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, Sigma.forall, add_tsub_cancel_left, Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff, implies_true, add_tsub_cancel_of_le, lt_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
      (fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a

Tactic:
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Premises used: le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, Sigma.forall, add_tsub_cancel_left, Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff, implies_true, add_tsub_cancel_of_le, lt_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (n - m)) a →
      (fun (a : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          ((fun (a : (_ : ℕ) × ℕ) ↦
              (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.fst (β := fun (i : ℕ) ↦ ℕ) + a.snd (β := fun (i : ℕ) ↦ ℕ))
                  (a.fst (β := fun (i : ℕ) ↦ ℕ)) :
                (_ : ℕ) × ℕ))
            a) =
        a

Tactic:
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Premises used: le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, Sigma.forall, add_tsub_cancel_left, Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff, implies_true, add_tsub_cancel_of_le, lt_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range n).sigma (α := fun (a : ℕ) ↦ ℕ) fun (m : ℕ) ↦ range (m + 1)) a →
      f (a.snd (β := fun (i : ℕ) ↦ ℕ)) (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) =
        f
          (Sigma.fst (β := fun (i : ℕ) ↦ ℕ)
            ((fun (a : (_ : ℕ) × ℕ) ↦
                (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                    (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                  (_ : ℕ) × ℕ))
              a))
          (Sigma.snd (β := fun (i : ℕ) ↦ ℕ)
            ((fun (a : (_ : ℕ) × ℕ) ↦
                (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (a.snd (β := fun (i : ℕ) ↦ ℕ))
                    (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) :
                  (_ : ℕ) × ℕ))
              a))

Tactic:
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Premises used: le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, Sigma.forall, add_tsub_cancel_left, Finset.mem_sigma, Finset.mem_range, Nat.lt_succ_iff, implies_true, add_tsub_cancel_of_le, lt_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n

Tactic:
fun a b han hba ↦ lt_of_le_of_lt hba han

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n

Tactic:
exact fun a b han hba ↦ lt_of_le_of_lt hba han

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
f : ℕ → M
n : ℕ
inst : CommGroup M
⊢ HDiv.hDiv (α := M) (∏ i ∈ range (n + 1), f i) (∏ i ∈ range n, f i) = f n

Tactic:
div_eq_iff_eq_mul'.mpr <| prod_range_succ f n

Premises used: Iff.mpr, div_eq_iff_eq_mul', Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
f : ℕ → M
n : ℕ
inst : CommGroup M
⊢ (∏ i ∈ range (n + 1), f i) / f n = ∏ i ∈ range n, f i

Tactic:
div_eq_iff_eq_mul.mpr <| prod_range_succ f n

Premises used: Iff.mpr, div_eq_iff_eq_mul, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
f : ℕ → M
m n : ℕ
inst : CommGroup M
hmn : m < n
⊢ (∏ i ∈ Ico m n, f i) / f m = ∏ i ∈ Ico (m + 1) n, f i

Tactic:
div_eq_iff_eq_mul'.mpr <| prod_eq_prod_Ico_succ_bot hmn _

Premises used: Iff.mpr, div_eq_iff_eq_mul', Finset.prod_eq_prod_Ico_succ_bot
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
f : ℕ → M
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
⊢ (∏ i ∈ Ico m (n + 1), f i) / f n = ∏ i ∈ Ico m n, f i

Tactic:
div_eq_iff_eq_mul.mpr <| prod_Ico_succ_top hmn _

Premises used: Iff.mpr, Finset.prod_Ico_succ_top, div_eq_iff_eq_mul
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
f : ℕ → M
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
rw : HDiv.hDiv (α := M) (∏ k ∈ range n, f (k + 1) / f k) (∏ k ∈ range m, f (k + 1) / f k) = f n / f m
rw₁ : f n / f 0 / ∏ k ∈ range m, f (k + 1) / f k = f n / f m
rw₂ : f n / f 0 / (f m / f 0) = f n / f m
rw₃ rw₄ : f n / f m = f n / f m
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m

Tactic:
rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]

Premises used: Finset.prod_range_div, Finset.prod_Ico_eq_div, div_div_div_cancel_right
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
f : ℕ → M
hmn₁ : m ≤ n + 1
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

Tactic:
rw [← Finset.Ico_add_one_right_eq_Icc, prod_Ico_div]

Premises used: Finset.Ico_add_one_right_eq_Icc, Finset.prod_Ico_div
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ m ≤ n + 1

Tactic:
omega
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
rw :
  Eq.{u_1 + 1} (α := α) (∏ i ∈ range n, if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Icc a b then f ⟨i, h⟩ else 1 else 1)
    (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f ⟨i, h⟩ else 1)
⊢ Eq.{u_1 + 1} (α := α) (∏ i ∈ Icc a b, f i) (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f ⟨i, h⟩ else 1)

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]

Premises used: Finset.prod_fin_eq_prod_range, Finset.prod_ite_mem_eq
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
h₁ :
  ∀ a_1 ∈ range n,
    a_1 ∉ Icc (↑a : ℕ) (↑b : ℕ) →
      Eq.{u_1 + 1} (α := α) (if h : a_1 < n then if (⟨a_1, h⟩ : Fin n) ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) 1
h₂ : ∀ a_1 ∈ Icc (↑a : ℕ) (↑b : ℕ), a_1 ∉ range n → Eq.{u_1 + 1} (α := α) (if h : a_1 < n then f ⟨a_1, h⟩ else 1) 1
h :
  ∀ a_1 ∈ range n,
    a_1 ∈ Icc (↑a : ℕ) (↑b : ℕ) →
      Eq.{u_1 + 1} (α := α) (if h : a_1 < n then if (⟨a_1, h⟩ : Fin n) ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1)
        (if h : a_1 < n then f ⟨a_1, h⟩ else 1)
⊢ Eq.{u_1 + 1} (α := α) (∏ i ∈ range n, if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Icc a b then f ⟨i, h⟩ else 1 else 1)
    (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f ⟨i, h⟩ else 1)

Tactic:
apply prod_congr_of_eq_on_inter

Premises used: Finset.prod_congr_of_eq_on_inter
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n,
    a_1 ∉ Icc (↑a : ℕ) (↑b : ℕ) →
      Eq.{u_1 + 1} (α := α) (if h : a_1 < n then if (⟨a_1, h⟩ : Fin n) ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ Icc (↑a : ℕ) (↑b : ℕ), a_1 ∉ range n → Eq.{u_1 + 1} (α := α) (if h : a_1 < n then f ⟨a_1, h⟩ else 1) 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ Icc (↑a : ℕ) (↑b : ℕ) →
      Eq.{u_1 + 1} (α := α) (if h : a_1 < n then if (⟨a_1, h⟩ : Fin n) ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1)
        (if h : a_1 < n then f ⟨a_1, h⟩ else 1)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
rw :
  (∏ i ∈ range n,
      if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Iic a then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1
      else 1) =
    f a.succ / f 0
⊢ ∏ i ∈ Iic a, f i.succ / f i.castSucc = f a.succ / f 0

Tactic:
rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]

Premises used: Finset.prod_fin_eq_prod_range, Finset.prod_ite_mem_eq
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ∈ range ((↑a : ℕ) + 1),
      HDiv.hDiv (α := M) (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) (if hi : i < n + 1 then f ⟨i, hi⟩ else 1) =
    HDiv.hDiv (α := M) (if hi : (↑a : ℕ) + 1 < n + 1 then f (⟨(↑a : ℕ) + 1, hi⟩ : Fin (n + 1)) else 1)
      (if hi : 0 < n + 1 then f (⟨0, hi⟩ : Fin (n + 1)) else 1)

Tactic:
prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1)

Premises used: Finset.prod_range_div, Fin.mk, Fin.val, dite, HAdd.hAdd, LT.lt, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
h :
  Eq.{u_3 + 1} (α := M)
    (∏ i ∈ range n,
      if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Iic a then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1
      else 1)
    (∏ i ∈ range ((↑a : ℕ) + 1),
      HDiv.hDiv (α := M) (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) (if hi : i < n + 1 then f ⟨i, hi⟩ else 1))
h₁ :
  f a.succ / f 0 =
    HDiv.hDiv (α := M) (if hi : (↑a : ℕ) + 1 < n + 1 then f ⟨(↑a : ℕ) + 1, hi⟩ else 1)
      (if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1)
⊢ (∏ i ∈ range n,
      if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Iic a then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1
      else 1) =
    f a.succ / f 0

Tactic:
convert! prod_range_div (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1) (a + 1) using 1 with k
    hk

Premises used: Finset.prod_range_div, Fin.mk, Fin.val, dite, HAdd.hAdd, LT.lt, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∉ range ((↑a : ℕ) + 1) →
      Eq.{u_3 + 1} (α := M)
        (if h : a_1 < n then
          if (⟨a_1, h⟩ : Fin n) ∈ Iic a then f (⟨a_1, h⟩ : Fin n).succ / f (⟨a_1, h⟩ : Fin n).castSucc else 1
        else 1)
        1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range ((↑a : ℕ) + 1),
    a_1 ∉ range n →
      HDiv.hDiv (α := M) (if hi : a_1 + 1 < n + 1 then f (⟨a_1 + 1, hi⟩ : Fin (n + 1)) else 1)
          (if hi : a_1 < n + 1 then f (⟨a_1, hi⟩ : Fin (n + 1)) else 1) =
        1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
simp_all :
  ∀ (a_1 : ℕ) (a_2 : a_1 < n),
    a_1 ≤ (↑a : ℕ) →
      (if (⟨a_1, ⋯⟩ : Fin n) ≤ a then f (⟨a_1 + 1, ⋯⟩ : Fin (n + 1)) / f (⟨a_1, ⋯⟩ : Fin (n + 1)) else 1) =
        f (⟨a_1 + 1, ⋯⟩ : Fin (n + 1)) / if h : a_1 ≤ n then f ⟨a_1, ⋯⟩ else 1
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ range ((↑a : ℕ) + 1) →
      (if h : a_1 < n then
          if (⟨a_1, h⟩ : Fin n) ∈ Iic a then f (⟨a_1, h⟩ : Fin n).succ / f (⟨a_1, h⟩ : Fin n).castSucc else 1
        else 1) =
        HDiv.hDiv (α := M) (if hi : a_1 + 1 < n + 1 then f (⟨a_1 + 1, hi⟩ : Fin (n + 1)) else 1)
          (if hi : a_1 < n + 1 then f (⟨a_1, hi⟩ : Fin (n + 1)) else 1)

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ (a_1 : ℕ) (a_2 : a_1 < n),
    a_1 ≤ (↑a : ℕ) →
      (if (⟨a_1, ⋯⟩ : Fin n) ≤ a then f (⟨a_1 + 1, ⋯⟩ : Fin (n + 1)) / f (⟨a_1, ⋯⟩ : Fin (n + 1)) else 1) =
        f (⟨a_1 + 1, ⋯⟩ : Fin (n + 1)) / if h : a_1 ≤ n then f ⟨a_1, ⋯⟩ else 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ Eq.{u_3 + 1} (α := M)
    (∏ i ∈ range n,
      if h : i < n then if (⟨i, h⟩ : Fin n) ∈ Iic a then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1
      else 1)
    (∏ i ∈ range ((↑a : ℕ) + 1),
      HDiv.hDiv (α := M) (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) (if hi : i < n + 1 then f ⟨i, hi⟩ else 1))

Tactic:
exact prod_congr_of_eq_on_inter (by grind) (by grind) (by simp_all; grind)

Premises used: Finset.prod_congr_of_eq_on_inter
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 =
    HDiv.hDiv (α := M) (if hi : (↑a : ℕ) + 1 < n + 1 then f ⟨(↑a : ℕ) + 1, hi⟩ else 1)
      (if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
rw :
  (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1) =
    f b.succ / f a.castSucc
⊢ ∏ i ∈ Icc a b, f i.succ / f i.castSucc = f b.succ / f a.castSucc

Tactic:
rw [prod_fin_Icc_eq_prod_nat_Icc]

Premises used: Finset.prod_fin_Icc_eq_prod_nat_Icc
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ ∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ),
      HDiv.hDiv (α := M) (if hi : i + 1 < n + 1 then f ⟨i + 1, hi⟩ else 1) (if hi : i < n + 1 then f ⟨i, hi⟩ else 1) =
    HDiv.hDiv (α := M) (if hi : (↑b : ℕ) + 1 < n + 1 then f (⟨(↑b : ℕ) + 1, hi⟩ : Fin (n + 1)) else 1)
      (if hi : (↑a : ℕ) < n + 1 then f (⟨(↑a : ℕ), hi⟩ : Fin (n + 1)) else 1)

Tactic:
Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)

Premises used: Fin.mk, Fin.le_def, dite, HAdd.hAdd, LT.lt, Iff.mp, Finset.prod_Icc_div, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
h :
  ∀ x ∈ Icc (↑a : ℕ) (↑b : ℕ),
    (if h : x < n then f (⟨x, h⟩ : Fin n).succ / f (⟨x, h⟩ : Fin n).castSucc else 1) =
      HDiv.hDiv (α := M) (if hi : x + 1 < n + 1 then f (⟨x + 1, hi⟩ : Fin (n + 1)) else 1)
        (if hi : x < n + 1 then f (⟨x, hi⟩ : Fin (n + 1)) else 1)
h₁ : f b.succ = if hi : (↑b : ℕ) + 1 < n + 1 then f ⟨(↑b : ℕ) + 1, hi⟩ else 1
h₂ : f a.castSucc = if hi : (↑a : ℕ) < n + 1 then f ⟨(↑a : ℕ), hi⟩ else 1
⊢ (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f (⟨i, h⟩ : Fin n).succ / f (⟨i, h⟩ : Fin n).castSucc else 1) =
    f b.succ / f a.castSucc

Tactic:
convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)

Premises used: Fin.mk, Fin.le_def, dite, HAdd.hAdd, LT.lt, Iff.mp, Finset.prod_Icc_div, OfNat.ofNat
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x : ℕ
h_1 : x ∈ Icc (↑a : ℕ) (↑b : ℕ)
h :
  (↑a : ℕ) ≤ x ∧ x ≤ (↑b : ℕ) →
    (if h : x < n then f (⟨x + 1, ⋯⟩ : Fin (n + 1)) / f (⟨x, ⋯⟩ : Fin (n + 1)) else 1) =
      HDiv.hDiv (α := M) (if h : x < n then f (⟨x + 1, ⋯⟩ : Fin (n + 1)) else 1)
        (if h : x ≤ n then f (⟨x, ⋯⟩ : Fin (n + 1)) else 1)
⊢ (if h : x < n then f (⟨x, h⟩ : Fin n).succ / f (⟨x, h⟩ : Fin n).castSucc else 1) =
    HDiv.hDiv (α := M) (if hi : x + 1 < n + 1 then f (⟨x + 1, hi⟩ : Fin (n + 1)) else 1)
      (if hi : x < n + 1 then f (⟨x, hi⟩ : Fin (n + 1)) else 1)

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x : ℕ
h : (↑a : ℕ) ≤ x ∧ x ≤ (↑b : ℕ)
⊢ (if h : x < n then f (⟨x + 1, ⋯⟩ : Fin (n + 1)) / f (⟨x, ⋯⟩ : Fin (n + 1)) else 1) =
    HDiv.hDiv (α := M) (if h : x < n then f (⟨x + 1, ⋯⟩ : Fin (n + 1)) else 1)
      (if h : x ≤ n then f (⟨x, ⋯⟩ : Fin (n + 1)) else 1)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f b.succ = if hi : (↑b : ℕ) + 1 < n + 1 then f ⟨(↑b : ℕ) + 1, hi⟩ else 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
h : f a.castSucc = f ⟨(↑a : ℕ), ⋯⟩
⊢ f a.castSucc = if hi : (↑a : ℕ) < n + 1 then f ⟨(↑a : ℕ), hi⟩ else 1

Tactic:
simp only [Order.lt_add_one_iff, is_le', ↓reduceDIte]

Premises used: reduceDIte, Order.lt_add_one_iff, Fin.is_le'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = f ⟨(↑a : ℕ), ⋯⟩

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]),
    (List.map f []).prod ≡ (List.map g []).prod [MOD n]
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [MOD n]) →
      ∀ (h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]),
        (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [MOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [MOD n]

Tactic:
induction l
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ (x : α), Membership.mem (γ := List α) [] x → f x ≡ g x [MOD n]
⊢ (List.map f []).prod ≡ (List.map g []).prod [MOD n]

Tactic:
aesop (add unsafe ModEq.mul)

Premises used: Nat.ModEq.mul
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
head : α
tail : List α
tail_ih : ∀ (h : ∀ x ∈ tail, f x ≡ g x [MOD n]), (List.map f tail).prod ≡ (List.map g tail).prod [MOD n]
h : ∀ x ∈ head :: tail, f x ≡ g x [MOD n]
⊢ (List.map f (head :: tail)).prod ≡ (List.map g (head :: tail)).prod [MOD n]

Tactic:
aesop (add unsafe ModEq.mul)

Premises used: Nat.ModEq.mul
-- Module: Mathlib.Algebra.BigOperators.ModEq
Goal:
α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 1 [MOD n]
⊢ List.prod (List.map (fun (x : α) ↦ 1) l) ≡ 1 [MOD n]

Tactic:
simp [ModEq.refl]

Premises used: Nat.ModEq.refl