-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
    (univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ =>
        Pi.mulSingle_apply_commute x i j) = x

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : j ∈ univ.erase i
⊢ Pi.mulSingle j (x j) i = 1

Tactic:
simp only [mem_erase, ne_eq, mem_univ, and_true] at hj

Result:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ Pi.mulSingle j (x j) i = 1

Proof state:
case h.convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ M i

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

Result:
no goals

Proof state:
case h.convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i = x i

Tactic:
simp only [MonoidHom.mulSingle_apply, ne_eq, Pi.mulSingle_eq_same]

Result:
no goals

Proof state:
case h.convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
a✝ : j ∈ insert i (univ.erase i)
⊢ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M j) (x j)) = Pi.mulSingle j (x j) i

Tactic:
dsimp

Result:
no goals

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
h : i = j
⊢ ⋯ ▸ x j = 1

Tactic:
simp [*] at *

Result:
no goals

Proof state:
case h.convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

Tactic:
intro j _

Result:
case h.convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
a✝ : j ∈ insert i (univ.erase i)
⊢ (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M j) (x j)) = Pi.mulSingle j (x j) i

Proof state:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i => (MonoidHom.mulSingle M i) (x i))

Tactic:
intro i _ j _ _

Result:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝² : i ∈ ↑univ
j : ι
a✝¹ : j ∈ ↑univ
a✝ : i ≠ j
⊢ (Commute on fun i => (MonoidHom.mulSingle M i) (x i)) i j

Proof state:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 => (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

case a
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i => (MonoidHom.mulSingle M i) (x i))

Tactic:
case a =>
  intro i _ j _ _
  exact Pi.mulSingle_apply_commute x i j

Result:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 => (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1

Tactic:
intro j hj

Result:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : j ∈ univ.erase i
⊢ Pi.mulSingle j (x j) i = 1

Proof state:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i => Pi.mulSingle 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

Result:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 => (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

case a
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (↑univ).Pairwise (Commute on fun i => (MonoidHom.mulSingle M i) (x i))

Proof state:
case h.convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

Tactic:
intro j

Result:
case h.convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ M i

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ ∀ (h : i = j), ⋯ ▸ x j = 1

Tactic:
intro h

Result:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
h : i = j
⊢ ⋯ ▸ x j = 1

Proof state:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
⊢ univ.noncommProd (fun i => Pi.mulSingle i (x i)) ⋯ = x

Tactic:
ext i

Result:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i => Pi.mulSingle i (x i)) ⋯ i = x i

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ Pi.mulSingle j (x j) i = 1

Tactic:
simp only [MonoidHom.mulSingle_apply, Pi.mulSingle, Function.update, Eq.ndrec, Pi.one_apply,
  ne_eq, dite_eq_right_iff]

Result:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ ∀ (h : i = j), ⋯ ▸ x j = 1

Proof state:
case h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ univ.noncommProd (fun i_1 => (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i

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

Result:
case h.convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

case h.convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i), (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = ?h.convert_3 x_1

case h.convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd ?h.convert_3 ⋯ = x i

Proof state:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : j ∈ univ.erase i
⊢ Pi.mulSingle j (x j) i = 1

Tactic:
simp? at hj says simp only [mem_erase, ne_eq, mem_univ, and_true] at hj

Result:
case h.convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
hj : ¬j = i
⊢ Pi.mulSingle j (x j) i = 1