[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
Eq : b * ↑u = a * c
⊢ b = a * (c * ↑u⁻¹)
[PROOFSTEP]
rw [← mul_assoc, ← Eq, Units.mul_inv_cancel_right]
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, u.mul_inv, mul_one]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
[PROOFSTEP]
apply mul_right_dvd
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ u ∣ a
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ ↑u ∣ a
[PROOFSTEP]
apply Units.coe_dvd
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
[PROOFSTEP]
apply Units.dvd_mul_right
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
[PROOFSTEP]
apply Units.mul_right_dvd
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
[PROOFSTEP]
apply Units.dvd_mul_left
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
apply Units.mul_left_dvd
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1
[PROOFSTEP]
rw [h, mul_comm]
