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
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
⊢ ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b

Tactic:
(mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_

Premises used: And.elim, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
⊢ b ∈ t

Tactic:
refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_

Premises used: And.elim, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
⊢ g b ≠ 1

Tactic:
refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_

Premises used: And.elim, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
H : g b = 1
⊢ Ne.{u_4 + 1} (α := M) 1 1

Tactic:
rw [H] at h₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
H : g b = 1
h₃ : Ne.{u_4 + 1} (α := M) 1 1
⊢ g b = 1

Tactic:
rw [H] at h₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : Ne.{u_4 + 1} (α := M) 1 1
H : g b = 1
⊢ False

Tactic:
simp at h₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
calc_3 :
  ∀ (a : ι) (ha₁ : a ∈ s) (ha₂ : f a ≠ 1) (eq : i a ha₁ ha₂ = b),
    ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b
⊢ ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b

Tactic:
obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
a : ι
ha₁ : a ∈ s
ha₂ : f a ≠ 1
eq : i a ha₁ ha₂ = b
⊢ ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b

Tactic:
⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
a : ι
ha₁ : a ∈ s
ha₂ : f a ≠ 1
eq : i a ha₁ ha₂ = b
⊢ ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b

Tactic:
exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
x : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s with f x ≠ 1, f x)
calc_1 :
  ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha ∈ {x ∈ t | g x ≠ 1}
calc_2 :
  ∀ (a₁ : ι) (ha₁ : a₁ ∈ {x ∈ s | f x ≠ 1}) (a₂ : ι) (ha₂ : a₂ ∈ {x ∈ s | f x ≠ 1}),
    Eq.{u_2 + 1} (α := κ) ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a₁ ha₁)
        ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a₂ ha₂) →
      a₁ = a₂
calc_3 :
  ∀ b ∈ {x ∈ t | g x ≠ 1},
    ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b
calc_4 : ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha)
calc_2₁ :
  ∀ (a₁ : ι) (ha₁ : a₁ ∈ {x ∈ s | f x ≠ 1}) (a₂ : ι) (ha₂ : a₂ ∈ {x ∈ s | f x ≠ 1}),
    Eq.{u_2 + 1} (α := κ) ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a₁ ha₁)
        ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a₂ ha₂) →
      a₁ = a₂
calc_3₁ :
  ∀ b ∈ {x ∈ t | g x ≠ 1},
    ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b
calc_4₁ : ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha)
calc_3₂ :
  ∀ b ∈ {x ∈ t | g x ≠ 1},
    ∃ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha = b
calc_4₂ calc_4₃ :
  ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g ((fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
classical
  calc
    ∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x := by rw [prod_filter_ne_one]
    _ = ∏ x ∈ t with g x ≠ 1, g x :=
      prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2)
        ?_ ?_ ?_ ?_
    _ = ∏ x ∈ t, g x := prod_filter_ne_one _
  · grind
  · solve_by_elim
  · intro b hb
    refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_
    obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
    exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
  · solve_by_elim

Premises used: Finset.prod_filter_ne_one, And.left, Iff.mp, Finset.mem_filter, Finset.prod_bij
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
h : Ne.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
contrapose! : ∀ (h : ∀ (a : ι) (_ : a ∈ s), f a = 1), Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
h : ∀ (a : ι) (_ : a ∈ s), f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
prod_eq_one h

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
h : ∀ (a : ι) (_ : a ∈ s), f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
exact prod_eq_one h

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
rw : ∏ x ∈ insert n (range n), f x = f n * ∏ x ∈ range n, f x
rw₁ rw₂ : f n * ∏ x ∈ range n, f x = f n * ∏ x ∈ range n, f x
⊢ ∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x

Tactic:
rw [range_add_one, prod_insert notMem_range_self]

Premises used: Finset.prod_insert, Finset.range_add_one, Finset.notMem_range_self
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

Tactic:
simp only [mul_comm, prod_range_succ_comm]

Premises used: Finset.prod_range_succ_comm, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
rw : ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f (n + 1) * f 0
rw₁ : ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f 0 * f (n + 1)
rw₂ : ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f k) * f (n + 1)
rw₃ rw₄ : (∏ x ∈ range (n + 1), f x) * f (n + 1) = (∏ k ∈ range (n + 1), f k) * f (n + 1)
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

Premises used: mul_right_comm, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
n : ℕ
hn : N ≤ n
obtain : ∀ (m : ℕ) (hn : N ≤ N + m), Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range n, u k) (∏ k ∈ range N, u k)

Tactic:
obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + 0), u k) (∏ k ∈ range N, u k)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
hm : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + (m + 1)), u k) (∏ k ∈ range N, u k)

Tactic:
simp [← add_assoc, prod_range_succ, hm, hu]

Premises used: add_assoc, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
zero : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + 0), u k) (∏ k ∈ range N, u k)
succ :
  ∀ (m : ℕ) (hm : Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)),
    Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + (m + 1)), u k) (∏ k ∈ range N, u k)
⊢ Eq.{u_4 + 1} (α := M) (∏ k ∈ range (N + m), u k) (∏ k ∈ range N, u k)

Tactic:
induction m with
  | zero => simp
  | succ m hm => simp [← add_assoc, prod_range_succ, hm, hu]

Premises used: Fin.succ, add_assoc, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 0), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range 0, f (n + x))

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))
succ : ∏ x ∈ range (n + m).succ, f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₁ :
  (∏ x ∈ range (n + m), f x) * f (n + m) = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
succ₂ : (∏ x ∈ range (n + m), f x) * f (n + m) = (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
succ₃ :
  HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x)) * f (n + m) =
    (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
succ₄ succ₅ :
  (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m)) =
    (∏ x ∈ range n, f x) * ((∏ x ∈ range m, f (n + x)) * f (n + m))
⊢ ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))

Tactic:
rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Premises used: mul_assoc, Nat.add_succ, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n m : ℕ
zero : ∏ x ∈ range (n + 0), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range 0, f (n + x))
succ :
  ∀ (m : ℕ) (hm : ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))),
    ∏ x ∈ range (n + (m + 1)), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range (m + 1), f (n + x))
⊢ ∏ x ∈ range (n + m), f x = HMul.hMul (α := M) (∏ x ∈ range n, f x) (∏ x ∈ range m, f (n + x))

Tactic:
induction m with
  | zero => simp
  | succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Premises used: Fin.succ, mul_assoc, Nat.add_succ, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
rw : ∏ k ∈ {0}, f k = f 0
rw₁ rw₂ : f 0 = f 0
⊢ ∏ k ∈ range 1, f k = f 0

Tactic:
rw [range_one, prod_singleton]

Premises used: Finset.prod_singleton, Finset.range_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
⊢ (List.map f []).prod = ∏ m ∈ toFinset [], f m ^ count m []

Tactic:
simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]

Premises used: pow_zero, List.count_nil, Finset.prod_const_one, List.prod_nil, List.map_nil
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
cons : f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
⊢ (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)

Tactic:
simp only [List.map, List.prod_cons, toFinset_cons, IH]

Premises used: List.map, List.toFinset_cons, List.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
pos :
  ∀ (has : a ∈ s.toFinset), f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
neg :
  ∀ (has : a ∉ s.toFinset), f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
by_cases has : a ∈ s.toFinset

Premises used: List.toFinset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
pos :
  f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']

Premises used: Finset.prod_insert, mul_assoc, Finset.insert_eq_of_mem, List.count_cons_self, Finset.notMem_erase, Finset.insert_erase, pow_succ'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
pos :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s.toFinset.erase a, f x ^ count x s) (∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s))
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
congr 1
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.toFinset.erase a, f x ^ count x s) (∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s))

Tactic:
prod_congr rfl fun x hx => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
pos : ∀ (x : ι) (hx : x ∈ s.toFinset.erase a), f x ^ count x s = f x ^ count x (a :: s)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.toFinset.erase a, f x ^ count x s) (∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s))

Tactic:
refine prod_congr rfl fun x hx => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
x : ι
hx : x ∈ s.toFinset.erase a
pos pos₁ : f x ^ count x s = f x ^ count x s
⊢ f x ^ count x s = f x ^ count x (a :: s)

Tactic:
rw [count_cons_of_ne (ne_of_mem_erase hx).symm]

Premises used: List.count_cons_of_ne, Finset.ne_of_mem_erase, Ne.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
neg : f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]

Premises used: List.mem_toFinset, Iff.mpr, Finset.prod_insert, mt, pow_one, List.count_eq_zero_of_not_mem, List.count_cons_self
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Tactic:
grind [Finset.prod_congr]

Premises used: Finset.prod_congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
l : List ι
f : ι → M
nil : (List.map f []).prod = ∏ m ∈ toFinset [], f m ^ count m []
cons :
  ∀ (a : ι) (s : List ι) (IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s),
    (List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)
⊢ (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ count m l

Tactic:
induction l with
  | nil => simp only [map_nil, prod_nil, count_nil, pow_zero, prod_const_one]
  | cons a s IH =>
  simp only [List.map, List.prod_cons, toFinset_cons, IH]
  by_cases has : a ∈ s.toFinset
  · rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]
  rw [prod_insert has, count_cons_self, count_eq_zero_of_not_mem (mt mem_toFinset.2 has), pow_one]
  grind [Finset.prod_congr]

Premises used: Finset.prod_insert, Finset.cons, List.map, mul_assoc, Finset.prod_congr, pow_zero, List.count_nil, Finset.prod_const_one, pow_one, List.prod_nil, List.count_cons_self, List.toFinset_cons, Finset.notMem_erase, List.prod_cons, pow_succ', rfl, List.map_nil, List.nil
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : List M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ count m s

Tactic:
simpa using prod_list_map_count s id

Premises used: Finset.prod_list_map_count, id
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
rw : Eq (α := M) (∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m) (∏ i ∈ s, i ^ count i m)
⊢ m.prod = ∏ i ∈ s, i ^ count i m

Tactic:
rw [prod_list_count]

Premises used: Finset.prod_list_count
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
⊢ Eq (α := M) (∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m) (∏ i ∈ s, i ^ count i m)

Tactic:
prod_subset hs fun x _ hx => ?_

Premises used: Finset.prod_subset