rw [← one_mul (p^m)] at hm
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z
case intro
M : Type ?u.8793
N : Type ?u.8796
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : x * y ∈ (Submonoid.powers p).toSubsemigroup
m : ℕ
hm : 1 * p ^ m = x * y
⊢ (∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated x z) ∧
    ∃ z ∈ (Submonoid.powers p).toSubsemigroup, Associated y z