awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)

Tactic:
exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

Premises used: Finset.prod_filter_ne_one, Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s : Set κ).Pairwise fun (i j : κ) ↦ ∀ k ∈ t i ∩ t j, f k = 1
let let₁ let₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₃ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₄ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
let₅ let₆ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}), (↑s : Set κ).PairwiseDisjoint t'
let₇ let₈ :
  let t' : (k : κ) → Finset ι := fun (k : κ) ↦ {i ∈ t k | f i ≠ 1};
  ∀ (this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)

Tactic:
classical
  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

Premises used: Finset.prod_biUnion, Finset.prod_filter_ne_one, Finset.prod_congr, ne_eq, Finset.mem_filter, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
j : κ
hj : j ∈ {i ∈ I | f i = f n}.erase n
⊢ j ≠ n ∧ j ∈ I ∧ f j = f n

Tactic:
simp only [mem_erase, mem_filter] at hj

Premises used: Finset.mem_erase, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
j : κ
hj : j ≠ n ∧ j ∈ I ∧ f j = f n
⊢ g (f j) = 1

Tactic:
hf hj.2.1 hn hj.1 hj.2.2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
j : κ
hj : j ≠ n ∧ j ∈ I ∧ f j = f n
⊢ g (f j) = 1

Tactic:
exact hf hj.2.1 hn hj.1 hj.2.2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1

Tactic:
have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 := by
    simp only [mem_erase, mem_filter] at hj
    exact hf hj.2.1 hn hj.1 hj.2.2
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
⊢ f n = f n

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
rw : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1
rw₁ : ∏ j ∈ I with f j = f n, g (f j) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
rw₂ rw₃ : g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x) = g (f n) * ∏ x ∈ {i ∈ I | f i = f n}.erase n, g (f x)
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)

Tactic:
rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]

Premises used: Iff.mpr, Finset.prod_eq_one, Finset.mul_prod_erase, And.intro, Finset.mem_filter, mul_one, Finset.filter, Eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
have : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
have₁ : ∀ (h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1), ∏ j ∈ I with f j = f n, g (f j) = g (f n)
have₂ : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1
have₃ have₄ :
  ∀ (h : ∀ (j : κ) (hj : j ∈ {i ∈ I | f i = f n}.erase n), g (f j) = 1), ∏ j ∈ I with f j = f n, g (f j) = g (f n)
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)

Tactic:
classical
  have h j (hj : j ∈ {i ∈ I | f i = f n}.erase n) : g (f j) = 1 := by
    simp only [mem_erase, mem_filter] at hj
    exact hf hj.2.1 hn hj.1 hj.2.2
  rw [← mul_one (g (f n)), ← prod_eq_one h,
    ← mul_prod_erase {i ∈ I | f i = f n} (fun i ↦ g (f i)) <| mem_filter.mpr ⟨hn, by rfl⟩]

Premises used: Iff.mpr, And.intro, Finset.mem_filter, mul_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
eq : ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, g (f j)
⊢ Eq.{u_4 + 1} (α := M) (∏ s ∈ image f I, g s) (∏ i ∈ I, g (f i))

Tactic:
rw [prod_image']

Premises used: Finset.prod_image'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, g (f j)

Tactic:
fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm

Premises used: Finset.prod_filter_of_pairwise_eq_one, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I : Set κ).Pairwise fun (i j : κ) ↦ f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, g (f j)

Tactic:
exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm

Premises used: Finset.prod_filter_of_pairwise_eq_one, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
⊢ Eq.{u_4 + 1} (α := M) (∏ s ∈ image f I, g s) (∏ i ∈ I, g (f i))

Tactic:
prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j hdisj hfij ↦ ?_

Premises used: Finset.prod_image_of_pairwise_eq_one, Set.Pairwise.imp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
refine : ∀ (i j : κ) (hdisj : (_root_.Disjoint on f) i j) (hfij : f i = f j), g (f i) = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ s ∈ image f I, g s) (∏ i ∈ I, g (f i))

Tactic:
refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j hdisj hfij ↦ ?_

Premises used: Finset.prod_image_of_pairwise_eq_one, Set.Pairwise.imp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
i j : κ
hdisj : (_root_.Disjoint on f) i j
hfij : f i = f j
⊢ f i = ⊥

Tactic:
rw [Function.onFun, ← hfij, disjoint_self] at hdisj

Premises used: Function.onFun, disjoint_self
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
i j : κ
hdisj : (_root_.Disjoint on f) i j
hfij : f i = f j
hdisj₁ : f i = ⊥
⊢ f i = f j

Tactic:
rw [Function.onFun, ← hfij, disjoint_self] at hdisj

Premises used: Function.onFun, disjoint_self
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
inst_2 : PartialOrder ι
inst_3 : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I : Set κ).PairwiseDisjoint f
i j : κ
hdisj : f i = ⊥
hfij : f i = f j
rw : g ⊥ = 1
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 1 1
⊢ g (f i) = 1

Tactic:
rw [hdisj, hg_bot]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
rw : ∏ x ∈ {default}, f x = f default
rw₁ rw₂ : f default = f default
⊢ ∏ x ∈ s, f x = f default

Tactic:
rw [h.eq_singleton_default, Finset.prod_singleton]

Premises used: Finset.Nonempty.eq_singleton_default, Finset.prod_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g : ι → M
h : ∀ i ∈ s, f i ∣ g i
⊢ Dvd.dvd.{u_4} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
Multiset.prod_dvd_prod_of_dvd _ _ h

Premises used: Finset.prod, Multiset.prod_dvd_prod_of_dvd
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
e : ι ≃ κ
⊢ (map e.toEmbedding s).prod (f ∘ (⇑e.symm : (a : κ) → ι)) = s.prod f

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : κ → M
e : ι ≃ κ
⊢ s.prod (f ∘ (⇑e : (a : ι) → κ)) = (map e.toEmbedding s).prod f

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
rw : ∏ x ∈ t \ s ∪ s, f x = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)
rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t \ s ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s \ t ∪ t, f x)
rw₃ : Eq.{u_4 + 1} (α := M) (∏ x ∈ t ∪ s, f x) (∏ x ∈ s ∪ t, f x)
rw₄ rw₅ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s ∪ t, f x) (∏ x ∈ s ∪ t, f x)
⊢ HMul.hMul (α := M) (∏ i ∈ t \ s, f i) (∏ i ∈ s, f i) = HMul.hMul (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t, f i)

Tactic:
rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
      sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]

Premises used: Finset.union_comm, Finset.prod_union, Finset.sdiff_union_self_eq_union
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq ι
inst_1 : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ Ne.{u_4 + 1} (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t \ s, f i) ↔ Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
prod_sdiff_eq_prod_sdiff_iff.not

Premises used: Iff.not, Finset.prod_sdiff_eq_prod_sdiff_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
G : Type u_3
s : Finset ι
a : ι
inst : CommGroup G
inst_1 : DecidableEq ι
ha : a ∉ s
f : ι → G
⊢ (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
G : Type u_3
s : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
rw : (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x
rw₁ rw₂ : Eq.{u_3 + 1} (α := G) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

Tactic:
rw [eq_div_iff_mul_eq', prod_erase_mul _ _ h]

Premises used: Finset.prod_erase_mul, eq_div_iff_mul_eq'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
base : f 0 / f 0 = 1
step : ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0

Tactic:
apply prod_range_induction

Premises used: Finset.prod_range_induction
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
base : f 0 / f 0 = 1
step : ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n

Tactic:
apply prod_range_induction

Premises used: Finset.prod_range_induction
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
rw : f n = f 0 * (f n / f 0)
rw₁ rw₂ : f n = f n
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Tactic:
rw [prod_range_div, mul_div_cancel]

Premises used: Finset.prod_range_div, mul_div_cancel
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
rw : f 0 * ∏ i ∈ range n, f (i + 1) / f i
| f n

Tactic:
rw [Finset.eq_prod_range_div f]

Premises used: Finset.eq_prod_range_div
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
conv_lhs : f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
⊢ f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
conv_lhs => rw [Finset.eq_prod_range_div f]

Premises used: Finset.eq_prod_range_div
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 * ∏ i ∈ range n, f (i + 1) / f i = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
simp [Finset.prod_range_succ', mul_comm]

Premises used: Finset.prod_range_succ', mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
G : Type u_3
inst : CommGroup G
f : ℕ → G
n m : ℕ
⊢ HDiv.hDiv (α := G) (∏ k ∈ range (n + m), f k) (∏ k ∈ range n, f k) = ∏ k ∈ range m, f (n + k)

Tactic:
div_eq_of_eq_mul' (prod_range_add f n m)

Premises used: div_eq_of_eq_mul', Finset.prod_range_add
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
rw : HMul.hMul (α := G) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁, f x) = ∏ x ∈ s₂, f x
rw₁ rw₂ : Eq.{u_3 + 1} (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₂, f x)
⊢ ∏ x ∈ s₂ \ s₁, f x = HDiv.hDiv (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₁, f x)

Tactic:
rw [eq_div_iff_mul_eq', prod_sdiff h]

Premises used: Finset.prod_sdiff, eq_div_iff_mul_eq'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst : CommGroup G
inst_1 : DecidableEq ι
f : ι → G
⊢ HDiv.hDiv (α := G) (∏ x ∈ s₂ \ s₁, f x) (∏ x ∈ s₁ \ s₂, f x) = HDiv.hDiv (α := G) (∏ x ∈ s₂, f x) (∏ x ∈ s₁, f x)

Tactic:
simp [← Finset.prod_sdiff (@inf_le_left _ _ s₁ s₂), ← Finset.prod_sdiff (@inf_le_right _ _ s₁ s₂)]

Premises used: inf_le_right, Finset.prod_sdiff, inf_le_left
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
apply : f 0 - f 0 = 0
apply₁ : ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

Tactic:
apply sum_range_induction

Premises used: Finset.sum_range_induction
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
h₁ : f 0 = 0 + f 0
⊢ f 0 - f 0 = 0

Tactic:
apply tsub_eq_of_eq_add

Premises used: tsub_eq_of_eq_add
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
h₁ h₂ : f 0 = f 0
⊢ f 0 = 0 + f 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 - f 0 = 0

Tactic:
case base => apply tsub_eq_of_eq_add; rw [zero_add]

Premises used: tsub_eq_of_eq_add, zero_add
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
_ : n < n_1 → f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)
⊢ n < n_1 → f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
⊢ f n ≤ f (n + 1)

Tactic:
have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
h₁ : f n ≤ f (n + 1)
⊢ f 0 ≤ f n

Tactic:
have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n_1 n : ℕ
h_1 : n < n_1
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
rw : f (n + 1) - f 0 = f n + (f (n + 1) - f n) - f 0
rw₁ rw₂ : f (n + 1) - f 0 = f (n + 1) - f 0
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Premises used: tsub_add_eq_add_tsub, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
case case₁ : ∀ n_1 < n, f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
case₂ : ∀ n_1 < n, ∀ (h₁ : f n_1 ≤ f (n_1 + 1)), f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
case₃ :
  ∀ n_1 < n, ∀ (h₁ : f n_1 ≤ f (n_1 + 1)) (h₂ : f 0 ≤ f n_1), f (n_1 + 1) - f 0 = f n_1 - f 0 + (f (n_1 + 1) - f n_1)
⊢ ∀ k < n, f (k + 1) - f 0 = f k - f 0 + (f (k + 1) - f k)

Tactic:
case step =>
    intro n _
    have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
    have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
    rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : AddLeftMono M
inst_5 : AddLeftReflectLE M
inst_6 : ExistsAddOfLE M
s : Finset ι
f g : ι → M
hfg : ∀ x ∈ s, g x ≤ f x
⊢ ∑ x ∈ s, (f x - g x) = HSub.hSub (α := M) (∑ x ∈ s, f x) (∑ x ∈ s, g x)

Tactic:
Multiset.sum_map_tsub _ hfg

Premises used: Multiset.sum_map_tsub, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
s : Finset ι
⊢ #s = ∑ x ∈ s, 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
rw : Eq (α := ℕ) (∑ x ∈ s, f x) (∑ _x ∈ s, m)
⊢ ∑ x ∈ s, f x = #s * m

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

Premises used: Nat.nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ Eq (α := ℕ) (∑ x ∈ s, f x) (∑ _x ∈ s, m)

Tactic:
apply sum_congr rfl h₁

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ j ∈ t, #({i ∈ s | g i = j}) = #({i ∈ s | g i ∈ t})

Tactic:
simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _

Premises used: Finset.card_eq_sum_ones, Finset.sum_fiberwise_eq_sum_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
t : ι → Finset M
h : (↑s : Set ι).PairwiseDisjoint t
⊢ #(s.disjiUnion t h) = ∑ a ∈ s, #(t a)

Tactic:
Multiset.card_bind _ _

Premises used: Multiset.sum, Multiset.foldr, Multiset.join, Finset.card, Multiset.card, Multiset.bind, Multiset.card_bind, Finset.sum
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : DecidableEq M
t : ι → Finset M
h : (↑s : Set ι).PairwiseDisjoint t
⊢ #(s.biUnion t) = ∑ u ∈ s, #(t u)

Tactic:
simpa using sum_biUnion h (M := ℕ) (f := 1)

Premises used: Finset.sum_biUnion
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s : Finset ι
t : ι → Finset M
this : DecidableEq ι
⊢ #(Finset.biUnion ∅ t) ≤ ∑ a ∈ ∅, #(t a)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s_1 : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
rw : #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
rw [biUnion_insert]

Premises used: Finset.biUnion_insert
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : DecidableEq M
s_1 : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
card_union_le ..

Premises used: Finset.card_union_le