Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Amelia Livingston, Yury Kudryashov,
Neil Strickland, Aaron Anderson
Ported by: Matej Penciak

! This file was ported from Lean 3 source module algebra.divisibility.basic
! leanprover-community/mathlib commit e8638a0fcaf73e4500469f368ef9494e495099b3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group

/-!
# Divisibility

This file defines the basics of the divisibility relation in the context of `(Comm)` `Monoid`s.

## Main definitions

* `semigroupDvd`

## Implementation notes

The divisibility relation is defined for all monoids, and as such, depends on the order of
multiplication if the monoid is not commutative. There are two possible conventions for
divisibility in the noncommutative context, and this relation follows the convention for ordinals,
so `a | b` is defined as `∃ c, b = a * c`.

## Tags

divisibility, divides
-/

variable {α: Type ?u.6848α : Type _: Type (?u.7449+1)Type _}

section Semigroup

variable [Semigroup: Type ?u.8 → Type ?u.8Semigroup α: Type ?u.5α] {a: αa b: αb c: αc : α: Type ?u.1639α}

/-- There are two possible conventions for divisibility, which coincide in a `CommMonoid`.
This matches the convention for ordinals. -/
instance (priority := 100) semigroupDvd: {α : Type u_1} → [inst : Semigroup α] → Dvd αsemigroupDvd : Dvd: Type ?u.29 → Type ?u.29Dvd α: Type ?u.17α :=
Dvd.mk: {α : Type ?u.31} → (α → α → Prop) → Dvd αDvd.mk fun a: ?m.35a b: ?m.38b => ∃ c: ?m.43c, b: ?m.38b = a: ?m.35a * c: ?m.43c
#align semigroup_has_dvd semigroupDvd: {α : Type u_1} → [inst : Semigroup α] → Dvd αsemigroupDvd

-- TODO: this used to not have `c` explicit, but that seems to be important
--       for use with tactics, similar to `Exists.intro`
theorem Dvd.intro: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro (c: αc : α: Type ?u.423α) (h: a * c = bh : a: αa * c: αc = b: αb) : a: αa ∣ b: αb :=
Exists.intro: ∀ {α : Sort ?u.788} {p : α → Prop} (w : α), p w → Exists pExists.intro c: αc h: a * c = bh.symm: ∀ {α : Sort ?u.796} {a b : α}, a = b → b = asymm
#align dvd.intro Dvd.intro: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro

alias Dvd.intro: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro ← dvd_of_mul_right_eq: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bdvd_of_mul_right_eq
#align dvd_of_mul_right_eq dvd_of_mul_right_eq: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bdvd_of_mul_right_eq

theorem exists_eq_mul_right_of_dvd: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∃ c, b = a * cexists_eq_mul_right_of_dvd (h: a ∣ bh : a: αa ∣ b: αb) : ∃ c: ?m.852c, b: αb = a: αa * c: ?m.852c :=
h: a ∣ bh
#align exists_eq_mul_right_of_dvd exists_eq_mul_right_of_dvd: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∃ c, b = a * cexists_eq_mul_right_of_dvd

theorem Dvd.elim: ∀ {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → PDvd.elim {P: PropP : Prop: TypeProp} {a: αa b: αb : α: Type ?u.1188α} (H₁: a ∣ bH₁ : a: αa ∣ b: αb) (H₂: ∀ (c : α), b = a * c → PH₂ : ∀ c: ?m.1229c, b: αb = a: αa * c: ?m.1229c → P: PropP) : P: PropP :=
Exists.elim: ∀ {α : Sort ?u.1566} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → bExists.elim H₁: a ∣ bH₁ H₂: ∀ (c : α), b = a * c → PH₂
#align dvd.elim Dvd.elim: ∀ {α : Type u_1} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → PDvd.elim

attribute [local simp] mul_assoc: ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc mul_comm: ∀ {G : Type u_1} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm mul_left_comm: ∀ {G : Type u_1} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)mul_left_comm

@[trans]
theorem dvd_trans: a ∣ b → b ∣ c → a ∣ cdvd_trans : a: αa ∣ b: αb → b: αb ∣ c: αc → a: αa ∣ c: αc
| ⟨d: αd, h₁: b = a * dh₁⟩, ⟨e: αe, h₂: c = b * eh₂⟩ => ⟨d: αd * e: αe, h₁: b = a * dh₁ ▸ h₂: c = b * eh₂.trans: ∀ {α : Sort ?u.2211} {a b c : α}, a = b → b = c → a = ctrans <| mul_assoc: ∀ {G : Type ?u.2235} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc a: αa d: αd e: αe⟩
#align dvd_trans dvd_trans: ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ cdvd_trans

alias dvd_trans: ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ cdvd_trans ← Dvd.dvd.trans: ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ cDvd.dvd.trans

/-- Transitivity of `|` for use in `calc` blocks. -/
instance: ∀ {α : Type u_1} [inst : Semigroup α], IsTrans α Dvd.dvdinstance : IsTrans: (α : Type ?u.2285) → (α → α → Prop) → PropIsTrans α: Type ?u.2273α Dvd.dvd: {α : Type ?u.2286} → [self : Dvd α] → α → α → PropDvd.dvd :=
⟨fun _: ?m.2326_ _: ?m.2329_ _: ?m.2332_ => dvd_trans: ∀ {α : Type ?u.2334} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ cdvd_trans⟩

@[simp]
theorem dvd_mul_right: ∀ (a b : α), a ∣ a * bdvd_mul_right (a: αa b: αb : α: Type ?u.2396α) : a: αa ∣ a: αa * b: αb :=
Dvd.intro: ∀ {α : Type ?u.2759} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro b: αb rfl: ∀ {α : Sort ?u.2778} {a : α}, a = arfl
#align dvd_mul_right dvd_mul_right: ∀ {α : Type u_1} [inst : Semigroup α] (a b : α), a ∣ a * bdvd_mul_right

theorem dvd_mul_of_dvd_left: a ∣ b → ∀ (c : α), a ∣ b * cdvd_mul_of_dvd_left (h: a ∣ bh : a: αa ∣ b: αb) (c: αc : α: Type ?u.2819α) : a: αa ∣ b: αb * c: αc :=
h: a ∣ bh.trans: ∀ {α : Type ?u.3188} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ ctrans (dvd_mul_right: ∀ {α : Type ?u.3215} [inst : Semigroup α] (a b : α), a ∣ a * bdvd_mul_right b: αb c: αc)
#align dvd_mul_of_dvd_left dvd_mul_of_dvd_left: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * cdvd_mul_of_dvd_left

alias dvd_mul_of_dvd_left: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * cdvd_mul_of_dvd_left ← Dvd.dvd.mul_right: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * cDvd.dvd.mul_right

theorem dvd_of_mul_right_dvd: a * b ∣ c → a ∣ cdvd_of_mul_right_dvd (h: a * b ∣ ch : a: αa * b: αb ∣ c: αc) : a: αa ∣ c: αc :=
(dvd_mul_right: ∀ {α : Type ?u.3590} [inst : Semigroup α] (a b : α), a ∣ a * bdvd_mul_right a: αa b: αb).trans: ∀ {α : Type ?u.3601} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ ctrans h: a * b ∣ ch
#align dvd_of_mul_right_dvd dvd_of_mul_right_dvd: ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a * b ∣ c → a ∣ cdvd_of_mul_right_dvd

section map_dvd

variable {M: Type ?u.3639M N: Type ?u.3642N : Type _: Type (?u.4629+1)Type _} [Monoid: Type ?u.3669 → Type ?u.3669Monoid M: Type ?u.3663M] [Monoid: Type ?u.3672 → Type ?u.3672Monoid N: Type ?u.3642N]

theorem map_dvd: ∀ {F : Type u_1} [inst : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f bmap_dvd {F: Type ?u.3675F : Type _: Type (?u.3675+1)Type _} [MulHomClass: Type ?u.3680 →
(M : outParam (Type ?u.3679)) →
(N : outParam (Type ?u.3678)) → [inst : Mul M] → [inst : Mul N] → Type (max(max?u.3680?u.3679)?u.3678)MulHomClass F: Type ?u.3675F M: Type ?u.3663M N: Type ?u.3666N] (f: Ff : F: Type ?u.3675F) {a: Ma b: Mb} : a: ?m.3833a ∣ b: ?m.3836b → f: Ff a: ?m.3833a ∣ f: Ff b: ?m.3836b
| ⟨c: Mc, h: b = a * ch⟩ => ⟨f: Ff c: Mc, h: b = a * ch.symm: ∀ {α : Sort ?u.4309} {a b : α}, a = b → b = asymm ▸ map_mul: ∀ {M : Type ?u.4321} {N : Type ?u.4322} {F : Type ?u.4320} [inst : Mul M] [inst_1 : Mul N] [inst_2 : MulHomClass F M N]
(f : F) (x y : M), ↑f (x * y) = ↑f x * ↑f ymap_mul f: Ff a: Ma c: Mc⟩
#align map_dvd map_dvd: ∀ {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] {F : Type u_1} [inst_2 : MulHomClass F M N]
(f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f bmap_dvd

theorem MulHom.map_dvd: ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (f : M →ₙ* N) {a b : M}, a ∣ b → ↑f a ∣ ↑f bMulHom.map_dvd (f: M →ₙ* Nf : M: Type ?u.4629M →ₙ* N: Type ?u.4632N) {a: ?m.4793a b: Mb} : a: ?m.4793a ∣ b: ?m.4796b → f: M →ₙ* Nf a: ?m.4793a ∣ f: M →ₙ* Nf b: ?m.4796b :=
_root_.map_dvd: ∀ {M : Type ?u.5138} {N : Type ?u.5139} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.5137}
[inst_2 : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f b_root_.map_dvd f: M →ₙ* Nf
#align mul_hom.map_dvd MulHom.map_dvd: ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (f : M →ₙ* N) {a b : M}, a ∣ b → ↑f a ∣ ↑f bMulHom.map_dvd

theorem MonoidHom.map_dvd: ∀ (f : M →* N) {a b : M}, a ∣ b → ↑f a ∣ ↑f bMonoidHom.map_dvd (f: M →* Nf : M: Type ?u.5268M →* N: Type ?u.5271N) {a: ?m.5388a b: Mb} : a: ?m.5388a ∣ b: ?m.5391b → f: M →* Nf a: ?m.5388a ∣ f: M →* Nf b: ?m.5391b :=
_root_.map_dvd: ∀ {M : Type ?u.6147} {N : Type ?u.6148} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.6146}
[inst_2 : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f b_root_.map_dvd f: M →* Nf
#align monoid_hom.map_dvd MonoidHom.map_dvd: ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) {a b : M}, a ∣ b → ↑f a ∣ ↑f bMonoidHom.map_dvd

end map_dvd

end Semigroup

section Monoid

variable [Monoid: Type ?u.7452 → Type ?u.7452Monoid α: Type ?u.6482α] {a: αa b: αb : α: Type ?u.6848α}

@[refl, simp]
theorem dvd_refl: ∀ {α : Type u_1} [inst : Monoid α] (a : α), a ∣ advd_refl (a: αa : α: Type ?u.6482α) : a: αa ∣ a: αa :=
Dvd.intro: ∀ {α : Type ?u.6562} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro 1: ?m.66281 (mul_one: ∀ {M : Type ?u.6725} [inst : MulOneClass M] (a : M), a * 1 = amul_one a: αa)
#align dvd_refl dvd_refl: ∀ {α : Type u_1} [inst : Monoid α] (a : α), a ∣ advd_refl

theorem dvd_rfl: ∀ {a : α}, a ∣ advd_rfl : ∀ {a: αa : α: Type ?u.6848α}, a: αa ∣ a: αa := fun {a: ?m.6929a} => dvd_refl: ∀ {α : Type ?u.6931} [inst : Monoid α] (a : α), a ∣ advd_refl a: ?m.6929a
#align dvd_rfl dvd_rfl: ∀ {α : Type u_1} [inst : Monoid α] {a : α}, a ∣ advd_rfl

instance: ∀ {α : Type u_1} [inst : Monoid α], IsRefl α fun x x_1 => x ∣ x_1instance : IsRefl: (α : Type ?u.6958) → (α → α → Prop) → PropIsRefl α: Type ?u.6948α (· ∣ ·): α → α → Prop(· ∣ ·) :=
⟨dvd_refl: ∀ {α : Type ?u.7046} [inst : Monoid α] (a : α), a ∣ advd_refl⟩

theorem one_dvd: ∀ (a : α), 1 ∣ aone_dvd (a: αa : α: Type ?u.7095α) : 1: ?m.71141 ∣ a: αa :=
Dvd.intro: ∀ {α : Type ?u.7277} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro a: αa (one_mul: ∀ {M : Type ?u.7342} [inst : MulOneClass M] (a : M), 1 * a = aone_mul a: αa)
#align one_dvd one_dvd: ∀ {α : Type u_1} [inst : Monoid α] (a : α), 1 ∣ aone_dvd

theorem dvd_of_eq: a = b → a ∣ bdvd_of_eq (h: a = bh : a: αa = b: αb) : a: αa ∣ b: αb := byGoals accomplished! 🐙 α: Type u_1inst✝: Monoid αa, b: αh: a = ba ∣ brw [α: Type u_1inst✝: Monoid αa, b: αh: a = ba ∣ bh: a = bhα: Type u_1inst✝: Monoid αa, b: αh: a = bb ∣ b]Goals accomplished! 🐙
#align dvd_of_eq dvd_of_eq: ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ bdvd_of_eq

alias dvd_of_eq: ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ bdvd_of_eq ← Eq.dvd: ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ bEq.dvd
#align eq.dvd Eq.dvd: ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ bEq.dvd

end Monoid

section CommSemigroup

variable [CommSemigroup: Type ?u.11087 → Type ?u.11087CommSemigroup α: Type ?u.7566α] {a: αa b: αb c: αc : α: Type ?u.7566α}

theorem Dvd.intro_left: ∀ (c : α), c * a = b → a ∣ bDvd.intro_left (c: αc : α: Type ?u.7578α) (h: c * a = bh : c: αc * a: αa = b: αb) : a: αa ∣ b: αb :=
Dvd.intro: ∀ {α : Type ?u.8096} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro _: ?m.8097_ (byGoals accomplished! 🐙 α: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh: c * a = ba * ?m.8324 c h = brw [α: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh: c * a = ba * ?m.8324 c h = bmul_comm: ∀ {G : Type ?u.8326} [inst : CommSemigroup G] (a b : G), a * b = b * amul_commα: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh✝: c * a = bh: a * c = ba * ?m.8324 c h✝ = b]α: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh✝: c * a = bh: a * c = ba * ?m.8324 c h✝ = b at h: c * a = bhα: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh✝: c * a = bh: a * c = ba * ?m.8324 c h✝ = b;α: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh✝: c * a = bh: a * c = ba * ?m.8324 c h✝ = b α: Type u_1inst✝: CommSemigroup αa, b, c✝, c: αh: c * a = ba * ?m.8324 c h = bapply h: a * c = bhGoals accomplished! 🐙)
#align dvd.intro_left Dvd.intro_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ bDvd.intro_left

alias Dvd.intro_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ bDvd.intro_left ← dvd_of_mul_left_eq: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ bdvd_of_mul_left_eq
#align dvd_of_mul_left_eq dvd_of_mul_left_eq: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ bdvd_of_mul_left_eq

theorem exists_eq_mul_left_of_dvd: a ∣ b → ∃ c, b = c * aexists_eq_mul_left_of_dvd (h: a ∣ bh : a: αa ∣ b: αb) : ∃ c: ?m.8587c, b: αb = c: ?m.8587c * a: αa :=
Dvd.elim: ∀ {α : Type ?u.8919} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → PDvd.elim h: a ∣ bh fun c: ?m.8988c => fun H1: b = a * cH1 : b: αb = a: αa * c: ?m.8988c => Exists.intro: ∀ {α : Sort ?u.9361} {p : α → Prop} (w : α), p w → Exists pExists.intro c: ?m.8988c (Eq.trans: ∀ {α : Sort ?u.9369} {a b c : α}, a = b → b = c → a = cEq.trans H1: b = a * cH1 (mul_comm: ∀ {G : Type ?u.9374} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm a: αa c: ?m.8988c))
#align exists_eq_mul_left_of_dvd exists_eq_mul_left_of_dvd: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * aexists_eq_mul_left_of_dvd

theorem dvd_iff_exists_eq_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = c * advd_iff_exists_eq_mul_left : a: αa ∣ b: αb ↔ ∃ c: ?m.9696c, b: αb = c: ?m.9696c * a: αa :=
⟨exists_eq_mul_left_of_dvd: ∀ {α : Type ?u.10035} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * aexists_eq_mul_left_of_dvd, byGoals accomplished! 🐙
α: Type u_1inst✝: CommSemigroup αa, b, c: α(∃ c, b = c * a) → a ∣ brintro ⟨c, rfl⟩: ∃ c, b = c * a⟨c: αc⟨c, rfl⟩: ∃ c, b = c * a, rfl: b = c * arfl⟨c, rfl⟩: ∃ c, b = c * a⟩α: Type u_1inst✝: CommSemigroup αa, c✝, c: αintroa ∣ c * a
α: Type u_1inst✝: CommSemigroup αa, b, c: α(∃ c, b = c * a) → a ∣ bexact ⟨c: αc, mul_comm: ∀ {G : Type ?u.10105} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm _: ?m.10106_ _: ?m.10106_⟩Goals accomplished! 🐙⟩
#align dvd_iff_exists_eq_mul_left dvd_iff_exists_eq_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = c * advd_iff_exists_eq_mul_left

theorem Dvd.elim_left: ∀ {P : Prop}, a ∣ b → (∀ (c : α), b = c * a → P) → PDvd.elim_left {P: PropP : Prop: TypeProp} (h₁: a ∣ bh₁ : a: αa ∣ b: αb) (h₂: ∀ (c : α), b = c * a → Ph₂ : ∀ c: ?m.10324c, b: αb = c: ?m.10324c * a: αa → P: PropP) : P: PropP :=
Exists.elim: ∀ {α : Sort ?u.10661} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → bExists.elim (exists_eq_mul_left_of_dvd: ∀ {α : Type ?u.10665} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * aexists_eq_mul_left_of_dvd h₁: a ∣ bh₁) fun c: ?m.10693c => fun h₃: b = c * ah₃ : b: αb = c: ?m.10693c * a: αa => h₂: ∀ (c : α), b = c * a → Ph₂ c: ?m.10693c h₃: b = c * ah₃
#align dvd.elim_left Dvd.elim_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} {P : Prop}, a ∣ b → (∀ (c : α), b = c * a → P) → PDvd.elim_left

@[simp]
theorem dvd_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * advd_mul_left (a: αa b: αb : α: Type ?u.11084α) : a: αa ∣ b: αb * a: αa :=
Dvd.intro: ∀ {α : Type ?u.11600} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro b: αb (mul_comm: ∀ {G : Type ?u.11667} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm a: αa b: αb)
#align dvd_mul_left dvd_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * advd_mul_left

theorem dvd_mul_of_dvd_right: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * bdvd_mul_of_dvd_right (h: a ∣ bh : a: αa ∣ b: αb) (c: αc : α: Type ?u.11862α) : a: αa ∣ c: αc * b: αb := byGoals accomplished! 🐙
α: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ c * brw [α: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ c * bmul_comm: ∀ {G : Type ?u.12386} [inst : CommSemigroup G] (a b : G), a * b = b * amul_commα: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ b * c]α: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ b * c;α: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ b * c α: Type u_1inst✝: CommSemigroup αa, b, c✝: αh: a ∣ bc: αa ∣ c * bexact h: a ∣ bh.mul_right: ∀ {α : Type ?u.12433} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * cmul_right _: ?m.12440_Goals accomplished! 🐙
#align dvd_mul_of_dvd_right dvd_mul_of_dvd_right: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * bdvd_mul_of_dvd_right

alias dvd_mul_of_dvd_right: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * bdvd_mul_of_dvd_right ← Dvd.dvd.mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * bDvd.dvd.mul_left

attribute [local simp] mul_assoc: ∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc mul_comm: ∀ {G : Type u_1} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm mul_left_comm: ∀ {G : Type u_1} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)mul_left_comm

theorem mul_dvd_mul: ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * dmul_dvd_mul : ∀ {a: αa b: αb c: αc d: αd : α: Type ?u.12670α}, a: αa ∣ b: αb → c: αc ∣ d: αd → a: αa * c: αc ∣ b: αb * d: αd
| a: αa, _, c: αc, _, ⟨e: αe, rfl: ∀ {α : Sort ?u.13391} {a : α}, a = arfl⟩, ⟨f: αf, rfl: ∀ {α : Sort ?u.13395} {a : α}, a = arfl⟩ => ⟨e: αe * f: αf, byGoals accomplished! 🐙 α: Type u_1inst✝: CommSemigroup αa✝, b, c✝, a, c, e, f: αa * e * (c * f) = a * c * (e * f)simpGoals accomplished! 🐙⟩
#align mul_dvd_mul mul_dvd_mul: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * dmul_dvd_mul

theorem dvd_of_mul_left_dvd: a * b ∣ c → b ∣ cdvd_of_mul_left_dvd (h: a * b ∣ ch : a: αa * b: αb ∣ c: αc) : b: αb ∣ c: αc :=
Dvd.elim: ∀ {α : Type ?u.15309} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → PDvd.elim h: a * b ∣ ch fun d: ?m.15378d ceq: ?m.15381ceq => Dvd.intro: ∀ {α : Type ?u.15383} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro (a: αa * d: ?m.15378d) (byGoals accomplished! 🐙 α: Type u_1inst✝: CommSemigroup αa, b, c: αh: a * b ∣ cd: αceq: c = a * b * db * (a * d) = csimp [ceq: c = a * b * dceq]Goals accomplished! 🐙)
#align dvd_of_mul_left_dvd dvd_of_mul_left_dvd: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c : α}, a * b ∣ c → b ∣ cdvd_of_mul_left_dvd

end CommSemigroup

section CommMonoid

variable [CommMonoid: Type ?u.16958 → Type ?u.16958CommMonoid α: Type ?u.16202α] {a: αa b: αb : α: Type ?u.16192α}

theorem mul_dvd_mul_left: ∀ {α : Type u_1} [inst : CommMonoid α] (a : α) {b c : α}, b ∣ c → a * b ∣ a * cmul_dvd_mul_left (a: αa : α: Type ?u.16202α) {b: αb c: αc : α: Type ?u.16202α} (h: b ∣ ch : b: αb ∣ c: αc) : a: αa * b: αb ∣ a: αa * c: αc :=
mul_dvd_mul: ∀ {α : Type ?u.16770} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * dmul_dvd_mul (dvd_refl: ∀ {α : Type ?u.16813} [inst : Monoid α] (a : α), a ∣ advd_refl a: αa) h: b ∣ ch
#align mul_dvd_mul_left mul_dvd_mul_left: ∀ {α : Type u_1} [inst : CommMonoid α] (a : α) {b c : α}, b ∣ c → a * b ∣ a * cmul_dvd_mul_left

theorem mul_dvd_mul_right: a ∣ b → ∀ (c : α), a * c ∣ b * cmul_dvd_mul_right (h: a ∣ bh : a: αa ∣ b: αb) (c: αc : α: Type ?u.16955α) : a: αa * c: αc ∣ b: αb * c: αc :=
mul_dvd_mul: ∀ {α : Type ?u.17515} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * dmul_dvd_mul h: a ∣ bh (dvd_refl: ∀ {α : Type ?u.17570} [inst : Monoid α] (a : α), a ∣ advd_refl c: αc)
#align mul_dvd_mul_right mul_dvd_mul_right: ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a * c ∣ b * cmul_dvd_mul_right

theorem pow_dvd_pow_of_dvd: ∀ {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ npow_dvd_pow_of_dvd {a: αa b: αb : α: Type ?u.17700α} (h: a ∣ bh : a: αa ∣ b: αb) : ∀ n: ℕn : ℕ: Typeℕ, a: αa ^ n: ℕn ∣ b: αb ^ n: ℕn
| 0: ℕ0 => byGoals accomplished! 🐙 α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ ba ^ 0 ∣ b ^ 0rw [α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ ba ^ 0 ∣ b ^ 0pow_zero: ∀ {M : Type ?u.23257} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero,α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ b1 ∣ b ^ 0 α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ ba ^ 0 ∣ b ^ 0pow_zero: ∀ {M : Type ?u.23413} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zeroα: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ b1 ∣ 1]Goals accomplished! 🐙
| n: ℕn + 1 => byGoals accomplished! 🐙
α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa ^ (n + 1) ∣ b ^ (n + 1)rw [α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa ^ (n + 1) ∣ b ^ (n + 1)pow_succ: ∀ {M : Type ?u.23459} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succ,α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa * a ^ n ∣ b ^ (n + 1) α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa ^ (n + 1) ∣ b ^ (n + 1)pow_succ: ∀ {M : Type ?u.23490} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ npow_succα: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa * a ^ n ∣ b * b ^ n]α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa * a ^ n ∣ b * b ^ n
α: Type u_1inst✝: CommMonoid αa✝, b✝, a, b: αh: a ∣ bn: ℕa ^ (n + 1) ∣ b ^ (n + 1)exact mul_dvd_mul: ∀ {α : Type ?u.23561} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * dmul_dvd_mul h: a ∣ bh (pow_dvd_pow_of_dvd: ∀ {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ npow_dvd_pow_of_dvd h: a ∣ bh n: ℕn)Goals accomplished! 🐙
#align pow_dvd_pow_of_dvd pow_dvd_pow_of_dvd: ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ npow_dvd_pow_of_dvd

end CommMonoid
```