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
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
j : κ
h : j ∈ t
i : ι
hi : i ∈ {i ∈ s | g i = j}
rw rw₁ : f j = f j
⊢ f j = f (g i)

Tactic:
rw [(mem_filter.1 hi).2]

Premises used: And.right, 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
inst_1 : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i)) (∏ i ∈ s with g i ∈ t, f (g i))

Tactic:
prod_fiberwise_eq_prod_filter _ _ _ _

Premises used: Finset.prod_fiberwise_eq_prod_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 κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f j) (∏ i ∈ s with g i ∈ t, f (g i))

Tactic:
calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
    _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _

Premises used: Finset.prod_congr, rfl, Finset.prod_fiberwise_eq_prod_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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
h₁ : Set.PairwiseDisjoint.{u_1, u_2} (α := Finset ι) (↑t : Set κ) fun (j : κ) ↦ {i ∈ s | g i = j}
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f i) (∏ i ∈ s, f i)

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]

Premises used: Finset.disjiUnion_filter_eq_of_maps_to, Finset.prod_disjiUnion
-- 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ (↑t : Set κ)
y' : κ
hy : y' ∈ (↑t : Set κ)
hne : x' ≠ y'
h₁ : ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
⊢ onFun.{u_2 + 1, u_1 + 1, 1} (β := Finset ι) Disjoint (fun (j : κ) ↦ {i ∈ s | g i = j}) x' y'

Tactic:
simp_rw [disjoint_left, mem_filter]

Premises used: Finset.mem_filter, Finset.disjoint_left
-- 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
i : ι
left : i ∈ s
hx : g i ∈ (↑t : Set κ)
left_1 : i ∈ s
hy : g i ∈ (↑t : Set κ)
hne : g i ≠ g i
⊢ False

Tactic:
hne rfl

Premises used: rfl
-- 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
i : ι
left : i ∈ s
hx : g i ∈ (↑t : Set κ)
left_1 : i ∈ s
hy : g i ∈ (↑t : Set κ)
hne : g i ≠ g i
⊢ False

Tactic:
exact hne rfl

Premises used: rfl
-- 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
h_1 : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
rw rw₁ : f y = f y
⊢ f y = f (g x)

Tactic:
rw [(mem_filter.1 hx).2]

Premises used: And.right, 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i)) (∏ i ∈ s, f (g i))

Tactic:
prod_fiberwise_of_maps_to h _

Premises used: Finset.prod_fiberwise_of_maps_to
-- 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 κ
inst_1 : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ t, ∏ i ∈ s with g i = j, f j) (∏ i ∈ s, f (g i))

Tactic:
calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
    _ = _ := prod_fiberwise_of_maps_to h _

Premises used: Finset.prod_fiberwise_of_maps_to, 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
inst_1 : DecidableEq κ
inst_2 : Fintype κ
s : Finset ι
g : ι → κ
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i ∈ s with g i = j, f i) (∏ i ∈ s, f i)

Tactic:
prod_fiberwise_of_maps_to (fun _ _ ↦ mem_univ _) _

Premises used: Finset.mem_univ, Finset.prod_fiberwise_of_maps_to
-- 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 : Fintype κ
s : Finset ι
g : ι → κ
f : κ → M
⊢ Eq.{u_4 + 1} (α := M) (∏ j : κ, ∏ i ∈ s with g i = j, f j) (∏ i ∈ s, f (g i))

Tactic:
prod_fiberwise_of_maps_to' (fun _ _ ↦ mem_univ _) _

Premises used: Finset.mem_univ, Finset.prod_fiberwise_of_maps_to'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι × ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s.diag, f i) (∏ i ∈ s, f (i, i))

Tactic:
simp [diag]

Premises used: Finset.diag
-- 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 κ
g : κ → ι
h : κ → M
eq : ∀ i ∈ s, f (g i) = ∏ j ∈ s with g j = g i, h j
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ image g s, f a) (∏ i ∈ s, h i)

Tactic:
calc
    ∏ a ∈ s.image g, f a = ∏ a ∈ s.image g, ∏ j ∈ s with g j = a, h j :=
      (prod_congr rfl) fun _a hx =>
        let ⟨i, his, hi⟩ := mem_image.1 hx
        hi ▸ eq i his
    _ = ∏ i ∈ s, h i := prod_fiberwise_of_maps_to (fun _ => mem_image_of_mem g) _

Premises used: Trans.trans, Finset.mem_image, Finset.prod_fiberwise_of_maps_to, _private.0.Finset.prod_image'.match_1, Eq.rec, Finset.prod_congr, Finset.prod, Iff.mp, Finset.mem_image_of_mem, Finset.filter, Eq, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g : ι → M
rw : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x * g x) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x * g x) s)
⊢ ∏ x ∈ s, f x * g x = fold (fun (x1 x2 : M) ↦ x1 * x2) (HMul.hMul (α := M) 1 1) (fun (x : ι) ↦ f x * g x) s

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x * g x) (fold (fun (x1 x2 : M) ↦ x1 * x2) 1 (fun (x : ι) ↦ f x * g x) s)

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f g h i : ι → M
simp_rw :
  HMul.hMul (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, g x) * HMul.hMul (α := M) (∏ x ∈ s, h x) (∏ x ∈ s, i x) =
    HMul.hMul (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, h x) * HMul.hMul (α := M) (∏ x ∈ s, g x) (∏ x ∈ s, i x)
⊢ HMul.hMul (α := M) (∏ a ∈ s, f a * g a) (∏ a ∈ s, h a * i a) =
    HMul.hMul (α := M) (∏ a ∈ s, f a * h a) (∏ a ∈ s, g a * i a)

Tactic:
simp_rw [prod_mul_distrib, mul_mul_mul_comm]

Premises used: Finset.prod_mul_distrib, mul_mul_mul_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
rw : x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1

Tactic:
rw [not_imp_comm, mem_filter]

Premises used: not_imp_comm, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x

Tactic:
simpa using hp _ h₁ h₂
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x

Tactic:
exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
p : ι → Prop
inst_1 : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
rw : x ∈ s → ¬f x = 1 → x ∈ {x ∈ s | p x}
rw₁ rw₂ rw₃ : x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
⊢ x ∈ s → x ∉ {x ∈ s | p x} → f x = 1

Tactic:
classical
      rw [not_imp_comm, mem_filter]
      exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩

Premises used: not_imp_comm, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset ι
inst_1 : (x : ι) → Decidable (f x ≠ 1)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s with f x ≠ 1, f x) (∏ x ∈ s, f x)

Tactic:
prod_filter_of_ne fun _ _ => id

Premises used: id, Finset.prod_filter_of_ne
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
hc : p a
⊢ f a = if p a then f a else 1

Tactic:
rw [if_pos]

Premises used: if_pos
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ p a

Tactic:
simpa using (mem_filter.1 h).2

Premises used: And.right, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)

Tactic:
prod_subset (filter_subset _ s) fun x hs h => ?_

Premises used: Finset.filter_subset, Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
refine : ∀ (x : ι) (hs : x ∈ s) (h : x ∉ {a ∈ s | p a}), (if p x then f x else 1) = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)

Tactic:
refine prod_subset (filter_subset _ s) fun x hs h => ?_

Premises used: Finset.filter_subset, Finset.prod_subset
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∉ {a ∈ s | p a}
⊢ x ∈ s → ¬p x

Tactic:
rw [mem_filter, not_and] at h

Premises used: Finset.mem_filter, not_and
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x

Tactic:
simpa using h hs
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ (if p x then f x else 1) = 1

Tactic:
exact if_neg (by simpa using h hs)

Premises used: if_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f : ι → M
refine : ∀ (x : ι) (hs : x ∈ s) (h : x ∉ {a ∈ s | p a}), (if p x then f x else 1) = 1
refine₁ : ∀ (x : ι) (hs : x ∈ s) (h : x ∈ s → ¬p x), (if p x then f x else 1) = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s with p a, if p a then f a else 1) (∏ a ∈ s, if p a then f a else 1)

Tactic:
{ refine prod_subset (filter_subset _ s) fun x hs h => ?_
        rw [mem_filter, not_and] at h
        exact if_neg (by simpa using h hs) }

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

Tactic:
(prod_subset ?_ ?_).symm

Premises used: Finset.prod_subset, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
refine_1 : {a} ⊆ s
refine_2 : ∀ x ∈ s, x ∉ {a} → f x = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)

Tactic:
refine (prod_subset ?_ ?_).symm

Premises used: Finset.prod_subset, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
a_1 : ι
H : Membership.mem (γ := Finset ι) {a} a_1
refine_1 refine_1₁ refine_1₂ refine_1₃ : a ∈ s
⊢ a_1 ∈ s

Tactic:
rwa [mem_singleton.1 H]

Premises used: Finset.mem_singleton, 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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1

Tactic:
simpa only [mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
refine_1 : {a} ⊆ s
refine_2 refine_2₁ : ∀ x ∈ s, x ∉ {a} → f x = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)

Tactic:
{ refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }

Premises used: Finset.mem_singleton, Finset.prod_subset, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ {a}, f x = f a

Tactic:
prod_singleton _ _

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
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
x : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ {a}, f x)
⊢ ∏ x ∈ s, f x = f a

Tactic:
calc
    ∏ x ∈ s, f x = ∏ x ∈ {a}, f x := by
      { refine (prod_subset ?_ ?_).symm
        · intro _ H
          rwa [mem_singleton.1 H]
        · simpa only [mem_singleton] }
    _ = f a := prod_singleton _ _

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
this_1 : DecidableEq ι
b : ι
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Tactic:
this hb
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
this_1 : DecidableEq ι
b : ι
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Tactic:
exact this hb
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ι → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
rw : Eq.{u_4 + 1} (α := M) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
⊢ Eq.{u_4 + 1} (α := M) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)

Tactic:
rw [← Finset.prod_filter]

Premises used: Finset.prod_filter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ι → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
e_s : {a : ι | a ∈ s} = s
⊢ Eq.{u_4 + 1} (α := M) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ι → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ {a : ι | a ∈ s} = s

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₀ : ∀ b ∈ s, b ≠ a → f b = 1
pos : ∀ (h : a ∈ s), ∏ x ∈ s, f x = if a ∈ s then f a else 1
neg : ∀ (h : a ∉ s), ∏ x ∈ s, f x = if a ∈ s then f a else 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
by_cases h : a ∈ s
-- 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₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∈ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
simp [Finset.prod_eq_single_of_mem a h h₀, h]

Premises used: Finset.prod_eq_single_of_mem
-- 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₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∀ b ∈ s, f b = 1

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₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∀ b ∈ s, f b = 1

Tactic:
replace h₀ : ∀ b ∈ s, f b = 1 := by 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
h₀ : ∀ b ∈ s, f b = 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
simp +contextual [h₀]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s₁ ∪ s₂, f a) (∏ a ∈ s₁, f a)

Tactic:
Eq.symm <|
    prod_subset subset_union_left fun _a ha ha' ↦ hs _ ((mem_union.1 ha).resolve_left ha') ha'

Premises used: Or.resolve_left, Finset.subset_union_left, Finset.prod_subset, Iff.mp, Finset.mem_union, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst : CommMonoid M
f : ι → M
inst_1 : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
rw : Eq.{u_4 + 1} (α := M) (∏ a ∈ s₂ ∪ s₁, f a) (∏ a ∈ s₂, f a)
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) (∏ a ∈ s₂, f a) (∏ a ∈ s₂, f a)
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s₁ ∪ s₂, f a) (∏ a ∈ s₂, f a)

Tactic:
rw [union_comm, prod_union_eq_left hs]

Premises used: Finset.prod_union_eq_left, Finset.union_comm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ a ∈ s₁ \ s₂, a ∉ s₁ ∩ s₂ → f a = 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
rw : ∏ a ∈ s₁ ∩ s₂, f a
| ∏ a ∈ s₁, f a

Tactic:
rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]

Premises used: Finset.prod_union_eq_right, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)

Tactic:
conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]

Premises used: Finset.prod_union_eq_right, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ a ∈ s₂ \ s₁, a ∉ s₂ ∩ s₁ → g a = 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
rw : ∏ a ∈ s₁ ∩ s₂, g a
| ∏ a ∈ s₂, g a

Tactic:
rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]

Premises used: Finset.inter_comm, Finset.prod_union_eq_right, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
conv_rhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₁ ∩ s₂, g a)
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)

Tactic:
conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]

Premises used: Finset.inter_comm, Finset.prod_union_eq_right, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ x ∈ s₁ ∩ s₂, f x = g x

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₁ ∩ s₂, g a)

Tactic:
exact prod_congr rfl (by simpa)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
conv_lhs : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)
conv_lhs₁ conv_lhs₂ : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₂, g a)
conv_lhs₃ : Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁ ∩ s₂, f a) (∏ a ∈ s₁ ∩ s₂, g a)
⊢ Eq.{u_6 + 1} (α := M) (∏ a ∈ s₁, f a) (∏ a ∈ s₂, g a)

Tactic:
classical
  conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
  conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
  exact prod_congr rfl (by simpa)

Premises used: Finset.inter_comm, Finset.prod_congr, Finset.prod_union_eq_right, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
haveI : ∀ (this : DecidableEq ι), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ s' ⊆ s

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ s' ⊆ s

Tactic:
have hu : s' ⊆ s := by grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∀ c ∈ s, c ∉ s' → f c = 1

Tactic:
grind