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
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
⊢ ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
have rw : ∏ k ∈ Ico a (b + 1 + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
Tactic: rw [← Ico_add_one_right_eq_Icc, prod_Ico_succ_top hab, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
rw : ∏ k ∈ Ico a (b + 1 + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
⊢ ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
have rw₁ : (∏ k ∈ Ico a (b + 1), f k) * f (b + 1) = (∏ k ∈ Icc a b, f k) * f (b + 1)
Tactic: rw [← Ico_add_one_right_eq_Icc, prod_Ico_succ_top hab, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b + 1
f : ℕ → M
rw : ∏ k ∈ Ico a (b + 1 + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
rw₁ : (∏ k ∈ Ico a (b + 1), f k) * f (b + 1) = (∏ k ∈ Icc a b, f k) * f (b + 1)
⊢ ∏ k ∈ Icc a (b + 1), f k = (∏ k ∈ Icc a b, f k) * f (b + 1)
have rw₂ : (∏ k ∈ Icc a b, f k) * f (b + 1) = (∏ k ∈ Icc a b, f k) * f (b + 1)
Tactic: rw [← Ico_add_one_right_eq_Icc, prod_Ico_succ_top hab, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
δ : Type u_4
inst : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ HMul.hMul (α := δ) (∏ k ∈ Ico m n, f k) (∏ k ∈ range m, f k) = ∏ k ∈ range n, f k
have rw : HMul.hMul (α := δ) (∏ k ∈ range m, f k) (∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ HDiv.hDiv (α := G) (∏ k ∈ range m, f k) (∏ k ∈ range n, f k) = ∏ k ∈ range m with n ≤ k, f k
have rw : Eq.{u_4 + 1} (α := G) (∏ k ∈ Ico n m, f k) (∏ k ∈ range m with n ≤ k, f k)
Tactic: rw [← prod_Ico_eq_div f hnm]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ Eq.{u_4 + 1} (α := G) (∏ k ∈ Ico n m, f k) (∏ k ∈ range m with n ≤ k, f k)
have e_s : Ico n m = {k ∈ range m | n ≤ k}
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ Ico n m = {k ∈ range m | n ≤ k}
have e_s : ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}
Tactic: apply Finset.ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}
have e_s : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
Tactic: simp only [mem_Ico, mem_filter, mem_range, *]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₄ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
e_s₄ e_s₅ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₆ : ∀ (a : ℕ), n ≤ a → a < m → a < m
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
e_s₄ e_s₅ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
e_s₆ : ∀ (a : ℕ), n ≤ a → a < m → a < m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₇ : ∀ (a : ℕ), n ≤ a → a < m → n ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
e_s₄ e_s₅ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
e_s₆ : ∀ (a : ℕ), n ≤ a → a < m → a < m
e_s₇ : ∀ (a : ℕ), n ≤ a → a < m → n ≤ a
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₈ : ∀ a < m, n ≤ a → n ≤ a ∧ a < m
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
e_s₄ e_s₅ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
e_s₆ : ∀ (a : ℕ), n ≤ a → a < m → a < m
e_s₇ : ∀ (a : ℕ), n ≤ a → a < m → n ≤ a
e_s₈ e_s₉ : ∀ a < m, n ≤ a → n ≤ a ∧ a < m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₁₀ : ∀ a < m, n ≤ a → n ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s e_s₁ : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
e_s₂ : ∀ (a : ℕ), n ≤ a ∧ a < m → a < m ∧ n ≤ a
e_s₃ : ∀ (a : ℕ), a < m ∧ n ≤ a → n ≤ a ∧ a < m
e_s₄ e_s₅ : ∀ (a : ℕ), n ≤ a → a < m → a < m ∧ n ≤ a
e_s₆ : ∀ (a : ℕ), n ≤ a → a < m → a < m
e_s₇ : ∀ (a : ℕ), n ≤ a → a < m → n ≤ a
e_s₈ e_s₉ : ∀ a < m, n ≤ a → n ≤ a ∧ a < m
e_s₁₀ : ∀ a < m, n ≤ a → n ≤ a
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
have e_s₁₁ : ∀ a < m, n ≤ a → a < m
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j) (∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j)
have rw : Eq.{u_4 + 1} (α := M)
  (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b,
    f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
  (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1),
    f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
Tactic: rw [Finset.sum_sigma', Finset.sum_sigma']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b,
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
have refine_1 : ∀ (a_1 : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b) a_1 →
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1))
      ((fun (x : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a_1)
Tactic: refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (a_1 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b) a_1 →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1))
        ((fun (x : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a_1)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b,
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
have refine_2 : ∀ (a_1 : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1)) a_1 →
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b)
      ((fun (x : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a_1)
Tactic: refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b) a_1 →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1))
        ((fun (x : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a_1)
have refine_1 : ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1 + 1
Tactic: simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (j : ℕ) ↦ Ico a (j + 1))
        a_1 →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico i b)
        ((fun (x : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a_1)
have refine_2 : ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 + 1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 ≤ a_1 ∧ a_1 < b
Tactic: simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j) (∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j)
have rw : Eq.{u_4 + 1} (α := M)
  (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b,
    f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
  (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a),
    f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
Tactic: rw [Finset.sum_sigma', Finset.sum_sigma']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b,
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
have refine_1 : ∀ (a_1 : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b) a_1 →
    (fun (x : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a_1 ∈
      (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a)
Tactic: refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
refine_1 :
  ∀ (a_1 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b)
        a_1 →
      (fun (x : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a_1 ∈
        (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b,
      f (x.fst (β := fun (i : ℕ) ↦ ℕ)) (x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ x ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a),
      f (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)))
have refine_2 : ∀ a_1 ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b)
    ((fun (x : (_ : ℕ) × ℕ) ↦
        (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
      a_1)
Tactic: refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a_1 : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b)
        a_1 →
      (fun (x : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a_1 ∈
        (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a)
have refine_1 : ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 + 1 ≤ b_1 ∧ b_1 < b → (a ≤ b_1 ∧ b_1 < b) ∧ a ≤ a_1 ∧ a_1 < b_1
Tactic: simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ a_1 ∈ (Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) (Ico a),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((Ico a b).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ Ico (i + 1) b)
      ((fun (x : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (x.snd (β := fun (i : ℕ) ↦ ℕ)) (x.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a_1)
have refine_2 : ∀ (a_1 b_1 : ℕ), (a ≤ a_1 ∧ a_1 < b) ∧ a ≤ b_1 ∧ b_1 < a_1 → (a ≤ b_1 ∧ b_1 < b) ∧ b_1 + 1 ≤ a_1 ∧ a_1 < b
Tactic: simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have pos : ∀ (h : m ≤ n), Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
Tactic: by_cases! h : m ≤ n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
pos : ∀ (h : m ≤ n), Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg : ∀ (h : n < m), Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
Tactic: by_cases! h : m ≤ n
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have pos : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ Ico 0 (n - m), f (m + k))
Tactic: rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
pos : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ Ico 0 (n - m), f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have pos₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico (0 + m) (n - m + m), f x)
Tactic: rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
pos : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ Ico 0 (n - m), f (m + k))
pos₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico (0 + m) (n - m + m), f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have pos₂ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico m (n - m + m), f x)
Tactic: rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
pos : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ Ico 0 (n - m), f (m + k))
pos₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico (0 + m) (n - m + m), f x)
pos₂ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico m (n - m + m), f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have pos₃ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico m n, f x)
Tactic: rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (hypothesis)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have h₁ : n ≤ m
Tactic: replace h := h.le
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range (n - m), f (m + k))
Tactic: rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
neg : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range (n - m), f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range 0, f (m + k))
Tactic: rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
neg : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range (n - m), f (m + k))
neg₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range 0, f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg₂ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ ∅, f (m + k))
Tactic: rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
neg : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range (n - m), f (m + k))
neg₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range 0, f (m + k))
neg₂ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ ∅, f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg₃ : Eq.{u_3 + 1} (α := M) 1 (∏ k ∈ ∅, f (m + k))
Tactic: rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Intervals (goal)
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
neg : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range (n - m), f (m + k))
neg₁ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ range 0, f (m + k))
neg₂ : Eq.{u_3 + 1} (α := M) (∏ k ∈ ∅, f k) (∏ k ∈ ∅, f (m + k))
neg₃ : Eq.{u_3 + 1} (α := M) 1 (∏ k ∈ ∅, f (m + k))
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))
have neg₄ : Eq.{u_3 + 1} (α := M) 1 1
Tactic: rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]
-- 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
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
have this : ∀ i < m, i ≤ n
Tactic: have : ∀ i < m, i ≤ n := by
    intro i hi
    exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
-- 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
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
have inl : ∀ (hkm : k < m), Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
Tactic: rcases lt_or_ge k m with hkm | hkm
-- 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
inl : ∀ (hkm : k < m), Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
have inr : ∀ (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)
Tactic: rcases lt_or_ge k m with hkm | hkm
-- 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
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)
have inl : Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ image (fun (x : ℕ) ↦ n - x) (Ico k m), f j)
Tactic: rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
-- 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
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ image (fun (x : ℕ) ↦ n - x) (Ico k m), f j)
have inl : Set.InjOn (HSub.hSub n) (↑(Ico k m) : Set ℕ)
Tactic: refine (prod_image ?_).symm
-- 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
⊢ Set.InjOn (HSub.hSub n) (↑(Ico k m) : Set ℕ)
have inl : ∀ ⦃x₁ : ℕ⦄, k ≤ x₁ ∧ x₁ < m → ∀ ⦃x₂ : ℕ⦄, k ≤ x₂ ∧ x₂ < m → n - x₁ = n - x₂ → x₁ = x₂
Tactic: simp only [mem_Ico, Set.InjOn, mem_coe]
-- 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
⊢ i = j
have inl : n - (n - i) = 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 (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
⊢ i = j
have inl₁ : n - (n - j) = j
Tactic: rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]