awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
apply : ∀ (x : ℕ) (hx : x ∈ Ioc m n) (h'x : x ∈ Ioc n k), False
⊢ Disjoint (Ioc m n) (Ioc n k)

Tactic:
apply disjoint_left.2 fun x hx h'x => _

Premises used: Iff.mpr, Finset.disjoint_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False

Tactic:
lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

Premises used: lt_irrefl, And.right, And.left, LT.lt.trans_le, Iff.mp, Finset.mem_Ioc
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
x : ℕ
hx : x ∈ Ioc m n
h'x : x ∈ Ioc n k
⊢ False

Tactic:
exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

Premises used: lt_irrefl, And.right, And.left, LT.lt.trans_le, Iff.mp, Finset.mem_Ioc
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
rw : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ Ioc b b.succ, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
rw₁ : HMul.hMul (α := M) (∏ i ∈ Ioc a b, f i) (∏ i ∈ {b + 1}, f i) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
rw₂ rw₃ : (∏ i ∈ Ioc a b, f i) * f (b + 1) = (∏ k ∈ Ioc a b, f k) * f (b + 1)
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Tactic:
rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]

Premises used: Nat.Ioc_succ_singleton, Finset.prod_singleton, Nat.le_succ, Finset.prod_Ioc_consecutive
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
rw₂ rw₃ : (∏ k ∈ Icc a b, 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)

Tactic:
rw [← Ico_add_one_right_eq_Icc, prod_Ico_succ_top hab, Ico_add_one_right_eq_Icc]

Premises used: Finset.Ico_add_one_right_eq_Icc, Finset.prod_Ico_succ_top
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ HMul.hMul (α := M) (∏ k ∈ range m, f k) (∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k

Tactic:
Nat.Ico_zero_eq_range m ▸ Nat.Ico_zero_eq_range n ▸ prod_Ico_consecutive f m.zero_le h

Premises used: Nat.zero_le, Finset.prod_Ico_consecutive, Eq.rec, Nat.Ico_zero_eq_range
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
hn : 0 < n
⊢ ∏ x ∈ range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x

Tactic:
Finset.range_eq_Ico n ▸ Finset.prod_eq_prod_Ico_succ_bot hn f

Premises used: Eq.rec, Finset.prod_eq_prod_Ico_succ_bot, Finset.range_eq_Ico, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
rw : HMul.hMul (α := δ) (∏ k ∈ range m, f k) (∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k
⊢ HMul.hMul (α := δ) (∏ k ∈ Ico m n, f k) (∏ k ∈ range m, f k) = ∏ k ∈ range n, f k

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ HMul.hMul (α := δ) (∏ k ∈ range m, f k) (∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k

Tactic:
prod_range_mul_prod_Ico f h

Premises used: Finset.prod_range_mul_prod_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ HMul.hMul (α := δ) (∏ k ∈ range m, f k) (∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k

Tactic:
exact prod_range_mul_prod_Ico f h

Premises used: Finset.prod_range_mul_prod_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : CommGroup δ
f : ℕ → δ
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = HDiv.hDiv (α := δ) (∏ k ∈ range n, f k) (∏ k ∈ range m, f k)

Tactic:
simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h

Premises used: div_eq_mul_inv, Finset.prod_Ico_eq_mul_inv
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
rw : Eq.{u_4 + 1} (α := G) (∏ k ∈ Ico n m, f k) (∏ k ∈ range m with n ≤ k, f k)
⊢ HDiv.hDiv (α := G) (∏ k ∈ range m, f k) (∏ k ∈ range n, f k) = ∏ k ∈ range m with n ≤ k, f k

Tactic:
rw [← prod_Ico_eq_div f hnm]

Premises used: Finset.prod_Ico_eq_div
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s : Ico n m = {k ∈ range m | n ≤ k}
⊢ Eq.{u_4 + 1} (α := G) (∏ k ∈ Ico n m, f k) (∏ k ∈ range m with n ≤ k, f k)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s : ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}
⊢ Ico n m = {k ∈ range m | n ≤ k}

Tactic:
apply Finset.ext

Premises used: Finset.ext
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
G : Type u_4
inst : CommGroup G
f : ℕ → G
n m : ℕ
hnm : n ≤ m
e_s : ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a
⊢ ∀ (a : ℕ), a ∈ Ico n m ↔ a ∈ {k ∈ range m | n ≤ k}

Tactic:
simp only [mem_Ico, mem_filter, mem_range, *]

Premises used: Finset.mem_range, Finset.mem_filter, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
e_s₁₁ : ∀ a < m, n ≤ a → a < m
⊢ ∀ (a : ℕ), n ≤ a ∧ a < m ↔ a < m ∧ n ≤ a

Tactic:
tauto
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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 : ℕ) ↦ ℕ)))
⊢ 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)

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']

Premises used: Finset.sum_sigma'
-- Module: Mathlib.Algebra.BigOperators.Intervals
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 : ℕ) ↦ ℕ)))

Tactic:
sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)

Premises used: Sigma.fst, Sigma.mk, Sigma.snd, rfl, Finset.sum_nbij'
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
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)
⊢ 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:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)

Premises used: rfl, Finset.sum_nbij'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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
⊢ ∀ (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:
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Premises used: Sigma.forall, Finset.mem_sigma, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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
⊢ ∀ (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:
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Premises used: Sigma.forall, Finset.mem_sigma, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (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:
lia
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (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:
lia
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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 : ℕ) ↦ ℕ)))
⊢ 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)

Tactic:
rw [Finset.sum_sigma', Finset.sum_sigma']

Premises used: Finset.sum_sigma'
-- Module: Mathlib.Algebra.BigOperators.Intervals
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 : ℕ) ↦ ℕ)))

Tactic:
sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)

Premises used: Sigma.fst, Sigma.mk, Sigma.snd, rfl, Finset.sum_nbij'
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
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)
⊢ 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:
refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl)

Premises used: rfl, Finset.sum_nbij'
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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
⊢ ∀ (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:
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Premises used: Sigma.forall, Finset.mem_sigma, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
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
⊢ ∀ 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:
simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma]

Premises used: Sigma.forall, Finset.mem_sigma, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (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:
lia
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_4
inst : AddCommMonoid M
a b : ℕ
f : ℕ → ℕ → M
⊢ ∀ (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:
lia
-- Module: Mathlib.Algebra.BigOperators.Intervals
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))
neg : ∀ (h : n < m), 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))

Tactic:
by_cases! h : m ≤ n
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
pos₃ pos₄ : Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ x ∈ Ico m n, f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, f k) (∏ k ∈ range (n - m), f (m + k))

Tactic:
rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le, zero_add, Nat.Ico_zero_eq_range, Finset.prod_Ico_add
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ n ≤ m

Tactic:
replace h := h.le
-- Module: Mathlib.Algebra.BigOperators.Intervals
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))
neg₄ neg₅ : Eq.{u_3 + 1} (α := M) 1 1
⊢ Eq.{u_3 + 1} (α := M) (∏ k ∈ Ico m n, 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]

Premises used: Iff.mpr, Finset.prod_empty, tsub_eq_zero_iff_le, Finset.Ico_eq_empty_of_le, Finset.range_zero
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n

Tactic:
(add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)

Premises used: Nat.lt_iff_add_one_le, add_le_add_iff_right, Iff.mp, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
i : ℕ
hi : i < m
⊢ i ≤ n

Tactic:
exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)

Premises used: Nat.lt_iff_add_one_le, add_le_add_iff_right, Iff.mp, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
⊢ ∀ 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)
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
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)
⊢ 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

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
inl : Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ image (fun (x : ℕ) ↦ n - x) (Ico k m), f j)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)

Tactic:
rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]

Premises used: Nat.Ico_image_const_sub_eq_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)

Tactic:
(prod_image ?_).symm

Premises used: Eq.symm, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
inl : Set.InjOn (HSub.hSub n) (↑(Ico k m) : Set ℕ)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ image (fun (x : ℕ) ↦ n - x) (Ico k m), f j)

Tactic:
refine (prod_image ?_).symm

Premises used: Eq.symm, Finset.prod_image
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
inl : ∀ ⦃x₁ : ℕ⦄, k ≤ x₁ ∧ x₁ < m → ∀ ⦃x₂ : ℕ⦄, k ≤ x₂ ∧ x₂ < m → n - x₁ = n - x₂ → x₁ = x₂
⊢ Set.InjOn (HSub.hSub n) (↑(Ico k m) : Set ℕ)

Tactic:
simp only [mem_Ico, Set.InjOn, mem_coe]

Premises used: Set.InjOn, Finset.mem_coe, Finset.mem_Ico
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
inl₂ inl₃ : j = j
⊢ i = j

Tactic:
rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]

Premises used: tsub_tsub_cancel_of_le
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
rw : m ≤ k
⊢ n + 1 - k ≤ n + 1 - m

Tactic:
rw [tsub_le_tsub_iff_left h]

Premises used: tsub_le_tsub_iff_left
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
⊢ m ≤ k

Tactic:
hkm
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
⊢ m ≤ k

Tactic:
exact hkm
-- Module: Mathlib.Algebra.BigOperators.Intervals
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
⊢ n + 1 - k ≤ n + 1 - m

Tactic:
have : n + 1 - k ≤ n + 1 - m := by
      rw [tsub_le_tsub_iff_left h]
      exact hkm
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this_1 : ∀ i < m, i ≤ n
hkm : m ≤ k
this : n + 1 - k ≤ n + 1 - m
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico k m, f (n - j)) (∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)

Tactic:
simp only [hkm, Ico_eq_empty_of_le, prod_empty, Ico_eq_empty_of_le this]

Premises used: Finset.prod_empty, Finset.Ico_eq_empty_of_le
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : AddCommMonoid δ
f : ℕ → δ
k m n : ℕ
h : m ≤ n + 1
⊢ Eq.{u_4 + 1} (α := δ) (∑ j ∈ Ico k m, f (n - j)) (∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j)

Tactic:
@prod_Ico_reflect (Multiplicative δ) _ f k m n h

Premises used: Multiset.sum, Finset.prod_Ico_reflect, Multiplicative, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Intervals
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)
succ : ∀ (n : ℕ), Eq.{u_3 + 1} (α := M) (∏ j ∈ range (n + 1), f (n + 1 - 1 - j)) (∏ j ∈ range (n + 1), f j)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range n, f (n - 1 - j)) (∏ j ∈ range n, f j)

Tactic:
cases n
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range 0, f (HSub.hSub (α := ℕ) 0 1 - j)) (∏ j ∈ range 0, f j)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
succ : Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico 0 (n + 1), f (n - x)) (∏ x ∈ Ico 0 (n + 1), f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ range (n + 1), f (n + 1 - 1 - j)) (∏ j ∈ range (n + 1), f j)

Tactic:
simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]

Premises used: tsub_zero, Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
succ : Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico (n + 1 - (n + 1)) (n + 1 - 0), f j) (∏ x ∈ Ico 0 (n + 1), f x)
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ Ico 0 (n + 1), f (n - x)) (∏ x ∈ Ico 0 (n + 1), f x)

Tactic:
rw [prod_Ico_reflect _ _ le_rfl]

Premises used: le_rfl, Finset.prod_Ico_reflect
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
M : Type u_3
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ Eq.{u_3 + 1} (α := M) (∏ j ∈ Ico (n + 1 - (n + 1)) (n + 1 - 0), f j) (∏ x ∈ Ico 0 (n + 1), f x)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Intervals
Goal:
δ : Type u_4
inst : AddCommMonoid δ
f : ℕ → δ
n : ℕ
⊢ Eq.{u_4 + 1} (α := δ) (∑ j ∈ range n, f (n - 1 - j)) (∑ j ∈ range n, f j)

Tactic:
@prod_range_reflect (Multiplicative δ) _ f n

Premises used: Multiset.sum, Finset.prod_range_reflect, Multiplicative, Finset.sum