awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := 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
hf : ∀ c ∈ s, c ∉ s' → f c = 1
rw : ∏ x ∈ s', f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [← Finset.prod_subset hu hf]

Premises used: Finset.prod_subset
-- 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
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s', f x = f a * f b

Tactic:
Finset.prod_pair hn

Premises used: Finset.prod_pair
-- 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
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s', f x = f a * f b

Tactic:
exact Finset.prod_pair hn

Premises used: Finset.prod_pair
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 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 : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
pos : ∀ (h₁ : a ∈ s), ∏ x ∈ s, f x = f a * f b
neg : ∀ (h₁ : a ∉ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by_cases h₁ : a ∈ s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
neg : ∀ (h₂ : b ∉ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by_cases h₂ : b ∈ s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
pos : ∀ (h₂ : b ∈ s), ∏ x ∈ s, f x = f a * f b
neg : ∀ (h₂ : b ∉ s), ∏ x ∈ s, f x = f a * f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by_cases h₂ : b ∈ s
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
prod_eq_mul_of_mem a b h₁ h₂ hn h₀

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

Tactic:
exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀

Premises used: Finset.prod_eq_mul_of_mem
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
neg : ∏ x ∈ s, f x = f a
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [hb h₂, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
neg : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = f a

Tactic:
apply prod_eq_single_of_mem a 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
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∀ b ∈ s, b ≠ a → f b = 1

Tactic:
fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩

Premises used: ne_of_mem_of_not_mem, And.intro
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∀ b ∈ s, b ≠ a → f b = 1

Tactic:
exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩

Premises used: ne_of_mem_of_not_mem, And.intro
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
pos : ∏ x ∈ s, f x = f b
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
pos : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
⊢ ∏ x ∈ s, f x = f b

Tactic:
apply prod_eq_single_of_mem b 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
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1

Tactic:
fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

Premises used: ne_of_mem_of_not_mem, And.intro
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1

Tactic:
exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩

Premises used: ne_of_mem_of_not_mem, And.intro
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
neg : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [ha h₁, hb h₂, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
_root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

Premises used: trans, Finset.prod_congr, ne_of_mem_of_not_mem, Finset.prod_const_one, And.intro, 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 : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
h₂ : b ∉ s
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
exact
      _root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

Premises used: trans, Finset.prod_congr, ne_of_mem_of_not_mem, Finset.prod_const_one, And.intro, rfl
-- 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
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x)
    (∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p : (a : Subtype p) → ι) x))

Tactic:
have := prod_map (s.subtype p) (Function.Embedding.subtype _) f
-- 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
this :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x)
    (∏ x ∈ Finset.subtype p s, f ((Embedding.subtype p : (a : Subtype p) → ι) x))
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ Finset.subtype p s, f (↑x : ι)) (∏ x ∈ s with p x, f x)

Tactic:
simp_all
-- 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
h rw : ∀ x ∈ s, p x
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ Finset.subtype p s, f (↑x : ι)) (∏ x ∈ s, f x)

Tactic:
rw [prod_subtype_eq_prod_filter, filter_true_of_mem]

Premises used: Finset.filter_true_of_mem, Finset.prod_subtype_eq_prod_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
h : ∀ x ∈ s, p x
⊢ ∀ x ∈ s, p x

Tactic:
simpa using h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
p : ι → Prop
s : Finset { x : ι // p x }
f : { x : ι // p x } → M
g : ι → M
h : ∀ x ∈ s, g (↑x : ι) = f x
rw :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s, g ((Embedding.subtype fun (x : ι) ↦ p x : (a : { x : ι // p x }) → ι) x))
    (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ map (Embedding.subtype fun (x : ι) ↦ p x) s, g x) (∏ x ∈ s, f x)

Tactic:
rw [Finset.prod_map]

Premises used: Finset.prod_map
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
p : ι → Prop
s : Finset { x : ι // p x }
f : { x : ι // p x } → M
g : ι → M
h : ∀ x ∈ s, g (↑x : ι) = f x
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, g ((Embedding.subtype fun (x : ι) ↦ p x : (a : { x : ι // p x }) → ι) x))
    (∏ x ∈ s, f x)

Tactic:
Finset.prod_congr rfl h

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
p : ι → Prop
s : Finset { x : ι // p x }
f : { x : ι // p x } → M
g : ι → M
h : ∀ x ∈ s, g (↑x : ι) = f x
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, g ((Embedding.subtype fun (x : ι) ↦ p x : (a : { x : ι // p x }) → ι) x))
    (∏ x ∈ s, f x)

Tactic:
exact Finset.prod_congr rfl h

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

Tactic:
prod_attach _ _

Premises used: Finset.univ, Finset.attach, Finset.prod_attach
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Finset ι
⊢ Eq.{u_4 + 1} (α := M) (∏ i : (↑(↑s : Set ι) : Type u_1), f (↑i : ι)) (∏ i ∈ s, f i)

Tactic:
prod_coe_sort s f

Premises used: Finset.prod_coe_sort
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
p : ι → Prop
F : Fintype (Subtype p)
s : Finset ι
h : ∀ (x : ι), x ∈ s ↔ p x
f : ι → M
⊢ p = fun (x : ι) ↦ x ∈ s

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
p : ι → Prop
F : Fintype (Subtype p)
s : Finset ι
h : ∀ (x : ι), x ∈ s ↔ p x
f : ι → M
obtain :
  ∀ {F : Fintype ↥s} (h : ∀ (x : ι), x ∈ s ↔ (fun (x : ι) ↦ x ∈ s) x),
    Eq.{u_4 + 1} (α := M) (∏ a ∈ s, f a) (∏ a : ↥s, f (↑a : ι))
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s, f a) (∏ a : Subtype p, f (↑a : ι))

Tactic:
obtain rfl : p = (· ∈ s) := by simp [h]

Premises used: Membership.mem, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun (x : ι) ↦ x ∈ s) x
rw : Eq.{u_4 + 1} (α := M) (∏ i : ↥s, f (↑i : ι)) (∏ a : ↥s, f (↑a : ι))
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ s, f a) (∏ a : ↥s, f (↑a : ι))

Tactic:
rw [← prod_coe_sort]

Premises used: Finset.prod_coe_sort
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun (x : ι) ↦ x ∈ s) x
⊢ Eq.{u_4 + 1} (α := M) (∏ i : ↥s, f (↑i : ι)) (∏ a : ↥s, f (↑a : ι))

Tactic:
congr!
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
f : ι → M
s : Set ι
inst_1 : Fintype (↑s : Type u_1)
⊢ Eq.{u_4 + 1} (α := M) (∏ i : (↑s : Type u_1), f (↑i : ι)) (∏ i ∈ s.toFinset, f i)

Tactic:
(Finset.prod_subtype s.toFinset (fun _ ↦ Set.mem_toFinset) f).symm

Premises used: Set.toFinset, Set.mem_toFinset, Finset.prod_subtype, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Set ι
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
f : ι → M
g : (↑s : Type u_1) → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
w' : ∀ x ∉ s, f x = 1
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) univ x → x ∉ s.toFinset → f x = 1

Tactic:
simpa
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Set ι
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
f : ι → M
g : (↑s : Type u_1) → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
w' : ∀ x ∉ s, f x = 1
⊢ ∀ (x : ι), x ∈ s.toFinset ↔ (fun (x : ι) ↦ x ∈ s) x

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Set ι
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
f : ι → M
g : (↑s : Type u_1) → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
w' : ∀ x ∉ s, f x = 1
rw : Eq.{u_4 + 1} (α := M) (∏ a : { x : ι // x ∈ s }, f (↑a : ι)) (∏ i : (↑s : Type u_1), g i)
rw₁ : Fintype { x : ι // x ∈ s }
⊢ Eq.{u_4 + 1} (α := M) (∏ i : ι, f i) (∏ i : (↑s : Type u_1), g i)

Tactic:
rw [← prod_subset s.toFinset.subset_univ (by simpa), prod_subtype (p := (· ∈ s)) _ (by simp)]

Premises used: Finset.prod_subset, Set.toFinset, Finset.prod_subtype, Finset.subset_univ
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Set ι
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
f : ι → M
g : (↑s : Type u_1) → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
w' : ∀ x ∉ s, f x = 1
x : ι
h : x ∈ s
h_1 : Membership.mem (γ := Finset { x : ι // x ∈ s }) univ (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
⊢ f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) : ι) = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)

Tactic:
w x h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype ι
s : Set ι
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
f : ι → M
g : (↑s : Type u_1) → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
w' : ∀ x ∉ s, f x = 1
x : ι
h : x ∈ s
h_1 : Membership.mem (γ := Finset { x : ι // x ∈ s }) univ (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)
⊢ f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h) : ι) = g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x h)

Tactic:
exact w x h
-- 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
⊢ Eq.{u_4 + 1} (α := M) (∏ i ∈ s, if i ∈ s then f i else 1) (∏ i ∈ s, f i)

Tactic:
(prod_congr rfl) fun _i hi => if_pos hi

Premises used: Finset.prod_congr, if_pos, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ↥s → M
rw :
  Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f x)
    (∏ x ∈ s.attach, extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) f 1 (↑x : ι))
⊢ Eq.{u_4 + 1} (α := M) (∏ x : ↥s, f x) (∏ x ∈ s, extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) f 1 x)

Tactic:
rw [univ_eq_attach, ← Finset.prod_attach s]

Premises used: Finset.univ_eq_attach, Finset.prod_attach
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ↥s → M
e_f :
  ∀ (x : ι) (hx : x ∈ s),
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) =
      extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) f 1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s.attach, f x)
    (∏ x ∈ s.attach, extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) f 1 (↑x : ι))

Tactic:
congr with ⟨x, hx⟩
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ↥s → M
x : ι
hx : x ∈ s
e_f e_f₁ : f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) = f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
⊢ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) =
    extend (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) f 1 (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) : ι)

Tactic:
rw [Subtype.val_injective.extend_apply]

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- 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₂)
rw rw₁ : Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ s with f x ≠ 1, f x)

Tactic:
rw [prod_filter_ne_one]

Premises used: 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
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 ≠ 1

Tactic:
simpa using (mem_filter.mp ha).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 κ
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₂)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ t with g x ≠ 1, g x) (∏ x ∈ t, g x)

Tactic:
prod_filter_ne_one _

Premises used: 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
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₂)
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)
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, g x)

Tactic:
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 _

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
κ : 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}), (fun (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}) ↦ i a ⋯ ⋯) a ha ∈ {x ∈ t | g x ≠ 1}

Tactic:
grind
-- 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}) (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₂

Tactic:
solve_by_elim