awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ x ∈ s, ∀ (hx : x ∉ m.toFinset), x ^ count x m = 1
⊢ Eq (α := M) (∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m) (∏ i ∈ s, i ^ count i m)

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

Premises used: Finset.prod_subset
-- 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
x : M
h : x ∈ s
hx : x ∉ m.toFinset
⊢ x ∉ m

Tactic:
rw [mem_toFinset] at hx

Premises used: List.mem_toFinset
-- 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
x : M
h : x ∈ s
hx : x ∉ m
rw : HPow.hPow (β := ℕ) x 0 = 1
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 1 1
⊢ x ^ count x m = 1

Tactic:
rw [count_eq_zero_of_not_mem hx, pow_zero]

Premises used: pow_zero, List.count_eq_zero_of_not_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
M : Type u_5
inst_1 : CommMonoid M
f : ι → M
⊢ (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s

Tactic:
Quot.induction_on s fun l => ?_

Premises used: Quot.induction_on
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
M : Type u_5
inst_1 : CommMonoid M
f : ι → M
refine :
  ∀ (l : List ι),
    (Multiset.map f (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)).prod =
      ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l),
        f m ^ Multiset.count m (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)
⊢ (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s

Tactic:
refine Quot.induction_on s fun l => ?_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Multiset ι
M : Type u_5
inst_1 : CommMonoid M
f : ι → M
l : List ι
⊢ (Multiset.map f (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)).prod =
    ∏ m ∈ Multiset.toFinset (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l),
      f m ^ Multiset.count m (Quot.mk (⇑(isSetoid ι) : List ι → List ι → Prop) l)

Tactic:
simp [prod_list_map_count l f]

Premises used: Finset.prod_list_map_count
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : Multiset M
⊢ (Multiset.map id s).prod = ∏ m ∈ s.toFinset, id m ^ Multiset.count m s

Tactic:
prod_multiset_map_count s id

Premises used: Finset.prod_multiset_map_count, id
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : Multiset M
h : s = Multiset.map id s
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s

Tactic:
convert! prod_multiset_map_count s id

Premises used: Finset.prod_multiset_map_count, id
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
s : Multiset M
h h₁ : s = s
⊢ s = Multiset.map id s

Tactic:
rw [Multiset.map_id]

Premises used: Multiset.map_id
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
hs : m.toFinset ⊆ s
revert : ∀ (hs : m.toFinset ⊆ s), m.prod = ∏ i ∈ s, i ^ Multiset.count i m
⊢ m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
revert hs
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
⊢ ∀ (hs : m.toFinset ⊆ s), m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
Quot.induction_on m fun l => ?_

Premises used: Quot.induction_on
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
refine :
  ∀ (l : List M) (hs : Multiset.toFinset (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) ⊆ s),
    Multiset.prod (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) =
      ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l)
⊢ ∀ (hs : m.toFinset ⊆ s), m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
refine Quot.induction_on m fun l => ?_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
l : List M
simp : ∀ (hs : (↑l : Multiset M).toFinset ⊆ s), l.prod = ∏ x ∈ s, x ^ List.count x l
⊢ ∀ (hs : Multiset.toFinset (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) ⊆ s),
    Multiset.prod (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l) =
      ∏ i ∈ s, i ^ Multiset.count i (Quot.mk (⇑(isSetoid M) : List M → List M → Prop) l)

Tactic:
simp only [quot_mk_to_coe'', prod_coe, coe_count]

Premises used: Multiset.coe_count, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq M
m : Multiset M
s : Finset M
l : List M
⊢ ∀ (hs : (↑l : Multiset M).toFinset ⊆ s), l.prod = ∏ x ∈ s, x ^ List.count x l

Tactic:
apply prod_list_count_of_subset l s

Premises used: Finset.prod_list_count_of_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
step : ∀ k < 0, s (k + 1) = s k * f k
zero : 1 = s 0
zero₁ zero₂ : Eq.{u_4 + 1} (α := M) 1 1
⊢ ∏ k ∈ range 0, f k = s 0

Tactic:
rw [Finset.prod_range_zero, base]

Premises used: Finset.prod_range_zero
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
succ : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1
⊢ ∏ k ∈ range (k + 1), f k = s (k + 1)

Tactic:
rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]

Premises used: Nat.lt_succ_self, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1

Tactic:
fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1

Tactic:
exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
zero : ∀ (step : ∀ k < 0, s (k + 1) = s k * f k), ∏ k ∈ range 0, f k = s 0
succ :
  ∀ (k : ℕ) (hk : ∀ (step : ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range k, f k = s k)
    (step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1), ∏ k ∈ range (k + 1), f k = s (k + 1)
⊢ ∏ k ∈ range n, f k = s n

Tactic:
induction n with
  | zero => rw [Finset.prod_range_zero, base]
  | succ k hk =>
    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)

Premises used: Fin.succ, Finset.prod_range_zero, Finset.prod_range_succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
b : M
⊢ ∏ _x ∈ s, b = b ^ #s

Tactic:
(congr_arg _ <| s.val.map_const b).trans <| Multiset.prod_replicate #s b

Premises used: Multiset.prod_replicate, Multiset.map_const, Finset.val, Finset.prod, congr_arg, Finset.card, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
b : M
hf : ∀ a ∈ s, f a = b
⊢ ∏ a ∈ s, f a = b ^ #s

Tactic:
(prod_congr rfl hf).trans <| prod_const _

Premises used: Finset.prod_congr, Finset.prod_const, rfl, Eq.trans
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
b : M
⊢ b ^ #s * ∏ a ∈ s, f a = ∏ a ∈ s, b * f a

Tactic:
(Finset.prod_const b).symm ▸ prod_mul_distrib.symm

Premises used: Finset.prod_mul_distrib, Eq.rec, Finset.prod_const, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
b : M
⊢ (∏ a ∈ s, f a) * b ^ #s = ∏ a ∈ s, f a * b

Tactic:
(Finset.prod_const b).symm ▸ prod_mul_distrib.symm

Premises used: Finset.prod_mul_distrib, Eq.rec, Finset.prod_const, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
b : M
⊢ ∀ (n : ℕ), b ^ n = ∏ _k ∈ range n, b

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → ℕ
a : M
⊢ ∏ i ∈ ∅, a ^ f i = HPow.hPow (β := ℕ) a (∑ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → ℕ
a : M
x : ι
x_1 : Finset ι
h : x ∉ x_1
h_1 : ∏ i ∈ x_1, a ^ f i = HPow.hPow (β := ℕ) a (∑ i ∈ x_1, f i)
⊢ ∏ i ∈ cons x x_1 h, a ^ f i = HPow.hPow (β := ℕ) a (∑ i ∈ cons x x_1 h, f i)

Tactic:
simp [prod_cons, sum_cons, pow_add, *]

Premises used: Finset.sum_cons, pow_add, Finset.prod_cons
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
zero : f (HSub.hSub (α := ℕ) 0 0) = ∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k
zero₁ zero₂ : f (HSub.hSub (α := ℕ) 0 0) = f 0
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)

Tactic:
rw [prod_range_one, prod_range_one]

Premises used: Finset.prod_range_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
ih : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)
succ : (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1 + 1), f (n + 1 - r)) (∏ k ∈ range (n + 1 + 1), f k)

Tactic:
rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]

Premises used: Finset.prod_range_succ', Finset.prod_range_succ, Nat.succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
f : ℕ → M
n : ℕ
ih : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)
⊢ (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ

Tactic:
simp [← ih]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
M : Type u_4
inst : CommMonoid M
n : ℕ
f : ℕ → M
zero :
  Eq.{u_4 + 1} (α := M) (∏ r ∈ range (HAdd.hAdd (α := ℕ) 0 1), f (0 - r)) (∏ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), f k)
succ :
  ∀ (n : ℕ) (ih : Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)),
    Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1 + 1), f (n + 1 - r)) (∏ k ∈ range (n + 1 + 1), f k)
⊢ Eq.{u_4 + 1} (α := M) (∏ r ∈ range (n + 1), f (n - r)) (∏ k ∈ range (n + 1), f k)

Tactic:
induction n with
  | zero => rw [prod_range_one, prod_range_one]
  | succ n ih =>
    rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
    simp [← ih]

Premises used: Finset.prod_range_succ', Fin.succ, Finset.prod_range_one, Finset.prod_range_succ, Nat.succ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
?_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
H :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
induction s using Finset.strongInduction with | H s ih => ?_

Premises used: Finset.strongInduction
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
H :
  ∀
    (ih :
      ∀ t ⊂ ∅,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → Membership.mem (γ := Finset ι) ∅ a → ι)
    (hg₁ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a ≠ 1 → g a ha ≠ a)
    (g_mem : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), Membership.mem (γ := Finset ι) ∅ (g a ha))
    (hg₄ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), g (g a ha) ⋯ = a),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ ∅, f x) 1
H₁ : ∀ (x : ι) (hx : x ∈ s), Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
ih :
  ∀ t ⊂ ∅,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → Membership.mem (γ := Finset ι) ∅ a → ι
hg₁ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), Membership.mem (γ := Finset ι) ∅ (g a ha)
hg₄ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), g (g a ha) ⋯ = a
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ ∅, f x) 1

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ {x, g x hx} ⊆ s

Tactic:
simp [insert_subset_iff, hx, g_mem]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ {x, g x hx} ⊆ s

Tactic:
have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ {x, g x hx}, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
rw [← prod_sdiff this, h, one_mul]

Premises used: Finset.prod_sdiff, one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
hx' : g x hx = x
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ {x, g x hx}, f x) 1

Tactic:
simpa [hx'] using hg₃ x hx
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
hx' : g x hx ≠ x
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ {x, g x hx}, f x) 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
⊢ g x hx = x ∨ g x hx ≠ x

Tactic:
cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind

Premises used: eq_or_ne
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
H : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1 by
    rw [← prod_sdiff this, h, one_mul]
    cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ x ∉ s \ {x, g x hx} ∧ insert x (s \ {x, g x hx}) ⊆ s

Tactic:
simp [insert_subset_iff, hx]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s_1 : Finset ι
inst : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
      (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
      (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), f a * f (g a ⋯) = 1

Tactic:
simp [hg₁]