no goals
α : Type u_1
β : Type ?u.104187
γ : Type ?u.104190
δ : Type ?u.104193
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
⊢ p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz
no goals
α : Type u_1
β : Type ?u.104187
γ : Type ?u.104190
δ : Type ?u.104193
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝² : p ^ k ∣ a
x✝¹ : p ^ l ∣ b
x✝ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
⊢ x * y = p * z
rwa [mul_right_inj' hp0] at h
no goals
α : Type u_1
β : Type ?u.104187
γ : Type ?u.104190
δ : Type ?u.104193
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ x
d : α
hd : x = p * d
⊢ a = p ^ (k + 1) * d
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]
no goals
α : Type u_1
β : Type ?u.104187
γ : Type ?u.104190
δ : Type ?u.104193
inst✝ : CancelCommMonoidWithZero α
a✝ p : α
hp : Prime p
a b : α
k l : ℕ
x✝³ : p ^ k ∣ a
x✝² : p ^ l ∣ b
x✝¹ : p ^ (k + l + 1) ∣ a * b
x : α
hx : a = p ^ k * x
y : α
hy : b = p ^ l * y
z : α
hz : a * b = p ^ (k + l + 1) * z
h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z)
hp0 : p ^ (k + l) ≠ 0
hpd : p ∣ x * y
x✝ : p ∣ y
d : α
hd : y = p * d
⊢ b = p ^ (l + 1) * d
simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]