no goals
A : Type ?u.1848
B : Type ?u.1851
G : Type ?u.1854
H : Type ?u.1857
M : Type u_1
N : Type u_2
P : Type ?u.1866
inst✝¹ : Monoid M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)
rw [mk_mul_mk, mul_one]