[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h : c * a = b
⊢ a * ?m.8269 c h = b
[PROOFSTEP]
rw [mul_comm] at h 
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h✝ : c * a = b
h : a * c = b
⊢ a * ?m.8269 c h✝ = b
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ (∃ c, b = c * a) → a ∣ b
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommSemigroup α
a c✝ c : α
⊢ a ∣ c * a
[PROOFSTEP]
exact ⟨c, mul_comm _ _⟩
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ c * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ b * c
[PROOFSTEP]
exact h.mul_right _
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a✝ b c✝ a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c
[PROOFSTEP]
simp [ceq]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a ^ (n + 1) ∣ b ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a * a ^ n ∣ b * b ^ n
[PROOFSTEP]
exact mul_dvd_mul h (pow_dvd_pow_of_dvd h n)
