awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1

Tactic:
suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
    ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
      (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃ (fun _ _ => hg₄ _ _)
-- 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
⊢ ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}

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

Tactic:
prod_involution (fun i _ => g i) (fun i _ => hg₁ i) (fun _ _ hi => hg₂ _ hi)
    (fun i _ => g_mem i) (fun i _ => hg₃ i)

Premises used: Finset.prod_involution
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst : CommMonoid M
inst_1 : DecidableEq κ
f : κ → M
g : ι → κ
simp_rw : Eq.{u_4 + 1} (α := M) (∏ a ∈ s, f (g a)) (∏ x ∈ image g s, ∏ _x ∈ s with g _x = x, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s, f (g a)) (∏ b ∈ image g s, f b ^ #({a ∈ s | g a = b}))

Tactic:
simp_rw [← prod_const, prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _]

Premises used: Finset.prod_fiberwise_of_maps_to', Finset.prod_const, Finset.mem_image_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y)

Tactic:
(Finset.prod_image' f fun x _hx => ?_).symm

Premises used: Finset.prod_image', Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
refine : ∀ (x : ι) (_hx : x ∈ s), Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y) (∏ j ∈ s with ⟦j⟧ = ⟦x⟧, f j)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y)

Tactic:
refine (Finset.prod_image' f fun x _hx => ?_).symm

Premises used: Finset.prod_image', Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
x : ι
_hx : x ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y) (∏ j ∈ s with ⟦j⟧ = ⟦x⟧, f j)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
h : ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ a ∈ s with (R : ι → ι → Prop) a x, f a) 1
rw : ∀ x ∈ image (Quotient.mk R) s, Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = x, f y) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
rw [prod_partition R, ← Finset.prod_eq_one]

Premises used: Finset.prod_eq_one, Finset.prod_partition
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
h : ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ a ∈ s with (R : ι → ι → Prop) a x, f a) 1
xbar : Quotient R
xbar_in_s : xbar ∈ image (Quotient.mk R) s
obtain :
  ∀ (x : ι) (x_in_s : x ∈ s) (xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s),
    Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = xbar, f y) 1

Tactic:
obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
h : ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ a ∈ s with (R : ι → ι → Prop) a x, f a) 1
x : ι
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
⊢ ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ x ∈ s with ⟦x⟧ = ⟦x⟧, f x) 1

Tactic:
simp only [← Quotient.eq] at h

Premises used: Quotient.eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
x : ι
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
h : ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ x ∈ s with ⟦x⟧ = ⟦x⟧, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y) 1

Tactic:
h x x_in_s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
R : Setoid ι
inst_1 : DecidableRel (α := ι) (⇑R : ι → ι → Prop)
x : ι
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
h : ∀ x ∈ s, Eq.{u_4 + 1} (α := M) (∏ x ∈ s with ⟦x⟧ = ⟦x⟧, f x) 1
⊢ Eq.{u_4 + 1} (α := M) (∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y) 1

Tactic:
exact h x x_in_s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
pos : ∀ (hc0 : #s = 0), f x = b
neg : ∀ (hc0 : ¬#s = 0), f x = b
⊢ f x = b

Tactic:
by_cases hc0 : #s = 0
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

Tactic:
False.elim (card_ne_zero_of_mem hx hc0)

Premises used: False.elim, Finset.card_ne_zero_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : #s = 0
⊢ f x = b

Tactic:
exact False.elim (card_ne_zero_of_mem hx hc0)

Premises used: False.elim, Finset.card_ne_zero_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
⊢ #s = 1

Tactic:
have h1 : #s = 1 := le_antisymm hc (Nat.one_le_of_lt (Nat.pos_of_ne_zero hc0))
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
h1 : #s = 1
⊢ ∃ (a : ι), s = {a}

Tactic:
rw [card_eq_one] at h1

Premises used: Finset.card_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
h1 : ∃ (a : ι), s = {a}
⊢ f x = b

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ insert a (s.erase a), f x) (∏ x ∈ s, f x)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
rw [← prod_insert (notMem_erase a s), insert_erase h]

Premises used: Finset.prod_insert, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
rw : f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x

Tactic:
rw [mul_comm, mul_prod_erase s f h]

Premises used: Finset.mul_prod_erase, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {a}, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.erase a, f x) (∏ x ∈ s, f x)

Tactic:
rw [← sdiff_singleton_eq_erase]

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

Tactic:
prod_subset sdiff_subset fun x hx hnx => ?_

Premises used: Finset.prod_subset, Finset.sdiff_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
refine : ∀ (x : ι) (hx : x ∈ s) (hnx : x ∉ s \ {a}), f x = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {a}, f x) (∏ x ∈ s, f x)

Tactic:
refine prod_subset sdiff_subset fun x hx hnx => ?_

Premises used: Finset.prod_subset, Finset.sdiff_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
x : ι
hx : x ∈ s
hnx : x ∉ s \ {a}
⊢ f x = 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid κ
inst_2 : LT κ
inst_3 : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
rw : ∏ m ∈ insert d (s.erase d), f m
| ∏ m ∈ s, f m

Tactic:
rw [← Finset.insert_erase hd]

Premises used: Finset.insert_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid κ
inst_2 : LT κ
inst_3 : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
conv : LT.lt.{u_5} (α := κ) (∏ m ∈ s.erase d, f m) (∏ m ∈ insert d (s.erase d), f m)
⊢ LT.lt.{u_5} (α := κ) (∏ m ∈ s.erase d, f m) (∏ m ∈ s, f m)

Tactic:
conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]

Premises used: Finset.insert_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid κ
inst_2 : LT κ
inst_3 : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
rw : ∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x
⊢ LT.lt.{u_5} (α := κ) (∏ m ∈ s.erase d, f m) (∏ m ∈ insert d (s.erase d), f m)

Tactic:
rw [Finset.prod_insert (Finset.notMem_erase d s)]

Premises used: Finset.prod_insert, Finset.notMem_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid κ
inst_2 : LT κ
inst_3 : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x

Tactic:
lt_mul_of_one_lt_left' _ hdf

Premises used: lt_mul_of_one_lt_left'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
κ : Type u_5
inst : DecidableEq ι
inst_1 : CommMonoid κ
inst_2 : LT κ
inst_3 : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < f d * ∏ x ∈ s.erase d, f x

Tactic:
exact lt_mul_of_one_lt_left' _ hdf

Premises used: lt_mul_of_one_lt_left'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
pos : ∀ (h : x = a), f x = 1
neg : ∀ (h : ¬x = a), f x = 1
⊢ f x = 1

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

Tactic:
rw [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ a ∈ s

Tactic:
rw [h] at hx
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
hx₁ : a ∈ s
⊢ x = a

Tactic:
rw [h] at hx
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
pos : ∀ (hp : f a = 1) (h1 : ∀ x ∈ s, x ≠ a → f x = 1) (x : ι) (hx : a ∈ s) (h : x = a), f a = 1
⊢ f a = 1

Tactic:
rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.prod_singleton, Finset.singleton_subset_iff, Finset.prod_subset, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1

Tactic:
hp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : f a = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1

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

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

Tactic:
exact h1 x hx h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
pos : ∀ (h : x = a), f x = 1
neg neg₁ : ∀ (h : ¬x = a), f x = 1
⊢ f x = 1

Tactic:
classical
    by_cases h : x = a
    · rw [h]
      rw [h] at hx
      rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (notMem_singleton.1 ha),
        prod_singleton] at hp
      exact hp
    · exact h1 x hx h

Premises used: Finset.prod_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
rw [← insert_erase ha]

Premises used: Finset.insert_erase
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
simp : (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂

Tactic:
simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]

Premises used: Finset.prod_insert, false_and, not_true_eq_false, ne_eq, Finset.mem_erase, not_false_eq_true
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw : f a * ((∏ a ∈ s.erase a, f a) * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₁ : (∏ a ∈ s.erase a, f a) * b₁ * f a = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₂ : (∏ a ∈ s.erase a, f a) * (b₁ * f a) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₃ : (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₄ : (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₅ : (∏ a ∈ s.erase a, f a) * f a * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
rw₆ rw₇ : (f a * ∏ a ∈ s.erase a, f a) * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
rw rw₁ rw₂ : (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
rw₃ : (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
classical
  rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

Premises used: Finset.prod_insert, mul_assoc, false_and, not_true_eq_false, ne_eq, Finset.mem_erase, mul_comm, not_false_eq_true
-- 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}
⊢ s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}

Tactic:
grind
-- 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}
⊢ s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}

Tactic:
have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
-- 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}
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, ∏ i ∈ t' x, f i) (∏ x ∈ s, ∏ i ∈ t x, f i)
rw₁ : (↑s : Set κ).PairwiseDisjoint t'
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.biUnion t, f x) (∏ x ∈ s, ∏ i ∈ t x, f i)

Tactic:
rw [← prod_filter_ne_one, ← this, prod_biUnion]

Premises used: Finset.prod_biUnion, Finset.prod_filter_ne_one
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
⊢ k ∈ t' i

Tactic:
have hki : k ∈ t' i := hai hk
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
⊢ k ∈ t' j

Tactic:
have hkj : k ∈ t' j := haj hk
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
hkj : k ∈ t' j
⊢ k ∈ t i ∧ ¬f k = 1

Tactic:
simp only [ne_eq, mem_filter, t'] at hki hkj

Premises used: ne_eq, Finset.mem_filter
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t' i
hkj : k ∈ t' j
hki₁ : k ∈ t i ∧ ¬f k = 1
⊢ k ∈ t j ∧ ¬f k = 1

Tactic:
simp only [ne_eq, mem_filter, t'] at hki hkj

Premises used: ne_eq, Finset.mem_filter
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ k ∈ t i ∩ t j

Tactic:
grind
-- 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}
i : κ
hi : i ∈ (↑s : Set κ)
j : κ
hj : j ∈ (↑s : Set κ)
hij : i ≠ j
a : Finset ι
hai : a ≤ t' i
haj : a ≤ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ Membership.mem (γ := Finset ι) ⊥ k

Tactic:
exact (hki.2 (hs hi hj hij k (by grind))).elim

Premises used: False.elim, And.right
-- 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:
Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

Premises used: Finset.prod_filter_ne_one, Finset.prod_congr, rfl