-- Mathlib/GroupTheory/NoncommPiCoprod.lean
@[to_additive]
lemma commute_noncommPiCoprod {m : M}
    (comm : ∀ i (x : N i), Commute m ((ϕ i x))) (h : (i : ι) → N i) :
    Commute m (MonoidHom.noncommPiCoprod ϕ hcomm h)

Proof state:
case hom
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)

Tactic:
exact fun x y ↦ Commute.mul_right

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m ((noncommPiCoprod ϕ hcomm) h)

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m (Finset.univ.noncommProd (fun i => (ϕ i) (h i)) ⋯)

Proof state:
case unit
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m 1

Tactic:
exact Commute.one_right _

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m (Finset.univ.noncommProd (fun i => (ϕ i) (h i)) ⋯)

Tactic:
apply Finset.noncommProd_induction

Result:
case hom
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ ∀ (a b : M), Commute m a → Commute m b → Commute m (a * b)

case unit
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m 1

case base
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ ∀ x ∈ Finset.univ, Commute m ((ϕ x) (h x))

Proof state:
case base
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ ∀ x ∈ Finset.univ, Commute m ((ϕ x) (h x))

Tactic:
exact fun x _ ↦ comm x (h x)

Result:
no goals