no goals
α : Type u_1
β : Type ?u.218014
γ : Type ?u.218017
δ : Type ?u.218020
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ p = p * ↑u * ↑u⁻¹
simp
α : Type u_1
β : Type ?u.218014
γ : Type ?u.218017
δ : Type ?u.218020
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
α : Type u_1
β : Type ?u.218014
γ : Type ?u.218017
δ : Type ?u.218020
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ p * ↑u * ↑u⁻¹ = a * (b * ↑u⁻¹)
rw [hu]
no goals
α : Type u_1
β : Type ?u.218014
γ : Type ?u.218017
δ : Type ?u.218020
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)
simp [hab, mul_assoc]
no goals
α : Type u_1
β : Type ?u.218014
γ : Type ?u.218017
δ : Type ?u.218020
inst✝ : Monoid α
p q : α
h : p ~ᵤ q
hp : Irreducible p
u : αˣ
hu : p * ↑u = q
a b : α
hab : q = a * b
hpab : p = a * (b * ↑u⁻¹)
x✝ : IsUnit (b * ↑u⁻¹)
v : αˣ
hv : ↑v = b * ↑u⁻¹
⊢ ↑(v * u) = b
simp [hv]