case intro
α : Type u_1
inst✝ : CommSemigroup α
a c✝ c : α
⊢ a ∣ c * a
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ (∃ c, b = c * a) → a ∣ b
rintro ⟨c, rfl⟩
no goals
case intro
α : Type u_1
inst✝ : CommSemigroup α
a c✝ c : α
⊢ a ∣ c * a
exact ⟨c, mul_comm _ _⟩