awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f g : α → β
comm_ff : (↑∅ : Set α).Pairwise (Commute on f)
comm_gg : (↑∅ : Set α).Pairwise (Commute on g)
comm_gf : (↑∅ : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
⊢ noncommProd ∅ (f * g) ⋯ = noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
    (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
rw : ∀ (y : α) (hy : y ∈ s), Commute (g x) (f y)
⊢ (cons x s hnotMem).noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]

Premises used: Commute.mul_mul_mul_comm, Pi.mul_apply, Finset.mem_cons_of_mem, Set.Pairwise.mono, Finset.noncommProd_commute, Finset.noncommProd_cons
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
    (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)

Tactic:
comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm

Premises used: Finset.mem_cons_of_mem, Ne.symm, ne_of_mem_of_not_mem, Finset.mem_cons_self
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
    (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)

Tactic:
exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm

Premises used: Finset.mem_cons_of_mem, Ne.symm, ne_of_mem_of_not_mem, Finset.mem_cons_self
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
empty :
  ∀ (comm_ff : (↑∅ : Set α).Pairwise (Commute on f)) (comm_gg : (↑∅ : Set α).Pairwise (Commute on g))
    (comm_gf : (↑∅ : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    noncommProd ∅ (f * g) ⋯ = noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg
cons :
  ∀ (x : α) (s : Finset α) (hnotMem : x ∉ s)
    (ih :
      ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
        (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
        s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg)
    (comm_ff : (↑(Finset.cons x s hnotMem) : Set α).Pairwise (Commute on f))
    (comm_gg : (↑(Finset.cons x s hnotMem) : Set α).Pairwise (Commute on g))
    (comm_gf : (↑(Finset.cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    (Finset.cons x s hnotMem).noncommProd (f * g) ⋯ =
      (Finset.cons x s hnotMem).noncommProd f comm_ff * (Finset.cons x s hnotMem).noncommProd g comm_gg
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons x s hnotMem ih =>
    rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
    exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm

Premises used: Commute.mul_mul_mul_comm, Pi.mul_apply, Finset.cons, Finset.noncommProd_commute, Finset.noncommProd_cons
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
h : ∀ (i : ι), noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ i = x i
⊢ noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ = x

Tactic:
ext i
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h :
  noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i
apply :
  (↑univ : Set ι).Pairwise
    (Function.onFun (β := (i : ι) → M i) Commute fun (i : ι) ↦
      ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i))
⊢ noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ i = x i

Tactic:
apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans

Premises used: Finset.univ, MonoidHom.mulSingle, Finset.map_noncommProd, Pi.evalMonoidHom, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i_1 i : ι
_ :
  i ∈ (↑univ : Set ι) →
    ∀ ⦃y : ι⦄,
      y ∈ (↑univ : Set ι) →
        i ≠ y →
          Function.onFun (β := (i : ι) → M i) Commute
            (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i y
⊢ i ∈ (↑univ : Set ι) →
    ∀ ⦃y : ι⦄,
      y ∈ (↑univ : Set ι) →
        i ≠ y →
          Function.onFun (β := (i : ι) → M i) Commute
            (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i y

Tactic:
_
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i_1 i : ι
h : i ∈ (↑univ : Set ι)
j : ι
_ :
  j ∈ (↑univ : Set ι) →
    i ≠ j →
      Function.onFun (β := (i : ι) → M i) Commute
        (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j
⊢ j ∈ (↑univ : Set ι) →
    i ≠ j →
      Function.onFun (β := (i : ι) → M i) Commute
        (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j

Tactic:
_
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i_1 i : ι
h : i ∈ (↑univ : Set ι)
j : ι
h_1 : j ∈ (↑univ : Set ι)
_ :
  i ≠ j →
    Function.onFun (β := (i : ι) → M i) Commute
      (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j
⊢ i ≠ j →
    Function.onFun (β := (i : ι) → M i) Commute
      (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j

Tactic:
_
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i_1 i : ι
h : i ∈ (↑univ : Set ι)
j : ι
h_1 : j ∈ (↑univ : Set ι)
h_2 : i ≠ j
⊢ Function.onFun (β := (i : ι) → M i) Commute
    (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j

Tactic:
Pi.mulSingle_apply_commute x i j

Premises used: Function.update, dite, Pi.mulSingle_apply_commute, Pi.mulSingle
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i_1 i : ι
h : i ∈ (↑univ : Set ι)
j : ι
h_1 : j ∈ (↑univ : Set ι)
h_2 : i ≠ j
⊢ Function.onFun (β := (i : ι) → M i) Commute
    (fun (i : ι) ↦ ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i)) i j

Tactic:
exact Pi.mulSingle_apply_commute x i j

Premises used: Pi.mulSingle_apply_commute
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ : Set ι).Pairwise
    (Function.onFun (β := (i : ι) → M i) Commute fun (i : ι) ↦
      ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i))

Tactic:
case a =>
    intro i _ j _ _
    exact Pi.mulSingle_apply_commute x i j
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i

Tactic:
(noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _

Premises used: Finset.mem_univ, Eq.symm, Finset.insert_erase, Finset.noncommProd_congr, Eq.trans
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h : ι → M i
h₁ :
  ∀ x_1 ∈ insert i (erase univ i),
    (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
        (((MonoidHom.mulSingle M x_1 : M x_1 →* (i : ι) → M i) : (a : M x_1) → (i : ι) → M i) (x x_1)) =
      Pi.mulSingle (M := M) x_1 (x x_1) i
h₂ : (insert i (erase univ i)).noncommProd (fun (j : ι) ↦ Pi.mulSingle (M := M) j (x j) i) ⋯ = x i
⊢ noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i

Tactic:
convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _

Premises used: Finset.mem_univ, Eq.symm, Finset.insert_erase, Finset.noncommProd_congr, Eq.trans
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ M i

Tactic:
exact Pi.mulSingle j (x j) i

Premises used: Pi.mulSingle
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i j : ι
h :
  j ∈ insert i (erase univ i) →
    (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
        (((MonoidHom.mulSingle M j : M j →* (i : ι) → M i) : (a : M j) → (i : ι) → M i) (x j)) =
      Pi.mulSingle (M := M) j (x j) i
⊢ j ∈ insert i (erase univ i) →
    (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
        (((MonoidHom.mulSingle M j : M j →* (i : ι) → M i) : (a : M j) → (i : ι) → M i) (x j)) =
      Pi.mulSingle (M := M) j (x j) i

Tactic:
_
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i j : ι
h : j ∈ insert i (erase univ i)
⊢ (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
      (((MonoidHom.mulSingle M j : M j →* (i : ι) → M i) : (a : M j) → (i : ι) → M i) (x j)) =
    Pi.mulSingle (M := M) j (x j) i

Tactic:
dsimp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h : Pi.mulSingle (M := M) i (x i) i = x i
h₁ : ∀ x_1 ∈ erase univ i, Pi.mulSingle (M := M) x_1 (x x_1) i = 1
⊢ (insert i (erase univ i)).noncommProd (fun (j : ι) ↦ Pi.mulSingle (M := M) j (x j) i) ⋯ = x i

Tactic:
rw [noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),
      noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]

Premises used: one_pow, Finset.univ, Finset.notMem_erase, mul_one, Finset.noncommProd_eq_pow_card, Finset.erase, Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle (M := M) i (x i) i = x i

Tactic:
simp only [Pi.mulSingle_eq_same]

Premises used: Pi.mulSingle_eq_same
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ erase univ i, Pi.mulSingle (M := M) x_1 (x x_1) i = 1

Tactic:
simpa using fun _ a ↦ Pi.mulSingle_eq_of_ne (a ·.symm) _

Premises used: Pi.mulSingle_eq_of_ne
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
intro : ∀ (val : Fintype ι), f = g
⊢ f = g

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
intro :
  ∀ (x : (i : ι) → M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) x : γ) ((g : (a : (i : ι) → M i) → γ) x : γ)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
intro :
  Eq.{u_5 + 1} (α := γ)
    (noncommProd univ (fun (i : ι) ↦ (f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)
    (noncommProd univ (fun (i : ι) ↦ (g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)
⊢ Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) x : γ) ((g : (a : (i : ι) → M i) → γ) x : γ)

Tactic:
rw [← noncommProd_mulSingle x, univ.map_noncommProd, univ.map_noncommProd]

Premises used: Finset.univ, Finset.noncommProd_mulSingle, Finset.map_noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
intro :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
⊢ Eq.{u_5 + 1} (α := γ)
    (noncommProd univ (fun (i : ι) ↦ (f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)
    (noncommProd univ (fun (i : ι) ↦ (g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i))) ⋯)

Tactic:
congr 1 with i
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
i : ι
⊢ Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
    ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)

Tactic:
h i (x i)
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
ι : Type u_2
γ : Type u_5
inst : Monoid γ
M : ι → Type u_6
inst_1 : (i : ι) → Monoid (M i)
inst_2 : Finite ι
inst_3 : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h :
  ∀ (i : ι) (x : M i),
    Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
      ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i x) : γ)
val : Fintype ι
x : (i : ι) → M i
i : ι
⊢ Eq.{u_5 + 1} (α := γ) ((f : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)
    ((g : (a : (i : ι) → M i) → γ) (Pi.mulSingle (M := M) i (x i)) : γ)

Tactic:
exact h i (x i)
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset α) (toFinset none) ∅

Tactic:
rfl

Premises used: Option.toFinset, rfl
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a : α
⊢ (some a).toFinset = {a}

Tactic:
rfl

Premises used: Option.toFinset, rfl
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a : α
o : Option α
none : Membership.mem (γ := Finset α) (toFinset Option.none) a ↔ Membership.mem (γ := Option α) Option.none a
some : ∀ (val : α), a ∈ (Option.some val).toFinset ↔ a ∈ Option.some val
⊢ a ∈ o.toFinset ↔ a ∈ o

Tactic:
cases o
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Finset α) (toFinset none) a ↔ Membership.mem (γ := Option α) none a

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
a val : α
⊢ a ∈ (some val).toFinset ↔ a ∈ some val

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
o : Option α
none : Finset.card.{u_1} (α := α) (toFinset Option.none) = Option.elim.{u_1, 1} (α := α) Option.none 0 1
some : ∀ (val : α), (Option.some val).toFinset.card = (Option.some val).elim 0 1
⊢ o.toFinset.card = o.elim 0 1

Tactic:
cases o
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
⊢ Finset.card.{u_1} (α := α) (toFinset none) = Option.elim.{u_1, 1} (α := α) none 0 1

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
val : α
⊢ (some val).toFinset.card = (some val).elim 0 1

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
β : Type u_2
s : Finset α
⊢ none ∉ map Embedding.some s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
rw : cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ≤ t
rw₁ : map Embedding.some s ⊆ map Embedding.some t ↔ s ≤ t
rw₂ : s ⊆ t ↔ s ≤ t
rw₃ rw₄ : s ⊆ t ↔ s ⊆ t
⊢ cons none (map Embedding.some s) ⋯ ≤ cons none (map Embedding.some t) ⋯ ↔ s ≤ t

Tactic:
rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]

Premises used: Finset.cons_subset_cons, Finset.le_iff_subset, Finset.map_subset_map
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
a : α
h : Membership.mem (γ := Option α) none a
⊢ a ∈ s

Tactic:
cases h
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ a_1 ∈ some a, a_1 ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
p : Option α → Prop
⊢ (∀ (a : Option α),
      Membership.mem (γ := Finset (Option α)) ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α))
          a →
        p a) ↔
    p none ∧ ∀ a ∈ s, p (some a)

Tactic:
simp [Option.forall]

Premises used: Option.forall
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Membership.mem (γ := Finset (Option α)) ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α))
      (some a) ↔
    a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
⊢ Membership.mem (γ := Finset (Option α)) ((insertNone : (a : Finset α) → Finset (Option α)) s : Finset (Option α)) none

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
⊢ Finset.Nonempty.{u_1} (α := Option α) ((insertNone : (a : Finset α) → Finset (Option α)) s)

Tactic:
⟨none, none_mem_insertNone⟩

Premises used: Finset.none_mem_insertNone, Option.none, Exists.intro, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
⊢ card.{u_1} (α := Option α) ((insertNone : (a : Finset α) → Finset (Option α)) s) = #s + 1

Tactic:
simp [insertNone]

Premises used: Finset.insertNone
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
x : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) x ↔ some x ∈ s

Tactic:
simp [eraseNone]

Premises used: Finset.eraseNone
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
p : Option α → Prop
⊢ (∀ (a : α),
      Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) a → p (some a)) ↔
    ∀ (a : α), some a ∈ s → p (some a)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset (Option α)
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) a ↔
      a ∈ s.biUnion Option.toFinset
⊢ (eraseNone : (a : Finset (Option α)) → Finset α) s = s.biUnion Option.toFinset

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset (Option α)
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) a ↔
    a ∈ s.biUnion Option.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
h :
  ∀ (a : α),
    Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (map Embedding.some s) : Finset α)
        a ↔
      a ∈ s
⊢ (eraseNone : (a : Finset (Option α)) → Finset α) (map Embedding.some s) = s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset α
a : α
⊢ Membership.mem (γ := Finset α) ((eraseNone : (a : Finset (Option α)) → Finset α) (map Embedding.some s) : Finset α)
      a ↔
    a ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
inst : DecidableEq (Option α)
s : Finset α
⊢ (eraseNone : (a : Finset (Option α)) → Finset α) (image some s) = s

Tactic:
simpa only [map_eq_image] using eraseNone_map_some s

Premises used: Finset.eraseNone_map_some, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Option
Goal:
α : Type u_1
s : Finset (Option α)
⊢ (↑((eraseNone : (a : Finset (Option α)) → Finset α) s : Finset α) : Set α) = some ⁻¹' (↑s : Set (Option α))

Tactic:
Set.ext fun _ => mem_eraseNone

Premises used: Set.ext, Finset.mem_eraseNone