awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left : k ≤ i
im : i < m
j : ℕ
left_1 : k ≤ j
jm : j < m
Hij : n - i = n - j
inl : n - (n - i) = j
inl₁ : n - (n - j) = j
⊢ i = j
have inl₂ : j = j
Tactic: rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (hypothesis)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
have this₁ : n + 1 - k ≤ n + 1 - m
Tactic: have : n + 1 - k ≤ n + 1 - m := by
      rw [tsub_le_tsub_iff_left h]
      exact hkm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range n, f (n - 1 - j)) (∏ j ∈ range n, f j)
have zero : Eq.{u_3 + 1} (α := M) (∏ j ∈ range 0, f (HSub.hSub (α := ℕ) 0 1 - j)) (∏ j ∈ range 0, f j)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
zero : Eq.{u_3 + 1} (α := M) (∏ j ∈ range 0, f (HSub.hSub (α := ℕ) 0 1 - j)) (∏ j ∈ range 0, f j)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range n, f (n - 1 - j)) (∏ j ∈ range n, f j)
have succ : ∀ (n : ℕ), Eq.{u_3 + 1} (α := M) (∏ j ∈ range (n + 1), f (n + 1 - 1 - j)) (∏ j ∈ range (n + 1), f j)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range (n + 1), f (n + 1 - 1 - j)) (∏ j ∈ range (n + 1), f j)
have succ : Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico 0 (n + 1), f (n - x)) (∏ x ∈ Ico 0 (n + 1), f x)
Tactic: simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico 0 (n + 1), f (n - x)) (∏ x ∈ Ico 0 (n + 1), f x)
have succ : Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico (n + 1 - (n + 1)) (n + 1 - 0), f j) (∏ x ∈ Ico 0 (n + 1), f x)
Tactic: rw [prod_Ico_reflect _ _ le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!
have rw : (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
rw : (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1)!
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!
have rw₁ : (∏ k ∈ Ico (succ 0) n.succ, k) * n.succ = (n + 1) * n !
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 !
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!
have rw₂ : n ! * n.succ = (n + 1) * n !
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 !
⊢ ∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!
have rw₄ : (n + 1) * n ! = (n + 1) * n !
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
⊢ HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, (n - 1 - i))
have rw : HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ j ∈ range n, j)
Tactic: rw [sum_range_reflect (fun i => i) n, mul_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
rw : HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 = 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))
have rw₁ : HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, i) = HAdd.hAdd (α := ℕ) (∑ i ∈ range n, i) (∑ j ∈ range n, j)
Tactic: rw [sum_range_reflect (fun i => i) n, mul_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)
have rw : #(range n) • (n - 1) = n * (n - 1)
Tactic: rw [sum_const, card_range, Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
rw : #(range n) • (n - 1) = n * (n - 1)
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)
have rw₁ : n • (n - 1) = n * (n - 1)
Tactic: rw [sum_const, card_range, Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
rw : #(range n) • (n - 1) = n * (n - 1)
rw₁ : n • (n - 1) = n * (n - 1)
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)
have rw₂ : n * (n - 1) = n * (n - 1)
Tactic: rw [sum_const, card_range, Nat.nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2
have rw : ∑ i ∈ range n, i = HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 / 2
Tactic: rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
n : ℕ
rw : ∑ i ∈ range n, i = HMul.hMul (α := ℕ) (∑ i ∈ range n, i) 2 / 2
⊢ ∑ i ∈ range n, i = n * (n - 1) / 2
have rw₁ : Eq (α := ℕ) (∑ i ∈ range n, i) (∑ i ∈ range n, i)
Tactic: rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ Nat.zero_lt_two]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ 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)
have 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 : ℕ) ↦ ℕ)))
Tactic: rw [prod_sigma', prod_sigma']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 : ℕ) ↦ ℕ)))
have refine_1 : ∀ (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: refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (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)
⊢ 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 : ℕ) ↦ ℕ)))
have refine_2 : ∀ (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: refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (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)
refine_2 :
  ∀ (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)
⊢ 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 : ℕ) ↦ ℕ)))
have refine_3 : ∀ (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: refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (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)
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (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
⊢ 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 : ℕ) ↦ ℕ)))
have refine_4 : ∀ (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: refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 →
      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)
have refine_1 : ∀ (a b : ℕ), a < n → b ≤ a → b < n
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]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
f : ℕ → M
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m
have rw : HDiv.hDiv (α := M) (∏ k ∈ range n, f (k + 1) / f k) (∏ k ∈ range m, f (k + 1) / f k) = f n / f m
Tactic: rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m
have rw₁ : f n / f 0 / ∏ k ∈ range m, f (k + 1) / f k = f n / f m
Tactic: rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m
have rw₂ : f n / f 0 / (f m / f 0) = f n / f m
Tactic: rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m
have rw₃ : f n / f m = f n / f m
Tactic: rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
m n : ℕ
inst : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m
have hmn₁ : m ≤ n + 1
Tactic: rw [← Finset.Ico_add_one_right_eq_Icc, prod_Ico_div]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ Eq.{u_1 + 1} (α := α) (∏ i ∈ Icc a b, f i) (∏ i ∈ Icc (↑a : ℕ) (↑b : ℕ), if h : i < n then f ⟨i, h⟩ else 1)
have 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)
Tactic: rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ 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)
have 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
Tactic: apply prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ 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)
have 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
Tactic: apply prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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
⊢ 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)
have 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)
Tactic: apply prod_congr_of_eq_on_inter
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∏ i ∈ Iic a, f i.succ / f i.castSucc = f a.succ / f 0
have 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
Tactic: rw [← prod_ite_mem_eq, prod_fin_eq_prod_range]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 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) =
    f a.succ / f 0
have 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))
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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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))
⊢ (∏ 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
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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) →
      (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)
have simp_all : ∀ (a_1 : ℕ) (a_2 : a_1 < n),
  a_1 ≤ (↑a : ℕ) →
    (if (⟨a_1, sorry⟩ : Fin n) ≤ a then f (⟨a_1 + 1, sorry⟩ : Fin (n + 1)) / f (⟨a_1, sorry⟩ : Fin (n + 1)) else 1) =
      f (⟨a_1 + 1, sorry⟩ : Fin (n + 1)) / if h : a_1 ≤ n then f ⟨a_1, sorry⟩ else 1
Tactic: simp_all
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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, f i.succ / f i.castSucc = f b.succ / f a.castSucc
have 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
Tactic: rw [prod_fin_Icc_eq_prod_nat_Icc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
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 : ℕ), 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
have 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)
Tactic: convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)