awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
s : Finset ι
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → M
⊢ (∏ x ∈ s, if p x then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s with p x, f x) (∏ x ∈ s with ¬p x, g x)

Tactic:
simp [prod_apply_ite _ _ fun x => x]

Premises used: Finset.prod_apply_ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)

Tactic:
prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Premises used: Subtype.mk, Finset.prod_bij', Subtype.val
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
refine_4 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a
refine_5 :
  ∀ (a : ι) (ha : a ∈ s),
    (if hi : p a then f a hi else g a hi) =
      g (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) ⋯
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, g (↑i : ι) ⋯)

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, ¬p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    (if hi : p a then f a hi else g a hi) =
      g (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) ⋯

Tactic:
aesop
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ x ∈ s, ¬p x
f g : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then f x else g x) (∏ x ∈ s, g x)

Tactic:
(prod_dite_of_false h _ _).trans (prod_attach _ _)

Premises used: Finset.prod_dite_of_false, Finset.prod_attach, Eq.trans, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)

Tactic:
prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Premises used: Subtype.mk, Finset.prod_bij', Subtype.val
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
refine_1 :
  ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)
refine_2 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s
refine_3 :
  ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a
refine_4 :
  ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a
refine_5 :
  ∀ (a : ι) (ha : a ∈ s),
    (if hi : p a then f a hi else g a hi) =
      f (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) ⋯
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if hi : p i then f i hi else g i hi) (∏ i : ↥s, f (↑i : ι) ⋯)

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_

Premises used: Finset.prod_bij'
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    Membership.mem (γ := Finset ↥s) univ ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha)

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha ∈ s

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    (fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι))
        ((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) ⋯ =
      a

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ↥s) (ha : Membership.mem (γ := Finset ↥s) univ a),
    (fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx)
        ((fun (x : ↥s) (x_1 : Membership.mem (γ := Finset ↥s) univ x) ↦ (↑x : ι)) a ha) ⋯ =
      a

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : ι) → p i → M
g : (i : ι) → ¬p i → M
⊢ ∀ (a : ι) (ha : a ∈ s),
    (if hi : p a then f a hi else g a hi) =
      f (↑((fun (x : ι) (hx : x ∈ s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s) x hx) a ha) : ι) ⋯

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
h : ∀ x ∈ s, p x
f g : ι → M
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then f x else g x) (∏ x ∈ s, f x)

Tactic:
(prod_dite_of_true h _ _).trans (prod_attach _ _)

Premises used: Finset.prod_attach, Eq.trans, Finset.prod_dite_of_true, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
simp_rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (g x))
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, k (if p x then f x else g x)) (∏ x ∈ s, k (g x))

Tactic:
simp_rw [apply_ite k]

Premises used: apply_ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (g x))

Tactic:
prod_ite_of_false h _ _

Premises used: Finset.prod_ite_of_false
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (g x))

Tactic:
exact prod_ite_of_false h _ _

Premises used: Finset.prod_ite_of_false
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
simp_rw : Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (f x))
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, k (if p x then f x else g x)) (∏ x ∈ s, k (f x))

Tactic:
simp_rw [apply_ite k]

Premises used: apply_ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (f x))

Tactic:
prod_ite_of_true h _ _

Premises used: Finset.prod_ite_of_true
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst : CommMonoid M
p : ι → Prop
inst_1 : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if p x then k (f x) else k (g x)) (∏ x ∈ s, k (f x))

Tactic:
exact prod_ite_of_true h _ _

Premises used: Finset.prod_ite_of_true
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f : ι → M
rw : Eq.{u_3 + 1} (α := M) (∏ a ∈ s with a ∈ t, f a) (∏ i ∈ s ∩ t, f i)
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) (∏ a ∈ s ∩ t, f a) (∏ i ∈ s ∩ t, f i)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s, if i ∈ t then f i else 1) (∏ i ∈ s ∩ t, f i)

Tactic:
rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]

Premises used: Finset.prod_filter, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
rw :
  Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯))
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ i : ι, if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else 1)

Tactic:
rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]

Premises used: Finset.prod_const_one, Finset.univ_eq_attach, Finset.prod_dite, mul_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : Eq.{u_1 + 1} (α := ι → Prop) (fun (x : ι) ↦ x ∈ s) fun (x : ι) ↦ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} x
h₁ : s = {x : ι | x ∈ s}
h₂ :
  HEq (α := ↥s → M) fun (i : ↥s) ↦ f i (β := ↥{x : ι | x ∈ s} → M) fun (x : ↥{x : ι | x ∈ s}) ↦
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯)
⊢ Eq.{u_3 + 1} (α := M) (∏ i ∈ s.attach, f i)
    (∏ x ∈ attach {x : ι | x ∈ s}, f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯))

Tactic:
congr
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ Eq.{u_1 + 1} (α := ι → Prop) (fun (x : ι) ↦ x ∈ s) fun (x : ι) ↦ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} x

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : ∀ (a : ι), a ∈ s ↔ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} a
⊢ s = {x : ι | x ∈ s}

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
a : ι
⊢ a ∈ s ↔ Membership.mem (γ := Finset ι) {x : ι | x ∈ s} a

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
h : ↥s = ↥{x : ι | x ∈ s}
h₁ : ∀ (a : ↥s) (a' : ↥{x : ι | x ∈ s}), a ≍ a' → f a ≍ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑a' : ι) ⋯)
⊢ HEq (α := ↥s → M) fun (i : ↥s) ↦ f i (β := ↥{x : ι | x ∈ s} → M) fun (x : ↥{x : ι | x ∈ s}) ↦
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) ⋯)

Tactic:
apply Function.hfunext

Premises used: Function.hfunext
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ ↥s = ↥{x : ι | x ∈ s}

Tactic:
simp +contextual [Subtype.heq_iff_coe_eq]

Premises used: Subtype.heq_iff_coe_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : Fintype ι
s : Finset ι
f : ↥s → M
inst_2 : DecidablePred fun (x : ι) ↦ x ∈ s
⊢ ∀ (a : ↥s) (a' : ↥{x : ι | x ∈ s}), a ≍ a' → f a ≍ f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑a' : ι) ⋯)

Tactic:
simp +contextual [Subtype.heq_iff_coe_eq]

Premises used: Subtype.heq_iff_coe_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯
neg : ∀ (h : a ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : a = x then b x h else 1) 1
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1
pos₁ : a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯

Tactic:
rw [Finset.prod_eq_single a, dif_pos rfl]

Premises used: dif_pos, Finset.prod_eq_single, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
b_1 : ι
pos : b_1 ∈ s → b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1
⊢ b_1 ∈ s → b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1

Tactic:
_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
pos : ¬a = b_1
⊢ Eq.{u_3 + 1} (α := M) (if h : a = b_1 then b b_1 h else 1) 1

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ ¬a = b_1

Tactic:
h.symm

Premises used: Ne.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ ¬a = b_1

Tactic:
exact h.symm

Premises used: Ne.symm
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
neg : ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : a = x then b x h else 1) 1
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : a = x then b x h else 1) 1

Tactic:
rw [Finset.prod_eq_one]

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : a = x then b x h else 1) 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
pos : ∀ (h : a ∈ s), (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯
neg : ∀ (h : a ∉ s), Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : x = a then b x h else 1) 1
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
pos : ∀ b_1 ∈ s, b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1
pos₁ : a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯

Tactic:
rw [Finset.prod_eq_single a, dif_pos rfl]

Premises used: dif_pos, Finset.prod_eq_single, rfl
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
b_1 : ι
pos : b_1 ∈ s → b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1
⊢ b_1 ∈ s → b_1 ≠ a → Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1

Tactic:
_
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
pos : ¬b_1 = a
⊢ Eq.{u_3 + 1} (α := M) (if h : b_1 = a then b b_1 h else 1) 1

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ ¬b_1 = a

Tactic:
h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h_1 : a ∈ s
b_1 : ι
h_2 : b_1 ∈ s
h : b_1 ≠ a
⊢ ¬b_1 = a

Tactic:
exact h
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → Eq.{u_3 + 1} (α := M) (if h : a = a then b a h else 1) 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
neg : ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : x = a then b x h else 1) 1
⊢ Eq.{u_3 + 1} (α := M) (∏ x ∈ s, if h : x = a then b x h else 1) 1

Tactic:
rw [Finset.prod_eq_one]

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ ∀ x ∈ s, Eq.{u_3 + 1} (α := M) (if h : x = a then b x h else 1) 1

Tactic:
grind
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : ι → M
⊢ (∏ x ∈ s, if a = x then b x else 1) = if a ∈ s then b a else 1

Tactic:
prod_dite_eq s a fun x _ => b x

Premises used: Finset.prod_dite_eq, ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : ι → M
⊢ (∏ x ∈ s, if x = a then b x else 1) = if a ∈ s then b a else 1

Tactic:
prod_dite_eq' s a fun x _ => b x

Premises used: Finset.prod_dite_eq', ite
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if a = x then b x else 1) = b a

Tactic:
simp only [prod_ite_eq, if_pos h]

Premises used: if_pos, Finset.prod_ite_eq
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s : Finset ι
a : ι
b : ι → M
h : a ∈ s
⊢ (∏ x ∈ s, if x = a then b x else 1) = b a

Tactic:
simp only [prod_ite_eq', if_pos h]

Premises used: Finset.prod_ite_eq', if_pos
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
a : ι
x : M
s : Finset ι
⊢ ∏ a' ∈ s, Pi.mulSingle (M := fun (a : ι) ↦ M) a x a' = if a ∈ s then x else 1

Tactic:
prod_dite_eq' _ _ _

Premises used: Function.update, Finset.prod_dite_eq', Pi.mulSingle
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : ι → Type u_6
inst : DecidableEq ι
inst_1 : (a : ι) → CommMonoid (M a)
a : ι
f : (a : ι) → M a
s : Finset ι
⊢ ∏ a' ∈ s, Pi.mulSingle (M := M) a' (f a') a = if a ∈ s then f a else 1

Tactic:
prod_dite_eq _ _ _

Premises used: Function.update, Finset.prod_dite_eq, Pi.mulSingle
-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Goal:
ι : Type u_1
M : Type u_3
inst : CommMonoid M
inst_1 : DecidableEq ι
s t : Finset ι
f g : ι → M
simp : (∏ x ∈ s, if x ∈ t then f x else g x) = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)
⊢ ∏ x ∈ s, t.piecewise (π := fun (i : ι) ↦ M) f g x = HMul.hMul (α := M) (∏ x ∈ s ∩ t, f x) (∏ x ∈ s \ t, g x)

Tactic:
simp only [piecewise]

Premises used: Finset.piecewise