α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
⊢ a ∣ b
α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
⊢ ∀ (c : α), Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c → a ∣ b
intro c hc
α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
d : αˣ
hd : a * c * ↑d = b
⊢ a ∣ b
α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
⊢ a ∣ b
let ⟨d, hd⟩ := (Quotient.exact hc).symm
no goals
α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
d : αˣ
hd : a * c * ↑d = b
⊢ a ∣ b
exact ⟨↑d * c,
    calc
      b = a * c * ↑d := hd.symm
      _ = a * (↑d * c) := by ac_rfl
      ⟩
no goals
α : Type u_1
β : Type ?u.301851
γ : Type ?u.301854
δ : Type ?u.301857
inst✝ : CommMonoid α
a b : α
c' : Associates α
hc' : Associates.mk b = Associates.mk a * c'
c : α
hc : Associates.mk b = Associates.mk a * Quotient.mk (Associated.setoid α) c
d : αˣ
hd : a * c * ↑d = b
⊢ a * c * ↑d = a * (↑d * c)
ac_rfl