awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
val : Fintype I
k : (i : I) → M i
intro :
  Eq.{u_9 + 1} (α := N) (∏ x : I, (g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))
    (∏ x : I, (h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))
⊢ Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) k : N) ((h : (a : (i : I) → M i) → N) k : N)

Tactic:
rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]

Premises used: Finset.univ_prod_mulSingle, map_prod
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H :
  ∀ (i : I) (x : M i),
    Eq.{u_9 + 1} (α := N) ((g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
      ((h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) i x) : N)
val : Fintype I
k : (i : I) → M i
⊢ Eq.{u_9 + 1} (α := N) (∏ x : I, (g : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))
    (∏ x : I, (h : (a : (i : I) → M i) → N) (Pi.mulSingle (M := M) x (k x)))

Tactic:
simp only [H]
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
M : I → Type u_8
inst_1 : (i : I) → CommMonoid (M i)
inst_2 : Finite I
N : Type u_9
inst_3 : CommMonoid N
g h : ((i : I) → M i) →* N
H : ∀ (i : I), g.comp (mulSingle M i) = h.comp (mulSingle M i)
⊢ g = h

Tactic:
g.functions_ext N h fun i => DFunLike.congr_fun (H i)

Premises used: DFunLike.congr_fun, MonoidHom.functions_ext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
I : Type u_7
inst : DecidableEq I
R : I → Type u_8
inst_1 : (i : I) → NonAssocSemiring (R i)
inst_2 : Finite I
S : Type u_9
inst_3 : NonAssocSemiring S
g h : ((i : I) → R i) →+* S
H :
  ∀ (i : I) (x : R i),
    Eq.{u_9 + 1} (α := S) ((g : (a : (i : I) → R i) → S) (single (M := R) i x) : S)
      ((h : (a : (i : I) → R i) → S) (single (M := R) i x) : S)
⊢ g = h

Tactic:
RingHom.coe_addMonoidHom_injective <|
    @AddMonoidHom.functions_ext I _ R _ _ S _ (g : (∀ i, R i) →+ S) h H

Premises used: AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.functions_ext, RingHom.coe_addMonoidHom_injective
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
s : Finset ι
f : ι → M × N
⊢ Eq.{u_3 + 1} (α := M) (∏ c ∈ s, f c).1 (∏ c ∈ s, (f c).1)

Tactic:
map_prod (MonoidHom.fst ..) f s

Premises used: map_prod, MonoidHom.fst
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : CommMonoid M
inst_1 : CommMonoid N
s : Finset ι
f : ι → M × N
⊢ Eq.{u_4 + 1} (α := N) (∏ c ∈ s, f c).2 (∏ c ∈ s, (f c).2)

Tactic:
map_prod (MonoidHom.snd ..) f s

Premises used: map_prod, MonoidHom.snd
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
h :
  ∀ (x : (i : ι) → M i),
    Eq.{u_9 + 1} (α := M')
      (((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
                (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
              ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) :
            (a : (i : ι) → M i) → M')
          x :
        M')
      ((φ : (a : (i : ι) → M i) → M') x : M')
⊢ (fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
        (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
      ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) =
    φ

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
h :
  Eq.{u_9 + 1} (α := M') ((φ : (a : (i : ι) → M i) → M') (∏ x_1 : ι, mulSingle (M := M) x_1 (x x_1)) : M')
    ((φ : (a : (i : ι) → M i) → M') x : M')
⊢ Eq.{u_9 + 1} (α := M')
    (((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
              (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
            ((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) φ) :
          (a : (i : ι) → M i) → M')
        x :
      M')
    ((φ : (a : (i : ι) → M i) → M') x : M')

Tactic:
simp only [MonoidHom.finsetProd_apply, MonoidHom.coe_comp, Function.comp_apply,
      evalMonoidHom_apply, MonoidHom.mulSingle_apply, ← map_prod]

Premises used: MonoidHom.coe_comp, Pi.evalMonoidHom_apply, MonoidHom.finsetProd_apply, MonoidHom.mulSingle_apply, map_prod, Function.comp_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
⊢ Eq.{u_9 + 1} (α := M') ((φ : (a : (i : ι) → M i) → M') (∏ x_1 : ι, mulSingle (M := M) x_1 (x x_1)) : M')
    ((φ : (a : (i : ι) → M i) → M') x : M')

Tactic:
congrArg _ <| funext fun _ ↦ ?_

Premises used: congrArg, funext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
h : ∀ (x_1 : ι), (∏ x_2 : ι, mulSingle (M := M) x_2 (x x_2)) x_1 = x x_1
⊢ Eq.{u_9 + 1} (α := M') ((φ : (a : (i : ι) → M i) → M') (∏ x_1 : ι, mulSingle (M := M) x_1 (x x_1)) : M')
    ((φ : (a : (i : ι) → M i) → M') x : M')

Tactic:
refine congrArg _ <| funext fun _ ↦ ?_

Premises used: congrArg, funext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
x_1 : ι
h : ∏ c : ι, mulSingle (M := M) c (x c) x_1 = x x_1
⊢ (∏ x_2 : ι, mulSingle (M := M) x_2 (x x_2)) x_1 = x x_1

Tactic:
rw [Fintype.prod_apply]

Premises used: Fintype.prod_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
x_1 : ι
⊢ ∏ c : ι, mulSingle (M := M) c (x c) x_1 = x x_1

Tactic:
Fintype.prod_pi_mulSingle ..

Premises used: Fintype.prod_pi_mulSingle
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : ((i : ι) → M i) →* M'
x : (i : ι) → M i
x_1 : ι
⊢ ∏ c : ι, mulSingle (M := M) c (x c) x_1 = x x_1

Tactic:
exact Fintype.prod_pi_mulSingle ..

Premises used: Fintype.prod_pi_mulSingle
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
h :
  ∀ (i : ι) (m : M i),
    Eq.{u_9 + 1} (α := M')
      (((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
              ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
                  (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
                φ)
              i :
            (a : M i) → M')
          m :
        M')
      ((φ i : (a : M i) → M') m : M')
⊢ (fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
      ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
          (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
        φ) =
    φ

Tactic:
ext i m
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
h :
  Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')
⊢ Eq.{u_9 + 1} (α := M')
    (((fun (φ : ((i : ι) → M i) →* M') (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
            ((fun (φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M') ↦
                (∏ i : ι, (φ i).comp (evalMonoidHom M i) : ((i : ι) → M i) →* M'))
              φ)
            i :
          (a : M i) → M')
        m :
      M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.finsetProd_apply, evalMonoidHom_apply, ]

Premises used: MonoidHom.coe_comp, Pi.evalMonoidHom_apply, MonoidHom.finsetProd_apply, MonoidHom.mulSingle_apply, Function.comp_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
h : ∀ (j : ι), ((φ j : (a : M j) → M') (mulSingle (M := M) i m j) : M')
| Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
enter [1, 2, j]
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
j : ι
h : (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m) j : M')
| ((φ j : (a : M j) → M') (mulSingle (M := M) i m j) : M')

Tactic:
rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]

Premises used: map_one, Pi.apply_mulSingle, rfl
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
h : ∀ (j : ι), (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m) j : M')
| Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]

Premises used: map_one, Pi.apply_mulSingle
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
h :
  Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m)) : M')
    ((φ i : (a : M i) → M') m : M')
⊢ Eq.{u_9 + 1} (α := M') (∏ x : ι, (φ x : (a : M x) → M') (mulSingle (M := M) i m x) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
conv =>
      enter [1, 2, j]
      rw [show φ j = φ' j from rfl, Pi.apply_mulSingle φ' (fun i ↦ map_one (φ i))]

Premises used: map_one, Pi.apply_mulSingle
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
h :
  Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i ((φ i : (a : M i) → M') m)) : M')
    ((φ i : (a : M i) → M') m : M')
⊢ Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i (φ' i m)) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
rw [show φ' i = φ i from rfl]

Premises used: rfl
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
⊢ Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i ((φ i : (a : M i) → M') m)) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
Fintype.prod_pi_mulSingle' ..

Premises used: Fintype.prod_pi_mulSingle'
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ : (i : ι) → MonoidHom.{u_8, u_9} (M i) M'
i : ι
m : M i
φ' : (i : ι) → M i → M' := fun (i : ι) ↦ (⇑(φ i) : (a : M i) → M')
⊢ Eq.{u_9 + 1} (α := M') (Finset.prod Finset.univ (mulSingle (M := fun (i : ι) ↦ M') i ((φ i : (a : M i) → M') m)) : M')
    ((φ i : (a : M i) → M') m : M')

Tactic:
exact Fintype.prod_pi_mulSingle' ..

Premises used: Fintype.prod_pi_mulSingle'
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
h :
  ∀ (x : ι) (x_1 : M x),
    Eq.{u_9 + 1} (α := M') (((φ * ψ).comp (MonoidHom.mulSingle M x) : (a : M x) → M') x_1 : M')
      ((HMul.hMul (α := (i : ι) → MonoidHom.{u_8, u_9} (M i) M') (β := (i : ι) → MonoidHom.{u_8, u_9} (M i) M')
              (fun (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) (fun (i : ι) ↦ ψ.comp (MonoidHom.mulSingle M i)) x :
            (a : M x) → M')
          x_1 :
        M')
⊢ (fun (i : ι) ↦ (φ * ψ).comp (MonoidHom.mulSingle M i)) =
    HMul.hMul (α := (i : ι) → MonoidHom.{u_8, u_9} (M i) M') (fun (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i))
      fun (i : ι) ↦ ψ.comp (MonoidHom.mulSingle M i)

Tactic:
ext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι_1 : Type u_1
κ : Type u_2
M_1 : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst : Fintype ι
inst_1 : DecidableEq ι
M : ι → Type u_8
inst_2 : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst_3 : CommMonoid M'
φ ψ : ((i : ι) → M i) →* M'
x : ι
x_1 : M x
⊢ Eq.{u_9 + 1} (α := M') (((φ * ψ).comp (MonoidHom.mulSingle M x) : (a : M x) → M') x_1 : M')
    ((HMul.hMul (α := (i : ι) → MonoidHom.{u_8, u_9} (M i) M') (β := (i : ι) → MonoidHom.{u_8, u_9} (M i) M')
            (fun (i : ι) ↦ φ.comp (MonoidHom.mulSingle M i)) (fun (i : ι) ↦ ψ.comp (MonoidHom.mulSingle M i)) x :
          (a : M x) → M')
        x_1 :
      M')

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.mul_apply, mul_apply]

Premises used: Pi.mul_apply, MonoidHom.coe_comp, MonoidHom.mulSingle_apply, Function.comp_apply, MonoidHom.mul_apply
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
intro : ∀ (val : Fintype ι), p f
⊢ p f

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
val : Fintype ι
intro : p (∑ i : ι, Pi.single (M := M) i (f i))
⊢ p f

Tactic:
rw [← Finset.univ_sum_single f]

Premises used: Finset.univ_sum_single
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
val : Fintype ι
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → p (Pi.single (M := M) x (f x))

Tactic:
simp [single]
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → AddCommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
zero : p 0
add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M i), p (Pi.single (M := M) i m)
val : Fintype ι
⊢ p (∑ i : ι, Pi.single (M := M) i (f i))

Tactic:
exact Finset.sum_induction _ _ add zero (by simp [single])

Premises used: Finset.sum_induction
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
intro : ∀ (val : Fintype ι), p f
⊢ p f

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
val : Fintype ι
intro : p (∏ i : ι, Pi.mulSingle (M := M) i (f i))
⊢ p f

Tactic:
rw [← Finset.univ_prod_mulSingle f]

Premises used: Finset.univ_prod_mulSingle
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
val : Fintype ι
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) Finset.univ x → p (Pi.mulSingle (M := M) x (f x))

Tactic:
simp [mulSingle]
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_1
inst : Finite ι
inst_1 : DecidableEq ι
M : ι → Type u_7
inst_2 : (i : ι) → CommMonoid (M i)
p : ((i : ι) → M i) → Prop
f : (i : ι) → M i
one : p 1
mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M i), p (Pi.mulSingle (M := M) i m)
val : Fintype ι
⊢ p (∏ i : ι, Pi.mulSingle (M := M) i (f i))

Tactic:
exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

Premises used: Finset.prod_induction
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
t : β
ht : t ∈ s
⊢ Eq.{u_9 + 1} (α := α) ((∏ i ∈ v, f i) t) ((∏ i ∈ v, f' i) t)

Tactic:
simp [funext fun i ↦ h i ht]

Premises used: funext
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
⊢ Set.EqOn.{u_10, u_9} (β := α) (∏ i ∈ v, f i) (∏ i ∈ v, f' i) s

Tactic:
eqOn_finsetProd h v

Premises used: eqOn_finsetProd
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
h₁ : ∀ (x : β), Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f i x) ((∏ i ∈ v, f i) x)
h₂ : ∀ (x : β), Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f' i x) ((∏ i ∈ v, f' i) x)
⊢ Set.EqOn.{u_10, u_9} (β := α) (fun (b : β) ↦ ∏ i ∈ v, f i b) (fun (b : β) ↦ ∏ i ∈ v, f' i b) s

Tactic:
convert! eqOn_finsetProd h v

Premises used: eqOn_finsetProd
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x : β
⊢ Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f i x) ((∏ i ∈ v, f i) x)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Pi
Goal:
ι : Type u_8
α : Type u_9
β : Type u_10
inst : CommMonoid α
s : Set β
f f' : ι → β → α
h : ∀ (i : ι), Set.EqOn (f i) (f' i) s
v : Finset ι
x : β
⊢ Eq.{u_9 + 1} (α := α) (∏ i ∈ v, f' i x) ((∏ i ∈ v, f' i) x)

Tactic:
simp
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
M : Type u_3
s : Finset ι
inst : CommMonoid M
inst_1 : HasDistribNeg M
f : ι → M
⊢ ∏ x ∈ s, -f x = HPow.hPow (α := M) (-1) #s * ∏ x ∈ s, f x

Tactic:
simpa using (s.1.map f).prod_map_neg

Premises used: Multiset.prod_map_neg, Multiset.map, Finset.val
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
rw : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) (∑ x ∈ s with ¬p x, 0)
rw₁ : (↑(#({x ∈ s | p x})) : R) = HAdd.hAdd (α := R) (∑ x ∈ s with p x, 1) 0
rw₂ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ x ∈ s with p x, 1)
rw₃ : (↑(#({x ∈ s | p x})) : R) = HSMul.hSMul (β := R) (#({x ∈ s | p x})) 1
rw₄ rw₅ : Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (↑(#({x ∈ s | p x})) : R)
⊢ Eq.{u_4 + 1} (α := R) (↑(#({x ∈ s | p x})) : R) (∑ a ∈ s, if p a then 1 else 0)

Tactic:
rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]

Premises used: Finset.sum_const_zero, nsmul_one, add_zero, Finset.sum_ite, Finset.sum_const
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : AddCommMonoidWithOne R
p : ι → Prop
inst_1 : DecidablePred p
s : Finset ι
⊢ Eq.{u_4 + 1} (α := R) (∑ x ∈ s, if p x then 1 else 0) (↑(#({x ∈ s | p x})) : R)

Tactic:
(natCast_card_filter _ _).symm

Premises used: Finset.natCast_card_filter, Eq.symm
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
s t : Finset ι
inst : DecidablePred fun (x : ι) ↦ x ∈ s
hst : s ⊆ t
⊢ #s = ∑ i ∈ t, if i ∈ s then 1 else 0

Tactic:
simp [hst]
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
a : R
⊢ (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a

Tactic:
map_sum (AddMonoidHom.mulRight a) _ s

Premises used: map_sum, AddMonoidHom.mulRight
-- Module: Mathlib.Algebra.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_4
inst : NonUnitalNonAssocSemiring R
s : Finset ι
f : ι → R
a : R
⊢ a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i

Tactic:
map_sum (AddMonoidHom.mulLeft a) _ s

Premises used: map_sum, AddMonoidHom.mulLeft