Theorem: Submonoid.bot_prodProperty (Kaplanski4/Absorbing.lean)

State before:
M : Type u_1
N : Type ?u.12181
inst✝ : CommMonoid M
x✝¹ x✝ : M
hxy : x✝¹ * x✝ ∈ ⊥.toSubsemigroup
⊢ x✝ * ?m.13325 x✝¹ x✝ hxy = 1
Tactic:
rwa [mul_comm] at hxy
State after:
no goals