case intro
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
⊢ f = g
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
⊢ f = g
cases nonempty_fintype ι
case intro.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ ↑f x = ↑g x
case intro
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
⊢ f = g
ext x
case intro.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ noncommProd univ (fun i => ↑f (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑f (Pi.mulSingle x_1 (x x_1))) (↑f (Pi.mulSingle y (x y)))) =
    noncommProd univ (fun i => ↑g (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑g (Pi.mulSingle x_1 (x x_1))) (↑g (Pi.mulSingle y (x y))))
case intro.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ ↑f x = ↑g x
rw [← noncommProd_mul_single x, univ.noncommProd_map, univ.noncommProd_map]
case intro.h.e_f.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
i : ι
⊢ ↑f (Pi.mulSingle i (x i)) = ↑g (Pi.mulSingle i (x i))
case intro.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ noncommProd univ (fun i => ↑f (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑f (Pi.mulSingle x_1 (x x_1))) (↑f (Pi.mulSingle y (x y)))) =
    noncommProd univ (fun i => ↑g (Pi.mulSingle i (x i)))
      (_ :
        ∀ (x_1 : ι),
          x_1 ∈ ↑univ →
            ∀ (y : ι), y ∈ ↑univ → x_1 ≠ y → Commute (↑g (Pi.mulSingle x_1 (x x_1))) (↑g (Pi.mulSingle y (x y))))
congr 1 with i
no goals
case intro.h.e_f.h
F : Type ?u.241399
ι : Type u_1
α : Type ?u.241405
β : Type ?u.241408
γ : Type u_3
f✝ : α → β → β
op : α → α → α
inst✝⁴ : Monoid β
inst✝³ : Monoid γ
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), ↑f (Pi.mulSingle i x) = ↑g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
i : ι
⊢ ↑f (Pi.mulSingle i (x i)) = ↑g (Pi.mulSingle i (x i))
exact h i (x i)