no goals
A : Type ?u.2634
B : Type ?u.2637
G : Type ?u.2640
H : Type ?u.2643
M : Type u_1
N : Type u_2
P : Type ?u.2652
inst✝¹ : Mul M
inst✝ : Monoid N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
rw [mk_mul_mk, mul_one]