/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.8
Semigroup α: 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.29
Dvd α: Type ?u.17
α :=
  Dvd.mk: {α : Type ?u.31} → (α → α → Prop) → Dvd α
Dvd.mk fun a: ?m.35
a b: ?m.38
b => ∃ c: ?m.43
c, b: ?m.38
b = a: ?m.35
a * c: ?m.43
c
#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 ∣ b
Dvd.intro (c: α
c : α: Type ?u.423
α) (h: a * c = b
h : a: α
a * c: α
c = b: α
b) : a: α
a ∣ b: α
b :=
  Exists.intro: ∀ {α : Sort ?u.788} {p : α → Prop} (w : α), p w → Exists p
Exists.intro c: α
c h: a * c = b
h.symm: ∀ {α : Sort ?u.796} {a b : α}, a = b → b = a
symm
#align dvd.intro Dvd.intro: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
Dvd.intro

alias Dvd.intro: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
Dvd.intro ← dvd_of_mul_right_eq: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
dvd_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 ∣ b
dvd_of_mul_right_eq

theorem exists_eq_mul_right_of_dvd: ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∃ c, b = a * c
exists_eq_mul_right_of_dvd (h: a ∣ b
h : a: α
a ∣ b: α
b) : ∃ c: ?m.852
c, b: α
b = a: α
a * c: ?m.852
c :=
  h: a ∣ b
h
#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 * c
exists_eq_mul_right_of_dvd

theorem Dvd.elim: ∀ {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → P
Dvd.elim {P: Prop
P : Prop: Type
Prop} {a: α
a b: α
b : α: Type ?u.1188
α} (H₁: a ∣ b
H₁ : a: α
a ∣ b: α
b) (H₂: ∀ (c : α), b = a * c → P
H₂ : ∀ c: ?m.1229
c, b: α
b = a: α
a * c: ?m.1229
c → P: Prop
P) : P: Prop
P :=
  Exists.elim: ∀ {α : Sort ?u.1566} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
Exists.elim H₁: a ∣ b
H₁ H₂: ∀ (c : α), b = a * c → P
H₂
#align dvd.elim Dvd.elim: ∀ {α : Type u_1} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → P
Dvd.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 * a
mul_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 ∣ c
dvd_trans : a: α
a ∣ b: α
b → b: α
b ∣ c: α
c → a: α
a ∣ c: α
c
  | ⟨d: α
d, h₁: b = a * d
h₁⟩, ⟨e: α
e, h₂: c = b * e
h₂⟩ => ⟨d: α
d * e: α
e, h₁: b = a * d
h₁ ▸ h₂: c = b * e
h₂.trans: ∀ {α : Sort ?u.2211} {a b c : α}, a = b → b = c → a = c
trans <| 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 ∣ c
dvd_trans

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

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

@[simp]
theorem dvd_mul_right: ∀ (a b : α), a ∣ a * b
dvd_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 ∣ b
Dvd.intro b: α
b rfl: ∀ {α : Sort ?u.2778} {a : α}, a = a
rfl
#align dvd_mul_right dvd_mul_right: ∀ {α : Type u_1} [inst : Semigroup α] (a b : α), a ∣ a * b
dvd_mul_right

theorem dvd_mul_of_dvd_left: a ∣ b → ∀ (c : α), a ∣ b * c
dvd_mul_of_dvd_left (h: a ∣ b
h : a: α
a ∣ b: α
b) (c: α
c : α: Type ?u.2819
α) : a: α
a ∣ b: α
b * c: α
c :=
  h: a ∣ b
h.trans: ∀ {α : Type ?u.3188} [inst : Semigroup α] {a b c : α}, a ∣ b → b ∣ c → a ∣ c
trans (dvd_mul_right: ∀ {α : Type ?u.3215} [inst : Semigroup α] (a b : α), a ∣ a * b
dvd_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 * c
dvd_mul_of_dvd_left

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

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

section map_dvd

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

theorem map_dvd: ∀ {F : Type u_1} [inst : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f b
map_dvd {F: Type ?u.3675
F : 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.3675
F M: Type ?u.3663
M N: Type ?u.3666
N] (f: F
f : F: Type ?u.3675
F) {a: M
a b: M
b} : a: ?m.3833
a ∣ b: ?m.3836
b → f: F
f a: ?m.3833
a ∣ f: F
f b: ?m.3836
b
  | ⟨c: M
c, h: b = a * c
h⟩ => ⟨f: F
f c: M
c, h: b = a * c
h.symm: ∀ {α : Sort ?u.4309} {a b : α}, a = b → b = a
symm ▸ 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 y
map_mul f: F
f a: M
a c: M
c⟩
#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 b
map_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 b
MulHom.map_dvd (f: M →ₙ* N
f : M: Type ?u.4629
M →ₙ* N: Type ?u.4632
N) {a: ?m.4793
a b: M
b} : a: ?m.4793
a ∣ b: ?m.4796
b → f: M →ₙ* N
f a: ?m.4793
a ∣ f: M →ₙ* N
f b: ?m.4796
b :=
  _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 →ₙ* N
f
#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 b
MulHom.map_dvd

theorem MonoidHom.map_dvd: ∀ (f : M →* N) {a b : M}, a ∣ b → ↑f a ∣ ↑f b
MonoidHom.map_dvd (f: M →* N
f : M: Type ?u.5268
M →* N: Type ?u.5271
N) {a: ?m.5388
a b: M
b} : a: ?m.5388
a ∣ b: ?m.5391
b → f: M →* N
f a: ?m.5388
a ∣ f: M →* N
f b: ?m.5391
b :=
  _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 →* N
f
#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 b
MonoidHom.map_dvd

end map_dvd

end Semigroup

section Monoid

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

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

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

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

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

theorem dvd_of_eq: a = b → a ∣ b
dvd_of_eq (h: a = b
h : a: α
a = b: α
b) : a: α
a ∣ b: α
b := by
Goals accomplished! 🐙 α: Type u_1

inst✝: Monoid α

a, b: α

h: a = b

a ∣ brw [α: Type u_1

inst✝: Monoid α

a, b: α

h: a = b

a ∣ bh: a = b
hα: Type u_1

inst✝: Monoid α

a, b: α

h: a = b

b ∣ b]
Goals accomplished! 🐙
#align dvd_of_eq dvd_of_eq: ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ b
dvd_of_eq

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

end Monoid

section CommSemigroup

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

theorem Dvd.intro_left: ∀ (c : α), c * a = b → a ∣ b
Dvd.intro_left (c: α
c : α: Type ?u.7578
α) (h: c * a = b
h : c: α
c * a: α
a = b: α
b) : a: α
a ∣ b: α
b :=
  Dvd.intro: ∀ {α : Type ?u.8096} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
Dvd.intro _: ?m.8097
_ (by
Goals accomplished! 🐙 α: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h: c * a = b

a * ?m.8324 c h = brw [α: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h: c * a = b

a * ?m.8324 c h = bmul_comm: ∀ {G : Type ?u.8326} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_commα: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h✝: c * a = b

h: a * c = b

a * ?m.8324 c h✝ = b]α: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h✝: c * a = b

h: a * c = b

a * ?m.8324 c h✝ = b at h: c * a = b
hα: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h✝: c * a = b

h: a * c = b

a * ?m.8324 c h✝ = b;α: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h✝: c * a = b

h: a * c = b

a * ?m.8324 c h✝ = b α: Type u_1

inst✝: CommSemigroup α

a, b, c✝, c: α

h: c * a = b

a * ?m.8324 c h = bapply h: a * c = b
h
Goals accomplished! 🐙)
#align dvd.intro_left Dvd.intro_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
Dvd.intro_left

alias Dvd.intro_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
Dvd.intro_left ← dvd_of_mul_left_eq: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α} (c : α), c * a = b → a ∣ b
dvd_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 ∣ b
dvd_of_mul_left_eq

theorem exists_eq_mul_left_of_dvd: a ∣ b → ∃ c, b = c * a
exists_eq_mul_left_of_dvd (h: a ∣ b
h : a: α
a ∣ b: α
b) : ∃ c: ?m.8587
c, b: α
b = c: ?m.8587
c * a: α
a :=
  Dvd.elim: ∀ {α : Type ?u.8919} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → P
Dvd.elim h: a ∣ b
h fun c: ?m.8988
c => fun H1: b = a * c
H1 : b: α
b = a: α
a * c: ?m.8988
c => Exists.intro: ∀ {α : Sort ?u.9361} {p : α → Prop} (w : α), p w → Exists p
Exists.intro c: ?m.8988
c (Eq.trans: ∀ {α : Sort ?u.9369} {a b c : α}, a = b → b = c → a = c
Eq.trans H1: b = a * c
H1 (mul_comm: ∀ {G : Type ?u.9374} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm a: α
a c: ?m.8988
c))
#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 * a
exists_eq_mul_left_of_dvd

theorem dvd_iff_exists_eq_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = c * a
dvd_iff_exists_eq_mul_left : a: α
a ∣ b: α
b ↔ ∃ c: ?m.9696
c, b: α
b = c: ?m.9696
c * a: α
a :=
  ⟨exists_eq_mul_left_of_dvd: ∀ {α : Type ?u.10035} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∃ c, b = c * a
exists_eq_mul_left_of_dvd, by
Goals accomplished! 🐙
    α: Type u_1

inst✝: 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 * a
rfl⟨c, rfl⟩: ∃ c, b = c * a
⟩α: Type u_1

inst✝: CommSemigroup α

a, c✝, c: α

introa ∣ c * a
    α: Type u_1

inst✝: 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 * a
mul_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 * a
dvd_iff_exists_eq_mul_left

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

@[simp]
theorem dvd_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * a
dvd_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 ∣ b
Dvd.intro b: α
b (mul_comm: ∀ {G : Type ?u.11667} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm a: α
a b: α
b)
#align dvd_mul_left dvd_mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] (a b : α), a ∣ b * a
dvd_mul_left

theorem dvd_mul_of_dvd_right: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
dvd_mul_of_dvd_right (h: a ∣ b
h : a: α
a ∣ b: α
b) (c: α
c : α: Type ?u.11862
α) : a: α
a ∣ c: α
c * b: α
b := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ c * brw [α: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ c * bmul_comm: ∀ {G : Type ?u.12386} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_commα: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ b * c]α: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ b * c;α: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ b * c α: Type u_1

inst✝: CommSemigroup α

a, b, c✝: α

h: a ∣ b

c: α

a ∣ c * bexact h: a ∣ b
h.mul_right: ∀ {α : Type ?u.12433} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * c
mul_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 * b
dvd_mul_of_dvd_right

alias dvd_mul_of_dvd_right: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
dvd_mul_of_dvd_right ← Dvd.dvd.mul_left: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
Dvd.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 * a
mul_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 * d
mul_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 = a
rfl⟩, ⟨f: α
f, rfl: ∀ {α : Sort ?u.13395} {a : α}, a = a
rfl⟩ => ⟨e: α
e * f: α
f, by
Goals accomplished! 🐙 α: Type u_1

inst✝: CommSemigroup α

a✝, b, c✝, a, c, e, f: α

a * e * (c * f) = a * c * (e * f)simp
Goals accomplished! 🐙⟩
#align mul_dvd_mul mul_dvd_mul: ∀ {α : Type u_1} [inst : CommSemigroup α] {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
mul_dvd_mul

theorem dvd_of_mul_left_dvd: a * b ∣ c → b ∣ c
dvd_of_mul_left_dvd (h: a * b ∣ c
h : 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) → P
Dvd.elim h: a * b ∣ c
h fun d: ?m.15378
d ceq: ?m.15381
ceq => Dvd.intro: ∀ {α : Type ?u.15383} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ b
Dvd.intro (a: α
a * d: ?m.15378
d) (by
Goals accomplished! 🐙 α: Type u_1

inst✝: CommSemigroup α

a, b, c: α

h: a * b ∣ c

d: α

ceq: c = a * b * d

b * (a * d) = csimp [ceq: c = a * b * d
ceq]
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 ∣ c
dvd_of_mul_left_dvd

end CommSemigroup

section CommMonoid

variable [CommMonoid: Type ?u.16958 → Type ?u.16958
CommMonoid α: 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 * c
mul_dvd_mul_left (a: α
a : α: Type ?u.16202
α) {b: α
b c: α
c : α: Type ?u.16202
α} (h: b ∣ c
h : 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 * d
mul_dvd_mul (dvd_refl: ∀ {α : Type ?u.16813} [inst : Monoid α] (a : α), a ∣ a
dvd_refl a: α
a) h: b ∣ c
h
#align mul_dvd_mul_left mul_dvd_mul_left: ∀ {α : Type u_1} [inst : CommMonoid α] (a : α) {b c : α}, b ∣ c → a * b ∣ a * c
mul_dvd_mul_left

theorem mul_dvd_mul_right: a ∣ b → ∀ (c : α), a * c ∣ b * c
mul_dvd_mul_right (h: a ∣ b
h : 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 * d
mul_dvd_mul h: a ∣ b
h (dvd_refl: ∀ {α : Type ?u.17570} [inst : Monoid α] (a : α), a ∣ a
dvd_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 * c
mul_dvd_mul_right

theorem pow_dvd_pow_of_dvd: ∀ {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ n
pow_dvd_pow_of_dvd {a: α
a b: α
b : α: Type ?u.17700
α} (h: a ∣ b
h : a: α
a ∣ b: α
b) : ∀ n: ℕ
n : ℕ: Type
ℕ, a: α
a ^ n: ℕ
n ∣ b: α
b ^ n: ℕ
n
  | 0: ℕ
0 => by
Goals accomplished! 🐙 α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

a ^ 0 ∣ b ^ 0rw [α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

a ^ 0 ∣ b ^ 0pow_zero: ∀ {M : Type ?u.23257} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zero,α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

1 ∣ b ^ 0 α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

a ^ 0 ∣ b ^ 0pow_zero: ∀ {M : Type ?u.23413} [inst : Monoid M] (a : M), a ^ 0 = 1
pow_zeroα: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

1 ∣ 1]
Goals accomplished! 🐙
  | n: ℕ
n + 1 => by
Goals accomplished! 🐙
    α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a ^ (n + 1) ∣ b ^ (n + 1)rw [α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a ^ (n + 1) ∣ b ^ (n + 1)pow_succ: ∀ {M : Type ?u.23459} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succ,α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a * a ^ n ∣ b ^ (n + 1) α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a ^ (n + 1) ∣ b ^ (n + 1)pow_succ: ∀ {M : Type ?u.23490} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a * a ^ n
pow_succα: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a * a ^ n ∣ b * b ^ n]α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

a * a ^ n ∣ b * b ^ n
    α: Type u_1

inst✝: CommMonoid α

a✝, b✝, a, b: α

h: a ∣ b

n: ℕ

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 * d
mul_dvd_mul h: a ∣ b
h (pow_dvd_pow_of_dvd: ∀ {a b : α}, a ∣ b → ∀ (n : ℕ), a ^ n ∣ b ^ n
pow_dvd_pow_of_dvd h: a ∣ b
h 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 ^ n
pow_dvd_pow_of_dvd

end CommMonoid