awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
rw : HMul.hMul (α := Associates M) (Associates.mk a) (Associates.mk 0) = Associates.mk 0
rw₁ : Eq (α := Associates M) (Associates.mk (a * 0)) (Associates.mk 0)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Associates M) (Associates.mk 0) (Associates.mk 0)
⊢ HMul.hMul (α := Associates M) (Associates.mk a) 0 = 0

Tactic:
rw [← mk_zero, mk_mul_mk, mul_zero]

Premises used: Associates.mk_zero, MulZeroClass.mul_zero, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
⊢ a ≤ 0

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : Associates M
hp : Prime p
a b : Associates M
h : p ≤ a * b
⊢ p ≤ a ∨ p ≤ b

Tactic:
hp.2.2 a b h

Premises used: And.right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
rw :
  (Ne (α := Associates M) (Associates.mk p) 0 ∧
      ¬IsUnit (M := Associates M) (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b →
            Dvd.dvd (α := Associates M) (Associates.mk p) (Associates.mk a) ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (M := Associates M) (Associates.mk p) ↔ Prime p

Tactic:
rw [Prime, _root_.Prime, forall_associated]

Premises used: Prime, Associates.forall_associated
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
⊢ (Ne (α := Associates M) (Associates.mk p) 0 ∧
      ¬IsUnit (M := Associates M) (Associates.mk p) ∧
        ∀ (a : M) (b : Associates M),
          Associates.mk p ∣ Associates.mk a * b →
            Dvd.dvd (α := Associates M) (Associates.mk p) (Associates.mk a) ∨ Associates.mk p ∣ b) ↔
    p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
simp only [forall_associated, mk_ne_zero, isUnit_mk, mk_mul_mk, mk_dvd_mk]

Premises used: Associates.forall_associated, Associates.mk_mul_mk, Associates.mk_ne_zero, Associates.isUnit_mk, Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
simp :
  (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ Irreducible (M := Associates M) (Associates.mk a) ↔ Irreducible a

Tactic:
simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]

Premises used: Associated.comm, Associates.mk_eq_mk_iff_associated, Associates.forall_associated, Associates.mk_mul_mk, irreducible_iff, Associates.isUnit_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
apply : (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b
⊢ (¬IsUnit a ∧ ∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔
    ¬IsUnit a ∧ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
apply Iff.rfl.and

Premises used: Iff.rfl, Iff.and
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
mp : (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) → ∀ ⦃a_2 b : M⦄, a = a_2 * b → IsUnit a_2 ∨ IsUnit b
mpr : (∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b) → ∀ (a_2 a_3 : M), a_2 * a_3 ~ᵤ a → IsUnit a_2 ∨ IsUnit a_3
⊢ (∀ (a_1 a_2 : M), a_1 * a_2 ~ᵤ a → IsUnit a_1 ∨ IsUnit a_2) ↔ ∀ ⦃a_1 b : M⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y

Tactic:
h _ _ <| .refl _

Premises used: Associated.refl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
x y : M
h : ∀ (a a_1 : M), a * a_1 ~ᵤ x * y → IsUnit a ∨ IsUnit a_1
⊢ IsUnit x ∨ IsUnit y

Tactic:
exact h _ _ <| .refl _
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
x y : M
u : Mˣ
h : ∀ ⦃a b : M⦄, x * y * (↑u : M) = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y

Tactic:
simpa using h (mul_assoc _ _ _)

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
simp : (a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ b = a * x
⊢ DvdNotUnit (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

Tactic:
simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := b)]

Premises used: Associated.comm, Associates.mk_eq_mk_iff_associated, Function.Surjective.exists, DvdNotUnit, Associates.mk_surjective, Associates.mk_mul_mk, Associates.mk_ne_zero, Associates.isUnit_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ b = a * x

Tactic:
Iff.rfl.and ?_

Premises used: Iff.rfl, Iff.and
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
refine : (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ (x : M), ¬IsUnit x ∧ b = a * x
⊢ (a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ b = a * x

Tactic:
refine Iff.rfl.and ?_

Premises used: Iff.rfl, Iff.and
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
mp : (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ (x : M), ¬IsUnit x ∧ b = a * x
mpr : (∃ (x : M), ¬IsUnit x ∧ b = a * x) → ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b
⊢ (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ (x : M), ¬IsUnit x ∧ b = a * x

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ∃ (x_1 : M), ¬IsUnit x_1 ∧ a * x * (↑u : M) = a * x_1

Tactic:
⟨x * u, ?_, mul_assoc ..⟩

Premises used: Units.val, HMul.hMul, mul_assoc, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
mp : ¬IsUnit (x * (↑u : M))
⊢ ∃ (x_1 : M), ¬IsUnit x_1 ∧ a * x * (↑u : M) = a * x_1

Tactic:
refine ⟨x * u, ?_, mul_assoc ..⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ¬IsUnit (x * (↑u : M))

Tactic:
simpa
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
w : M
h : ¬IsUnit x ∧ a * x ~ᵤ a * x
⊢ ∃ (x_1 : M), ¬IsUnit x_1 ∧ a * x_1 ~ᵤ a * x

Tactic:
use x
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : Associates M
hlt : a < b
left : a ≠ 0
right : ∃ (x : Associates M), ¬IsUnit x ∧ b = a * x
⊢ DvdNotUnit a b

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
apply : b ≤ 0
⊢ False

Tactic:
apply not_lt_of_ge _ hlt

Premises used: not_lt_of_ge
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ b ≤ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : Associates M
hlt : a < b
right : ∀ (x : Associates M) (ndvd : ¬a * x ∣ a), ∃ (x_1 : Associates M), ¬IsUnit x_1 ∧ a * x = a * x_1
⊢ ∃ (x : Associates M), ¬IsUnit x ∧ b = a * x

Tactic:
rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ∃ (x_1 : Associates M), ¬IsUnit x_1 ∧ a * x = a * x_1

Tactic:
⟨x, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
right : ¬IsUnit x
⊢ ∃ (x_1 : Associates M), ¬IsUnit x_1 ∧ a * x = a * x_1

Tactic:
refine ⟨x, ?_, rfl⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
right : ∀ (ndvd : IsUnit x), a * x ∣ a
⊢ ¬IsUnit x

Tactic:
contrapose ndvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
right : ∀ (u : (Associates M)ˣ), a * (↑u : Associates M) ∣ a
⊢ a * x ∣ a

Tactic:
rcases ndvd with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
u : (Associates M)ˣ
⊢ a * (↑u : Associates M) ∣ a

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
simp_rw :
  (∀ (a : M), Irreducible a ↔ Prime a) ↔
    ∀ (a : M), Irreducible (M := Associates M) (Associates.mk a) ↔ Prime (M := Associates M) (Associates.mk a)
simp_rw₁ : (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : M), Irreducible a ↔ Prime (M := Associates M) (Associates.mk a)
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a

Tactic:
simp_rw [forall_associated, irreducible_mk, prime_mk]

Premises used: Associates.irreducible_mk, Associates.forall_associated, Associates.prime_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a_1 : Associates M
a : M
ha : Ne (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a) 0
a₁ : Associates M
b : M
a₂ : Associates M
c : M
h :
  Eq.{u_1 + 1} (α := Associates M)
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b))
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c))
mk :
  ∀ (u : Mˣ) (hu : (fun (x1 x2 : M) ↦ x1 * x2) a b * (↑u : M) = (fun (x1 x2 : M) ↦ x1 * x2) a c),
    Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)
⊢ Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
    (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)

Tactic:
rcases Quotient.exact' h with ⟨u, hu⟩

Premises used: Quotient.exact'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a_1 : Associates M
a : M
ha : Ne (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a) 0
a₁ : Associates M
b : M
a₂ : Associates M
c : M
h :
  Eq.{u_1 + 1} (α := Associates M)
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b))
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c))
u : Mˣ
hu : (fun (x1 x2 : M) ↦ x1 * x2) a b * (↑u : M) = (fun (x1 x2 : M) ↦ x1 * x2) a c
rwa rwa₁ rwa₂ rwa₃ : a * b * (↑u : M) = a * c
⊢ a * (b * (↑u : M)) = a * c

Tactic:
rwa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a_1 : Associates M
a : M
ha : Ne (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a) 0
a₁ : Associates M
b : M
a₂ : Associates M
c : M
h :
  Eq.{u_1 + 1} (α := Associates M)
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b))
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c))
u : Mˣ
hu : (fun (x1 x2 : M) ↦ x1 * x2) a b * (↑u : M) = (fun (x1 x2 : M) ↦ x1 * x2) a c
⊢ a * (b * (↑u : M)) = a * c

Tactic:
have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a_1 : Associates M
a : M
ha : Ne (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a) 0
a₁ : Associates M
b : M
a₂ : Associates M
c : M
h :
  Eq.{u_1 + 1} (α := Associates M)
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b))
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c))
u : Mˣ
hu_1 : (fun (x1 x2 : M) ↦ x1 * x2) a b * (↑u : M) = (fun (x1 x2 : M) ↦ x1 * x2) a c
hu : a * (b * (↑u : M)) = a * c
⊢ Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
    (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)

Tactic:
Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩

Premises used: Quotient.sound', mul_left_cancel₀, Exists.intro, Iff.mp, Associates.mk_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a_1 : Associates M
a : M
ha : Ne (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a) 0
a₁ : Associates M
b : M
a₂ : Associates M
c : M
h :
  Eq.{u_1 + 1} (α := Associates M)
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b))
    ((fun (x : Associates M) ↦ Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a * x)
      (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c))
u : Mˣ
hu_1 : (fun (x1 x2 : M) ↦ x1 * x2) a b * (↑u : M) = (fun (x1 x2 : M) ↦ x1 * x2) a c
hu : a * (b * (↑u : M)) = a * c
⊢ Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
    (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)

Tactic:
exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : DecompositionMonoid M
p : Associates M
⊢ Irreducible p ↔ Prime p

Tactic:
irreducible_iff_prime

Premises used: irreducible_iff_prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
⊢ NoZeroDivisors.{u_1} (Associates M)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c : Associates M
ha : a ≠ 0
d : Associates M
hd : a * c = a * b * d
rwa rwa₁ rwa₂ rwa₃ : a * c = a * b * d
⊢ a * c = a * (b * d)

Tactic:
rwa [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
rcases :
  ∀ (p : M) (hp : Prime (M := Associates M) (Associates.mk p)) (hle : m ≤ Associates.mk p), m = 1 ∨ m = Associates.mk p
⊢ m = 1 ∨ m = p

Tactic:
rcases mk_surjective p with ⟨p, rfl⟩

Premises used: Associates.mk_surjective, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
m : Associates M
p : M
hp : Prime (M := Associates M) (Associates.mk p)
hle : m ≤ Associates.mk p
rcases :
  ∀ (m : M) (hle : LE.le (α := Associates M) (Associates.mk m) (Associates.mk p)),
    Eq (α := Associates M) (Associates.mk m) 1 ∨ Eq (α := Associates M) (Associates.mk m) (Associates.mk p)
⊢ m = 1 ∨ m = Associates.mk p

Tactic:
rcases mk_surjective m with ⟨m, rfl⟩

Premises used: Associates.mk_surjective, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime (M := Associates M) (Associates.mk p)
m : M
hle : LE.le (α := Associates M) (Associates.mk m) (Associates.mk p)
⊢ Eq (α := Associates M) (Associates.mk m) 1 ∨ Eq (α := Associates M) (Associates.mk m) (Associates.mk p)

Tactic:
simpa [mk_eq_mk_iff_associated, Associated.comm]
    using (prime_mk.1 hp).irreducible.dvd_iff.mp (mk_le_mk_iff_dvd.1 hle)

Premises used: Associated.comm, Prime.irreducible, Associates.mk_eq_mk_iff_associated, Associates.mk_le_mk_iff_dvd, Associates.prime_mk, Iff.mp, Irreducible.dvd_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b : Associates M
⊢ DvdNotUnit a b ↔ a < b

Tactic:
dvd_and_not_dvd_iff.symm

Premises used: dvd_and_not_dvd_iff, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
rw : p ≤ ⊥ ↔ p = ⊥
rw₁ rw₂ : p = ⊥ ↔ p = ⊥
⊢ p ≤ 1 ↔ p = 1

Tactic:
rw [← Associates.bot_eq_one, le_bot_iff]

Premises used: le_bot_iff, Associates.bot_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
obtain : ∀ (u : Mˣ) (h : DvdNotUnit p (r * (↑u : M))) (h' : r * (↑u : M) ~ᵤ r), DvdNotUnit p r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨u, rfl⟩ := Associated.symm h'

Premises used: Associated.symm, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p r : M
u : Mˣ
h : DvdNotUnit p (r * (↑u : M))
h' : r * (↑u : M) ~ᵤ r
obtain : ∀ (hp : p ≠ 0) (x : M) (hx : ¬IsUnit x ∧ r * (↑u : M) = p * x), DvdNotUnit p r
⊢ DvdNotUnit p r

Tactic:
obtain ⟨hp, x, hx⟩ := h
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p r : M
u : Mˣ
h' : r * (↑u : M) ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * (↑u : M) = p * x
⊢ DvdNotUnit p r

Tactic:
⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩

Premises used: HMul.hMul, Units.ne_zero, DvdNotUnit, Inv.inv, And.left, And.intro, Exists.intro, DvdNotUnit.not_unit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p r : M
u : Mˣ
h' : r * (↑u : M) ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * (↑u : M) = p * x
refine : r = p * (x * (↑u⁻¹ : M))
⊢ DvdNotUnit p r

Tactic:
refine ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p r : M
u : Mˣ
h' : r * (↑u : M) ~ᵤ r
hp : p ≠ 0
x : M
hx : ¬IsUnit x ∧ r * (↑u : M) = p * x
rw : r = p * x * (↑u⁻¹ : M)
rw₁ : r = r * (↑u : M) * (↑u⁻¹ : M)
rw₂ : r = r * ((↑u : M) * (↑u⁻¹ : M))
rw₃ : r = r * 1
rw₄ rw₅ : r = r
⊢ r = p * (x * (↑u⁻¹ : M))

Tactic:
rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]

Premises used: mul_assoc, Units.mul_inv, And.right, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
obtain : ∀ (a : Mˣ) (ha : p * b * (↑a : M) = p), IsUnit b
⊢ IsUnit b

Tactic:
obtain ⟨a, ha⟩ := h
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * (↑a : M) = p
⊢ IsUnit b

Tactic:
.of_mul_eq_one a ((mul_right_inj' hp).mp ?_)

Premises used: Units.val, IsUnit.of_mul_eq_one, Iff.mp, mul_right_inj'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * (↑a : M) = p
refine : p * (b * (↑a : M)) = p * 1
⊢ IsUnit b

Tactic:
refine .of_mul_eq_one a ((mul_right_inj' hp).mp ?_)
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * (↑a : M) = p
rwa : p * b * (↑a : M) = p * 1
rwa₁ rwa₂ rwa₃ rwa₄ : p * b * (↑a : M) = p
⊢ p * (b * (↑a : M)) = p * 1

Tactic:
rwa [← mul_assoc, mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
h : DvdNotUnit p (p * (↑a : M))
obtain : ∀ (hp : p ≠ 0) (x : M) (hx : ¬IsUnit x) (hx' : p * (↑a : M) = p * x), False
⊢ False

Tactic:
obtain ⟨hp, x, hx, hx'⟩ := h
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : p * (↑a : M) = p * x
⊢ ¬IsUnit (↑a : M)

Tactic:
rcases (mul_right_inj' hp).mp hx' with rfl

Premises used: Iff.mp, mul_right_inj', rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : p * (↑a : M) = p * x
hx₁ : ¬IsUnit (↑a : M)
⊢ p * (↑a : M) = p * (↑a : M)

Tactic:
rcases (mul_right_inj' hp).mp hx' with rfl

Premises used: Iff.mp, mul_right_inj', rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
hp : p ≠ 0
hx : ¬IsUnit (↑a : M)
hx' : p * (↑a : M) = p * (↑a : M)
⊢ False

Tactic:
hx a.isUnit

Premises used: Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
hp : p ≠ 0
hx : ¬IsUnit (↑a : M)
hx' : p * (↑a : M) = p * (↑a : M)
⊢ False

Tactic:
exact hx a.isUnit

Premises used: Units.isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
q : M
⊢ q ∣ HPow.hPow (β := ℕ) p 0 ↔ ∃ (i : ℕ), i ≤ 0 ∧ q ~ᵤ p ^ i

Tactic:
simp [← isUnit_iff_dvd_one, associated_one_iff_isUnit]

Premises used: associated_one_iff_isUnit, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
⊢ q ∣ p ^ (n + 1) ↔ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩

Premises used: _private.0.dvd_prime_pow.match_1, Dvd.dvd, Associated.dvd, pow_dvd_pow, HPow.hPow, HAdd.hAdd, Iff.intro, OfNat.ofNat, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
succ : ∀ (h : q ∣ p ^ (n + 1)), ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
⊢ q ∣ p ^ (n + 1) ↔ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
refine ⟨fun h => ?_, fun ⟨i, hi, hq⟩ => hq.dvd.trans (pow_dvd_pow p hi)⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p ^ (n + 1)
⊢ q ∣ p * p ^ n

Tactic:
rw [pow_succ'] at h

Premises used: pow_succ'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
hp : Prime p
n : ℕ
ih : ∀ {q : M}, q ∣ p ^ n ↔ ∃ (i : ℕ), i ≤ n ∧ q ~ᵤ p ^ i
q : M
h : q ∣ p * p ^ n
succ : ∀ (q : M) (h : p * q ∣ p * p ^ n), ∃ (i : ℕ), i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
succ₁ : ∀ (hno : q ∣ p ^ n), ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i

Tactic:
rcases hp.left_dvd_or_dvd_right_of_dvd_mul h with (⟨q, rfl⟩ | hno)

Premises used: Prime.left_dvd_or_dvd_right_of_dvd_mul, rfl