-- Mathlib/Data/Finset/NoncommProd.lean
theorem _root_.MonoidHom.pi_ext [Finite ι] [DecidableEq ι] {f g : (∀ i, M i) →* γ}
    (h : ∀ i x, f (Pi.mulSingle i x) = g (Pi.mulSingle i x)) : f = g

Proof state:
case intro.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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

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

Result:
case intro.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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
⊢ univ.noncommProd (fun i => f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i => g (Pi.mulSingle i (x i))) ⋯

Proof state:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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

Tactic:
ext x

Result:
case intro.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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

Proof state:
case intro.h.e_f.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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))

Tactic:
exact h i (x i)

Result:
no goals

Proof state:
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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

Proof state:
case intro.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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
⊢ univ.noncommProd (fun i => f (Pi.mulSingle i (x i))) ⋯ = univ.noncommProd (fun i => g (Pi.mulSingle i (x i))) ⋯

Tactic:
congr 1 with i

Result:
case intro.h.e_f.h
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
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))