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

! This file was ported from Lean 3 source module algebra.group_with_zero.divisibility
! 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.GroupWithZero.Basic
import Mathlib.Algebra.Divisibility.Units

/-!
# Divisibility in groups with zero.

Lemmas about divisibility in groups and monoids with zero.

-/

variable {α: Type ?u.4176α : Type _: Type (?u.1627+1)Type _}

section SemigroupWithZero

variable [SemigroupWithZero: Type ?u.16 → Type ?u.16SemigroupWithZero α: Type ?u.5α] {a: αa : α: Type ?u.268α}

theorem eq_zero_of_zero_dvd: 0 ∣ a → a = 0eq_zero_of_zero_dvd (h: 0 ∣ ah : 0: ?m.280 ∣ a: αa) : a: αa = 0: ?m.600 :=
Dvd.elim: ∀ {α : Type ?u.146} [inst : Semigroup α] {P : Prop} {a b : α}, a ∣ b → (∀ (c : α), b = a * c → P) → PDvd.elim h: 0 ∣ ah fun c: ?m.171c H': ?m.174H' => H': ?m.174H'.trans: ∀ {α : Sort ?u.176} {a b c : α}, a = b → b = c → a = ctrans (zero_mul: ∀ {M₀ : Type ?u.190} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0zero_mul c: ?m.171c)
#align eq_zero_of_zero_dvd eq_zero_of_zero_dvd: ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a → a = 0eq_zero_of_zero_dvd

/-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
product with zero equals `a` iff `a` equals zero. -/
@[simp]
theorem zero_dvd_iff: 0 ∣ a ↔ a = 0zero_dvd_iff : 0: ?m.2800 ∣ a: αa ↔ a: αa = 0: ?m.3100 :=
⟨eq_zero_of_zero_dvd: ∀ {α : Type ?u.403} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a → a = 0eq_zero_of_zero_dvd, fun h: ?m.434h => byGoals accomplished! 🐙
α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ arw [α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ ah: a = 0hα: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ 0]α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ 0
α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ aexact ⟨0: ?m.6380, α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 ∣ 0byGoals accomplished! 🐙 α: Type u_1inst✝: SemigroupWithZero αa: αh: a = 00 = 0 * 0simpGoals accomplished! 🐙⟩Goals accomplished! 🐙⟩
#align zero_dvd_iff zero_dvd_iff: ∀ {α : Type u_1} [inst : SemigroupWithZero α] {a : α}, 0 ∣ a ↔ a = 0zero_dvd_iff

@[simp]
theorem dvd_zero: ∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), a ∣ 0dvd_zero (a: αa : α: Type ?u.832α) : a: αa ∣ 0: ?m.8490 :=
Dvd.intro: ∀ {α : Type ?u.941} [inst : Semigroup α] {a b : α} (c : α), a * c = b → a ∣ bDvd.intro 0: ?m.9650 (byGoals accomplished! 🐙 α: Type u_1inst✝: SemigroupWithZero αa✝, a: αa * 0 = 0simpGoals accomplished! 🐙)
#align dvd_zero dvd_zero: ∀ {α : Type u_1} [inst : SemigroupWithZero α] (a : α), a ∣ 0dvd_zero

end SemigroupWithZero

/-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
`a*b` divides `a*c` iff `b` divides `c`. -/
theorem mul_dvd_mul_iff_left: ∀ [inst : CancelMonoidWithZero α] {a b c : α}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)mul_dvd_mul_iff_left [CancelMonoidWithZero: Type ?u.1186 → Type ?u.1186CancelMonoidWithZero α: Type ?u.1183α] {a: αa b: αb c: αc : α: Type ?u.1183α} (ha: a ≠ 0ha : a: αa ≠ 0: ?m.11980) :
a: αa * b: αb ∣ a: αa * c: αc ↔ b: αb ∣ c: αc :=
exists_congr: ∀ {α : Sort ?u.1464} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)exists_congr fun d: ?m.1480d => byGoals accomplished! 🐙 α: Type u_1inst✝: CancelMonoidWithZero αa, b, c: αha: a ≠ 0d: αa * c = a * b * d ↔ c = b * drw [α: Type u_1inst✝: CancelMonoidWithZero αa, b, c: αha: a ≠ 0d: αa * c = a * b * d ↔ c = b * dmul_assoc: ∀ {G : Type ?u.1487} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type u_1inst✝: CancelMonoidWithZero αa, b, c: αha: a ≠ 0d: αa * c = a * (b * d) ↔ c = b * d α: Type u_1inst✝: CancelMonoidWithZero αa, b, c: αha: a ≠ 0d: αa * c = a * b * d ↔ c = b * dmul_right_inj': ∀ {M₀ : Type ?u.1582} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, a ≠ 0 → (a * b = a * c ↔ b = c)mul_right_inj' ha: a ≠ 0haα: Type u_1inst✝: CancelMonoidWithZero αa, b, c: αha: a ≠ 0d: αc = b * d ↔ c = b * d]Goals accomplished! 🐙
#align mul_dvd_mul_iff_left mul_dvd_mul_iff_left: ∀ {α : Type u_1} [inst : CancelMonoidWithZero α] {a b c : α}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)mul_dvd_mul_iff_left

/-- Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero
element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
theorem mul_dvd_mul_iff_right: ∀ [inst : CancelCommMonoidWithZero α] {a b c : α}, c ≠ 0 → (a * c ∣ b * c ↔ a ∣ b)mul_dvd_mul_iff_right [CancelCommMonoidWithZero: Type ?u.1630 → Type ?u.1630CancelCommMonoidWithZero α: Type ?u.1627α] {a: αa b: αb c: αc : α: Type ?u.1627α} (hc: c ≠ 0hc : c: αc ≠ 0: ?m.16420) :
a: αa * c: αc ∣ b: αb * c: αc ↔ a: αa ∣ b: αb :=
exists_congr: ∀ {α : Sort ?u.1876} {p q : α → Prop}, (∀ (a : α), p a ↔ q a) → ((∃ a, p a) ↔ ∃ a, q a)exists_congr fun d: ?m.1892d => byGoals accomplished! 🐙 α: Type u_1inst✝: CancelCommMonoidWithZero αa, b, c: αhc: c ≠ 0d: αb * c = a * c * d ↔ b = a * drw [α: Type u_1inst✝: CancelCommMonoidWithZero αa, b, c: αhc: c ≠ 0d: αb * c = a * c * d ↔ b = a * dmul_right_comm: ∀ {G : Type ?u.1899} [inst : CommSemigroup G] (a b c : G), a * b * c = a * c * bmul_right_comm,α: Type u_1inst✝: CancelCommMonoidWithZero αa, b, c: αhc: c ≠ 0d: αb * c = a * d * c ↔ b = a * d α: Type u_1inst✝: CancelCommMonoidWithZero αa, b, c: αhc: c ≠ 0d: αb * c = a * c * d ↔ b = a * dmul_left_inj': ∀ {M₀ : Type ?u.1967} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, c ≠ 0 → (a * c = b * c ↔ a = b)mul_left_inj' hc: c ≠ 0hcα: Type u_1inst✝: CancelCommMonoidWithZero αa, b, c: αhc: c ≠ 0d: αb = a * d ↔ b = a * d]Goals accomplished! 🐙
#align mul_dvd_mul_iff_right mul_dvd_mul_iff_right: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {a b c : α}, c ≠ 0 → (a * c ∣ b * c ↔ a ∣ b)mul_dvd_mul_iff_right

section CommMonoidWithZero

variable [CommMonoidWithZero: Type ?u.2239 → Type ?u.2239CommMonoidWithZero α: Type ?u.2015α]

/-- `DvdNotUnit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a`
is not a unit. -/
def DvdNotUnit: α → α → PropDvdNotUnit (a: αa b: αb : α: Type ?u.2021α) : Prop: TypeProp :=
a: αa ≠ 0: ?m.20370 ∧ ∃ x: ?m.2071x, ¬IsUnit: {M : Type ?u.2073} → [inst : Monoid M] → M → PropIsUnit x: ?m.2071x ∧ b: αb = a: αa * x: ?m.2071x
#align dvd_not_unit DvdNotUnit: {α : Type u_1} → [inst : CommMonoidWithZero α] → α → α → PropDvdNotUnit

theorem dvdNotUnit_of_dvd_of_not_dvd: ∀ {a b : α}, a ∣ b → ¬b ∣ a → DvdNotUnit a bdvdNotUnit_of_dvd_of_not_dvd {a: αa b: αb : α: Type ?u.2236α} (hd: a ∣ bhd : a: αa ∣ b: αb) (hnd: ¬b ∣ ahnd : ¬b: αb ∣ a: αa) : DvdNotUnit: {α : Type ?u.2298} → [inst : CommMonoidWithZero α] → α → α → PropDvdNotUnit a: αa b: αb := byGoals accomplished! 🐙
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aDvdNotUnit a bconstructorα: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ alefta ≠ 0α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * x
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aDvdNotUnit a b·α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ alefta ≠ 0 α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ alefta ≠ 0α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * xrintro rfl: a = 0rflα: Type u_1inst✝: CommMonoidWithZero αb: αhd: 0 ∣ bhnd: ¬b ∣ 0leftFalse
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ alefta ≠ 0exact hnd: ¬b ∣ 0hnd (dvd_zero: ∀ {α : Type ?u.2349} [inst : SemigroupWithZero α] (a : α), a ∣ 0dvd_zero _: ?m.2350_)Goals accomplished! 🐙
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aDvdNotUnit a b·α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * x α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * xrcases hd: a ∣ bhd with ⟨c, rfl⟩: a ∣ b⟨c: αc⟨c, rfl⟩: a ∣ b, rfl: b = a * crfl⟨c, rfl⟩: a ∣ b⟩α: Type u_1inst✝: CommMonoidWithZero αa, c: αhnd: ¬a * c ∣ aright.intro∃ x, ¬IsUnit x ∧ a * c = a * x
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * xrefine' ⟨c: αc, _: ?m.2453_, rfl: ∀ {α : Sort ?u.2456} {a : α}, a = arfl⟩α: Type u_1inst✝: CommMonoidWithZero αa, c: αhnd: ¬a * c ∣ aright.intro¬IsUnit c
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * xrintro ⟨u, rfl⟩: IsUnit c⟨u: αˣu⟨u, rfl⟩: IsUnit c, rfl: ↑u = crfl⟨u, rfl⟩: IsUnit c⟩α: Type u_1inst✝: CommMonoidWithZero αa: αu: αˣhnd: ¬a * ↑u ∣ aright.intro.introFalse
α: Type u_1inst✝: CommMonoidWithZero αa, b: αhd: a ∣ bhnd: ¬b ∣ aright∃ x, ¬IsUnit x ∧ b = a * xsimp at hnd: ¬a * ↑u ∣ ahndGoals accomplished! 🐙
#align dvd_not_unit_of_dvd_of_not_dvd dvdNotUnit_of_dvd_of_not_dvd: ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {a b : α}, a ∣ b → ¬b ∣ a → DvdNotUnit a bdvdNotUnit_of_dvd_of_not_dvd

end CommMonoidWithZero

theorem dvd_and_not_dvd_iff: ∀ [inst : CancelCommMonoidWithZero α] {x y : α}, x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x ydvd_and_not_dvd_iff [CancelCommMonoidWithZero: Type ?u.2786 → Type ?u.2786CancelCommMonoidWithZero α: Type ?u.2783α] {x: αx y: αy : α: Type ?u.2783α} :
x: αx ∣ y: αy ∧ ¬y: αy ∣ x: αx ↔ DvdNotUnit: {α : Type ?u.2844} → [inst : CommMonoidWithZero α] → α → α → PropDvdNotUnit x: αx y: αy :=
⟨fun ⟨⟨d: αd, hd: y = x * dhd⟩, hyx: ¬y ∣ xhyx⟩ =>
⟨fun hx0: ?m.2918hx0 => byGoals accomplished! 🐙 α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xhx0: x = 0Falsesimp [hx0: x = 0hx0] at hyx: ¬y ∣ xhyxGoals accomplished! 🐙,
⟨d: αd, mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬amt isUnit_iff_dvd_one: ∀ {α : Type ?u.2942} [inst : CommMonoid α] {x : α}, IsUnit x ↔ x ∣ 1isUnit_iff_dvd_one.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 fun ⟨e: αe, he: 1 = d * ehe⟩ => hyx: ¬y ∣ xhyx ⟨e: αe, byGoals accomplished! 🐙 α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = y * erw [α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = y * ehd: y = x * dhd,α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = x * d * e α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = y * emul_assoc: ∀ {G : Type ?u.3868} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = x * (d * e) α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = y * e← he: 1 = d * ehe,α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = x * 1 α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = y * emul_one: ∀ {M : Type ?u.3941} [inst : MulOneClass M] (a : M), a * 1 = amul_oneα: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: x ∣ y ∧ ¬y ∣ xd: αhd: y = x * dhyx: ¬y ∣ xx✝: d ∣ 1e: αhe: 1 = d * ex = x]Goals accomplished! 🐙⟩,
hd: y = x * dhd⟩⟩,
fun ⟨hx0: x ≠ 0hx0, d: αd, hdu: ¬IsUnit dhdu, hdx: y = x * dhdx⟩ =>
⟨⟨d: αd, hdx: y = x * dhdx⟩, fun ⟨e: αe, he: x = y * ehe⟩ =>
hdu: ¬IsUnit dhdu
(isUnit_of_dvd_one: ∀ {α : Type ?u.3308} [inst : CommMonoid α] {a : α}, a ∣ 1 → IsUnit aisUnit_of_dvd_one
⟨e: αe, mul_left_cancel₀: ∀ {M₀ : Type ?u.3352} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsLeftCancelMulZero M₀] {a b c : M₀},
a ≠ 0 → a * b = a * c → b = cmul_left_cancel₀ hx0: x ≠ 0hx0 <| byGoals accomplished! 🐙 α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1 = x * (d * e)conv =>α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * (d * e)
α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1 = x * (d * e)lhsα: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1
α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1 = x * (d * e)rw [α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1he: x = y * ehe,α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ey * e * 1 α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1hdx: y = x * dhdxα: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * d * e * 1]α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * d * e * 1
α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * 1 = x * (d * e)simp [mul_assoc: ∀ {G : Type ?u.4039} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]α: Type u_1inst✝: CancelCommMonoidWithZero αx, y: αx✝¹: DvdNotUnit x yhx0: x ≠ 0d: αhdu: ¬IsUnit dhdx: y = x * dx✝: y ∣ xe: αhe: x = y * ex * (d * e)⟩)⟩⟩
#align dvd_and_not_dvd_iff dvd_and_not_dvd_iff: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] {x y : α}, x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x ydvd_and_not_dvd_iff

section MonoidWithZero

variable [MonoidWithZero: Type ?u.4185 → Type ?u.4185MonoidWithZero α: Type ?u.4176α]

theorem ne_zero_of_dvd_ne_zero: ∀ {p q : α}, q ≠ 0 → p ∣ q → p ≠ 0ne_zero_of_dvd_ne_zero {p: αp q: αq : α: Type ?u.4182α} (h₁: q ≠ 0h₁ : q: αq ≠ 0: ?m.41950) (h₂: p ∣ qh₂ : p: αp ∣ q: αq) : p: αp ≠ 0: ?m.42730 := byGoals accomplished! 🐙
α: Type u_1inst✝: MonoidWithZero αp, q: αh₁: q ≠ 0h₂: p ∣ qp ≠ 0rcases h₂: p ∣ qh₂ with ⟨u, rfl⟩: p ∣ q⟨u: αu⟨u, rfl⟩: p ∣ q, rfl: q = p * urfl⟨u, rfl⟩: p ∣ q⟩α: Type u_1inst✝: MonoidWithZero αp, u: αh₁: p * u ≠ 0introp ≠ 0
α: Type u_1inst✝: MonoidWithZero αp, q: αh₁: q ≠ 0h₂: p ∣ qp ≠ 0exact left_ne_zero_of_mul: ∀ {M₀ : Type ?u.4323} [inst : MulZeroClass M₀] {a b : M₀}, a * b ≠ 0 → a ≠ 0left_ne_zero_of_mul h₁: p * u ≠ 0h₁Goals accomplished! 🐙
#align ne_zero_of_dvd_ne_zero ne_zero_of_dvd_ne_zero: ∀ {α : Type u_1} [inst : MonoidWithZero α] {p q : α}, q ≠ 0 → p ∣ q → p ≠ 0ne_zero_of_dvd_ne_zero

end MonoidWithZero

section CancelCommMonoidWithZero

variable [CancelCommMonoidWithZero: Type ?u.5525 → Type ?u.5525CancelCommMonoidWithZero α: Type ?u.5101α] [Subsingleton: Sort ?u.5107 → PropSubsingleton α: Type ?u.5101αˣ] {a: αa b: αb : α: Type ?u.4387α}

theorem dvd_antisymm: a ∣ b → b ∣ a → a = bdvd_antisymm : a: αa ∣ b: αb → b: αb ∣ a: αa → a: αa = b: αb := byGoals accomplished! 🐙
α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, b: αa ∣ b → b ∣ a → a = brintro ⟨c, rfl⟩: a ∣ b⟨c: αc⟨c, rfl⟩: a ∣ b, rfl: b = a * crfl⟨c, rfl⟩: a ∣ b⟩ ⟨d, hcd⟩: a * c ∣ a⟨d: αd⟨d, hcd⟩: a * c ∣ a, hcd: a = a * c * dhcd⟨d, hcd⟩: a * c ∣ a⟩α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * c * dintro.introa = a * c
α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, b: αa ∣ b → b ∣ a → a = brw [α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * c * dintro.introa = a * cmul_assoc: ∀ {G : Type ?u.4611} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * (c * d)intro.introa = a * c α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * c * dintro.introa = a * ceq_comm: ∀ {α : Sort ?u.4700} {a b : α}, a = b ↔ b = aeq_comm,α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a * (c * d) = aintro.introa = a * c α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * c * dintro.introa = a * cmul_right_eq_self₀: ∀ {M₀ : Type ?u.4720} [inst : CancelMonoidWithZero M₀] {a b : M₀}, a * b = a ↔ b = 1 ∨ a = 0mul_right_eq_self₀,α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c * d = 1 ∨ a = 0intro.introa = a * c α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: a = a * c * dintro.introa = a * cmul_eq_one: ∀ {α : Type ?u.4763} [inst : CommMonoid α] [inst_1 : Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1mul_eq_oneα: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c = 1 ∧ d = 1 ∨ a = 0intro.introa = a * c]α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c = 1 ∧ d = 1 ∨ a = 0intro.introa = a * c at hcd: a = a * c * dhcdα: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c = 1 ∧ d = 1 ∨ a = 0intro.introa = a * c
α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, b: αa ∣ b → b ∣ a → a = bobtain ⟨rfl, -⟩: c = 1 ∧ d = 1⟨rfl: c = 1rfl⟨rfl, -⟩: c = 1 ∧ d = 1, -: d = 1-⟨rfl, -⟩: c = 1 ∧ d = 1⟩⟨rfl, -⟩ | rfl: c = 1 ∧ d = 1 ∨ a = 0 | rfl: a = 0rfl := hcd: c = 1 ∧ d = 1 ∨ a = 0hcdα: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, d: αintro.intro.inl.introa = a * 1α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣc, d: αintro.intro.inr0 = 0 * c α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c = 1 ∧ d = 1 ∨ a = 0intro.introa = a * c<;>α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, d: αintro.intro.inl.introa = a * 1α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣc, d: αintro.intro.inr0 = 0 * c α: Type u_1inst✝¹: CancelCommMonoidWithZero αinst✝: Subsingleton αˣa, c, d: αhcd: c = 1 ∧ d = 1 ∨ a = 0intro.introa = a * csimpGoals accomplished! 🐙
#align dvd_antisymm dvd_antisymm: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bdvd_antisymm

-- porting note: `attribute [protected]` is currently unsupported
-- attribute [protected] Nat.dvd_antisymm --This lemma is in core, so we protect it here

theorem dvd_antisymm': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = advd_antisymm' : a: αa ∣ b: αb → b: αb ∣ a: αa → b: αb = a: αa :=
flip: ∀ {α : Sort ?u.5217} {β : Sort ?u.5216} {φ : Sort ?u.5215}, (α → β → φ) → β → α → φflip dvd_antisymm: ∀ {α : Type ?u.5225} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bdvd_antisymm
#align dvd_antisymm' dvd_antisymm': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = advd_antisymm'

alias dvd_antisymm: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bdvd_antisymm ← Dvd.dvd.antisymm: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bDvd.dvd.antisymm
#align has_dvd.dvd.antisymm Dvd.dvd.antisymm: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bDvd.dvd.antisymm

alias dvd_antisymm': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = advd_antisymm' ← Dvd.dvd.antisymm': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = aDvd.dvd.antisymm'
#align has_dvd.dvd.antisymm' Dvd.dvd.antisymm': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → b = aDvd.dvd.antisymm'

theorem eq_of_forall_dvd: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α},
(∀ (c : α), a ∣ c ↔ b ∣ c) → a = beq_of_forall_dvd (h: ∀ (c : α), a ∣ c ↔ b ∣ ch : ∀ c: ?m.5335c, a: αa ∣ c: ?m.5335c ↔ b: αb ∣ c: ?m.5335c) : a: αa = b: αb :=
((h: ∀ (c : α), a ∣ c ↔ b ∣ ch _: α_).2: ∀ {a b : Prop}, (a ↔ b) → b → a2 dvd_rfl: ∀ {α : Type ?u.5400} [inst : Monoid α] {a : α}, a ∣ advd_rfl).antisymm: ∀ {α : Type ?u.5466} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bantisymm <| (h: ∀ (c : α), a ∣ c ↔ b ∣ ch _: α_).1: ∀ {a b : Prop}, (a ↔ b) → a → b1 dvd_rfl: ∀ {α : Type ?u.5496} [inst : Monoid α] {a : α}, a ∣ advd_rfl
#align eq_of_forall_dvd eq_of_forall_dvd: ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α},
(∀ (c : α), a ∣ c ↔ b ∣ c) → a = beq_of_forall_dvd

theorem eq_of_forall_dvd': (∀ (c : α), c ∣ a ↔ c ∣ b) → a = beq_of_forall_dvd' (h: ∀ (c : α), c ∣ a ↔ c ∣ bh : ∀ c: ?m.5573c, c: ?m.5573c ∣ a: αa ↔ c: ?m.5573c ∣ b: αb) : a: αa = b: αb :=
((h: ∀ (c : α), c ∣ a ↔ c ∣ bh _: α_).1: ∀ {a b : Prop}, (a ↔ b) → a → b1 dvd_rfl: ∀ {α : Type ?u.5638} [inst : Monoid α] {a : α}, a ∣ advd_rfl).antisymm: ∀ {α : Type ?u.5704} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α}, a ∣ b → b ∣ a → a = bantisymm <| (h: ∀ (c : α), c ∣ a ↔ c ∣ bh _: α_).2: ∀ {a b : Prop}, (a ↔ b) → b → a2 dvd_rfl: ∀ {α : Type ?u.5734} [inst : Monoid α] {a : α}, a ∣ advd_rfl
#align eq_of_forall_dvd' eq_of_forall_dvd': ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [inst_1 : Subsingleton αˣ] {a b : α},
(∀ (c : α), c ∣ a ↔ c ∣ b) → a = beq_of_forall_dvd'

end CancelCommMonoidWithZero
```