awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ = p₂ ^ k₂
rw : ∀ (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂), p₁ ~ᵤ p₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
apply h.of_pow_associated_of_prime hp₁ hp₂ hk₁

Premises used: Associated.of_pow_associated_of_prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
rw : ∀ (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂), p₁ ~ᵤ p₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : Subsingleton.{u_2 + 1} Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂

Tactic:
apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

Premises used: Associated.of_pow_associated_of_prime'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
⊢ Eq (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ a ~ᵤ b

Tactic:
Iff.intro Quotient.exact Quot.sound

Premises used: Quot.sound, Iff.intro, Quotient.exact
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ ⟦a⟧ = Associates.mk a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ Eq (α := Quot (α := M) (⇑(Associated.setoid M) : M → M → Prop)) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) a)
    (Associates.mk a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : Associates M
rw : Quot.mk (⇑(Associated.setoid M) : M → M → Prop) (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) a) = a
rw₁ rw₂ : a = a
⊢ Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) a) = a

Tactic:
rw [← quot_mk_eq_mk, Quot.out_eq]

Premises used: Quot.out_eq, Associates.quot_mk_eq_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : M
rw :
  Eq (α := Associates M) (Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) (Associates.mk a)))
    (Associates.mk a)
rw₁ rw₂ : Eq (α := Associates M) (Associates.mk a) (Associates.mk a)
⊢ Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) (Associates.mk a) ~ᵤ a

Tactic:
rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]

Premises used: Associates.mk_eq_mk_iff_associated, Associates.quot_out
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p : Associates M → Prop
⊢ (∀ (a : Associates M), p a) ↔ ∀ (a : M), p (Associates.mk a)

Tactic:
Iff.intro (fun h _ => h _) fun h a => Quotient.inductionOn a h

Premises used: Associates.mk, Quotient.inductionOn, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := M) (β := Associates M) Associates.mk

Tactic:
forall_associated.2 fun a => ⟨a, rfl⟩

Premises used: Iff.mpr, Associates.forall_associated, Exists.intro, Function.Surjective, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Associates M) (Associates.mk 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Associates M) 1 (Associates.mk 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : M
rw : Eq (α := Associates M) (Associates.mk a) (Associates.mk 1) ↔ IsUnit a
rw₁ : a ~ᵤ 1 ↔ IsUnit a
rw₂ rw₃ : IsUnit a ↔ IsUnit a
⊢ Eq (α := Associates M) (Associates.mk a) 1 ↔ IsUnit a

Tactic:
rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]

Premises used: Associates.mk_eq_mk_iff_associated, associated_one_iff_isUnit, Associates.mk_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
⊢ Eq.{u_1 + 1} (α := Associates M) ⊥ 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a : Associates M
⊢ ∃ (a0 : M), Associates.mk a0 = a

Tactic:
Quot.exists_rep a

Premises used: Quot.exists_rep, Quotient
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := M) (β := Associates M) Associates.mk

Tactic:
fun _ _ h => associated_iff_eq.mp (Associates.mk_eq_mk_iff_associated.mp h)

Premises used: Associates.mk_eq_mk_iff_associated, associated_iff_eq, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
x y : M
⊢ HMul.hMul (α := Associates M) (Associates.mk x) (Associates.mk y) = Associates.mk (x * y)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a' b' c' : Associates M
a b c : M
rw rw₁ : ⟦a * (b * c)⟧ = ⟦a * (b * c)⟧
⊢ ⟦a * b * c⟧ = ⟦a * (b * c)⟧

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a' : Associates M
a : M
⊢ ⟦1 * a⟧ = ⟦a⟧

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a' : Associates M
a : M
⊢ ⟦a * 1⟧ = ⟦a⟧

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a' b' : Associates M
a b : M
rw rw₁ : ⟦b * a⟧ = ⟦b * a⟧
⊢ ⟦a * b⟧ = ⟦b * a⟧

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ Eq (α := Associates M) ((Associates.mkMonoidHom : (a : M) → Associates M) a : Associates M)
    (Associates.mk a : Associates M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
f : Associates M →* M
hinv : Function.RightInverse (α := M) (β := Associates M) (⇑f : (a : Associates M) → M) Associates.mk
a : M
⊢ a ~ᵤ (f : (a : Associates M) → M) (Associates.mk a)

Tactic:
Associates.mk_eq_mk_iff_associated.1 (hinv (Associates.mk a)).symm

Premises used: Associates.mk, Associates.mk_eq_mk_iff_associated, Iff.mp, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
n : ℕ
zero : Associates.mk (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := Associates M) (β := ℕ) (Associates.mk a) 0
succ :
  ∀ (n : ℕ),
    Associates.mk (a ^ n) = HPow.hPow (α := Associates M) (Associates.mk a) n →
      Associates.mk (a ^ (n + 1)) = HPow.hPow (α := Associates M) (Associates.mk a) (n + 1)
⊢ Associates.mk (a ^ n) = HPow.hPow (α := Associates M) (Associates.mk a) n

Tactic:
induction n
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ Associates.mk (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := Associates M) (β := ℕ) (Associates.mk a) 0

Tactic:
simp [*, pow_succ, Associates.mk_mul_mk.symm]

Premises used: pow_succ, Associates.mk_mul_mk, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
n : ℕ
h : Associates.mk (a ^ n) = HPow.hPow (α := Associates M) (Associates.mk a) n
⊢ Associates.mk (a ^ (n + 1)) = HPow.hPow (α := Associates M) (Associates.mk a) (n + 1)

Tactic:
simp [*, pow_succ, Associates.mk_mul_mk.symm]

Premises used: pow_succ, Associates.mk_mul_mk, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq.{u_1 + 1} (α := Associates M → Associates M → Prop) (fun (x1 x2 : Associates M) ↦ x1 ∣ x2)
    fun (x1 x2 : Associates M) ↦ x1 ≤ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
hab : a * b = 1
hba : b * a = 1
h :
  ∀ (a b : M) (hab : ⟦a⟧ * ⟦b⟧ = 1) (hba : ⟦b⟧ * ⟦a⟧ = 1),
    { val := ⟦a⟧, inv := ⟦b⟧, val_inv := hab, inv_val := hba : (Associates M)ˣ } = default
⊢ { val := a, inv := b, val_inv := hab, inv_val := hba : (Associates M)ˣ } = default

Tactic:
induction a, b using Quotient.inductionOn₂ with | _ a b
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
hab : ⟦a⟧ * ⟦b⟧ = 1
hba : ⟦b⟧ * ⟦a⟧ = 1
⊢ { val := ⟦a⟧, inv := ⟦b⟧, val_inv := hab, inv_val := hba : (Associates M)ˣ } = default

Tactic:
Units.ext <| Quotient.sound <| associated_one_of_associated_mul_one <| Quotient.exact hab

Premises used: associated_one_of_associated_mul_one, Units.ext, Quotient.exact, Quotient.sound
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
hab : ⟦a⟧ * ⟦b⟧ = 1
hba : ⟦b⟧ * ⟦a⟧ = 1
⊢ { val := ⟦a⟧, inv := ⟦b⟧, val_inv := hab, inv_val := hba : (Associates M)ˣ } = default

Tactic:
exact Units.ext <| Quotient.sound <| associated_one_of_associated_mul_one <| Quotient.exact hab

Premises used: associated_one_of_associated_mul_one, Units.ext, Quotient.exact, Quotient.sound
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
u : (Associates M)ˣ
⊢ (↑u : Associates M) = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = 1

Tactic:
Iff.intro (fun ⟨_, h⟩ => h ▸ coe_unit_eq_one _) fun h => h.symm ▸ isUnit_one

Premises used: Eq.rec, Associates.coe_unit_eq_one, isUnit_one, Iff.intro, _private.0.Associates.isUnit_iff_eq_one.match_1, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : Associates M
rw : a = 1 ↔ a = ⊥
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ IsUnit a ↔ a = ⊥

Tactic:
rw [Associates.isUnit_iff_eq_one, bot_eq_one]

Premises used: Associates.bot_eq_one, Associates.isUnit_iff_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
rw : Eq (α := Associates M) (Associates.mk a) 1 ↔ a ~ᵤ 1
rw₁ : Eq (α := Associates M) (Associates.mk a) (Associates.mk 1) ↔ a ~ᵤ 1
rw₂ rw₃ : a ~ᵤ 1 ↔ a ~ᵤ 1
⊢ IsUnit (M := Associates M) (Associates.mk a) ↔ a ~ᵤ 1

Tactic:
rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]

Premises used: Associates.mk_eq_mk_iff_associated, Associates.one_eq_mk_one, Associates.isUnit_iff_eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b c d : Associates M
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates M
hx : b = a * x
y : Associates M
hy : d = c * y
⊢ b * d = a * c * (x * y)

Tactic:
simp [hx, hy, mul_comm, mul_left_comm]

Premises used: mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : Associates M
⊢ 1 ≤ a

Tactic:
one_le

Premises used: one_le
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
⟨b, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
rw : a ≤ a * b
⊢ a ≤ b * a

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
le_mul_right

Premises used: Associates.le_mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
exact le_mul_right

Premises used: Associates.le_mul_right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
simp : (∃ (x : M), a * x ~ᵤ b) ↔ ∃ (c : M), b = a * c
⊢ Dvd.dvd (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ a ∣ b

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

Premises used: Associated.comm, Associates.mk_eq_mk_iff_associated, dvd_def, Function.Surjective.exists, Associates.mk_surjective, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
mp : (∃ (x : M), a * x ~ᵤ b) → ∃ (c : M), b = a * c
mpr : (∃ (c : M), b = a * c) → ∃ (x : M), a * x ~ᵤ b
⊢ (∃ (x : M), a * x ~ᵤ b) ↔ ∃ (c : M), b = a * c

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a x : M
u : Mˣ
⊢ ∃ (c : M), a * x * (↑u : M) = a * c

Tactic:
⟨_, mul_assoc ..⟩

Premises used: mul_assoc, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a x : M
u : Mˣ
⊢ ∃ (c : M), a * x * (↑u : M) = a * c

Tactic:
exact ⟨_, mul_assoc ..⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a c w : M
h : a * c ~ᵤ a * c
⊢ ∃ (x : M), a * x ~ᵤ a * c

Tactic:
use c
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ LE.le (α := Associates M) (Associates.mk a) (Associates.mk b) → a ∣ b

Tactic:
mk_dvd_mk.mp

Premises used: Iff.mp, Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ a ∣ b → LE.le (α := Associates M) (Associates.mk a) (Associates.mk b)

Tactic:
mk_dvd_mk.mpr

Premises used: Iff.mpr, Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ LE.le (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ a ∣ b

Tactic:
mk_dvd_mk

Premises used: Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
simp_rw :
  (∀ (a_1 a_2 : M),
      a ∣ a_1 * a_2 →
        ∃ (x : M),
          ∃ (x_1 : M), x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
⊢ IsPrimal (α := Associates M) (Associates.mk a) ↔ IsPrimal a

Tactic:
simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]

Premises used: IsPrimal, Function.Surjective.exists, Associates.forall_associated, Associates.mk_surjective, Associates.mk_mul_mk, Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
mp :
  (∀ (a_1 a_2 : M),
      a ∣ a_1 * a_2 →
        ∃ (x : M),
          ∃ (x_1 : M), x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))) →
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
mpr :
  (∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂) →
    ∀ (a_2 a_3 : M),
      a ∣ a_2 * a_3 →
        ∃ (x : M), ∃ (x_1 : M), x ∣ a_2 ∧ x_1 ∣ a_3 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))
⊢ (∀ (a_1 a_2 : M),
      a ∣ a_1 * a_2 →
        ∃ (x : M),
          ∃ (x_1 : M), x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
h :
  ∀ (a_1 a_2 : M),
    a ∣ a_1 * a_2 →
      ∃ (x : M), ∃ (x_1 : M), x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))
b c : M
dvd : a ∣ b * c
mp :
  ∀ (a₁ a₂ : M) (h₁ : a₁ ∣ b) (h₂ : a₂ ∣ c) (eq : Eq (α := Associates M) (Associates.mk a) (Associates.mk (a₁ * a₂))),
    ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
⊢ ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
mpr :
  ∀ (a₁ a₂ : M) (h₁ : a₁ ∣ b) (h₂ : a₂ ∣ c) (eq : a = a₁ * a₂),
    ∃ (x : M), ∃ (x_1 : M), x ∣ b ∧ x_1 ∣ c ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))
⊢ ∃ (x : M), ∃ (x_1 : M), x ∣ b ∧ x_1 ∣ c ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))

Tactic:
obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
h :
  ∀ (a_1 a_2 : M),
    a ∣ a_1 * a_2 →
      ∃ (x : M), ∃ (x_1 : M), x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : Eq (α := Associates M) (Associates.mk a) (Associates.mk (a₁ * a₂))
mp :
  ∀ (u : Mˣ)
    (h :
      ∀ (a a_1 : M),
        a₁ * a₂ * (↑u : M) ∣ a * a_1 →
          ∃ (x : M),
            ∃ (x_1 : M),
              x ∣ a ∧ x_1 ∣ a_1 ∧ Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (x * x_1)))
    (dvd : a₁ * a₂ * (↑u : M) ∣ b * c)
    (eq : Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (a₁ * a₂))),
    ∃ (a₁_1 : M), ∃ (a₂_1 : M), a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * (↑u : M) = a₁_1 * a₂_1
⊢ ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm

Premises used: Associates.mk_eq_mk_iff_associated, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
b c a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
u : Mˣ
h :
  ∀ (a a_1 : M),
    a₁ * a₂ * (↑u : M) ∣ a * a_1 →
      ∃ (x : M),
        ∃ (x_1 : M),
          x ∣ a ∧ x_1 ∣ a_1 ∧ Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (x * x_1))
dvd : a₁ * a₂ * (↑u : M) ∣ b * c
eq : Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (a₁ * a₂))
⊢ ∃ (a₁_1 : M), ∃ (a₂_1 : M), a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * (↑u : M) = a₁_1 * a₂_1

Tactic:
⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩

Premises used: Iff.mpr, Units.val, HMul.hMul, mul_assoc, Units.mul_right_dvd, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
b c a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
u : Mˣ
h :
  ∀ (a a_1 : M),
    a₁ * a₂ * (↑u : M) ∣ a * a_1 →
      ∃ (x : M),
        ∃ (x_1 : M),
          x ∣ a ∧ x_1 ∣ a_1 ∧ Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (x * x_1))
dvd : a₁ * a₂ * (↑u : M) ∣ b * c
eq : Eq (α := Associates M) (Associates.mk (a₁ * a₂ * (↑u : M))) (Associates.mk (a₁ * a₂))
⊢ ∃ (a₁_1 : M), ∃ (a₂_1 : M), a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * (↑u : M) = a₁_1 * a₂_1

Tactic:
exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ (x : M), ∃ (x_1 : M), x ∣ b ∧ x_1 ∣ c ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))

Tactic:
⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩

Premises used: congr_arg, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ (a₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ (x : M), ∃ (x_1 : M), x ∣ b ∧ x_1 ∣ c ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))

Tactic:
exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
simp_rw : (∀ (a : Associates M), IsPrimal a) ↔ ∀ (a : M), IsPrimal a
simp_rw₁ : (∀ (a : M), IsPrimal (α := Associates M) (Associates.mk a)) ↔ ∀ (a : M), IsPrimal a
⊢ DecompositionMonoid.{u_1} (Associates M) ↔ DecompositionMonoid M

Tactic:
simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]

Premises used: decompositionMonoid_iff, Associates.forall_associated, Associates.isPrimal_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : DecompositionMonoid M
⊢ DecompositionMonoid.{u_1} (Associates M)

Tactic:
decompositionMonoid_iff.mpr ‹_›

Premises used: Iff.mpr, Associates.decompositionMonoid_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
simp_rw :
  (∀ ⦃d : Associates M⦄, d ∣ Associates.mk a → d ∣ Associates.mk b → IsUnit d) ↔ ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d
simp_rw₁ :
  (∀ (a_1 : M),
      Dvd.dvd (α := Associates M) (Associates.mk a_1) (Associates.mk a) →
        Dvd.dvd (α := Associates M) (Associates.mk a_1) (Associates.mk b) →
          IsUnit (M := Associates M) (Associates.mk a_1)) ↔
    ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d
simp_rw₂ :
  (∀ (a_1 : M), a_1 ∣ a → a_1 ∣ b → IsUnit (M := Associates M) (Associates.mk a_1)) ↔
    ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d
⊢ IsRelPrime (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b

Tactic:
simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]

Premises used: Associates.forall_associated, IsRelPrime, Associates.isUnit_mk, Associates.mk_dvd_mk
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Zero M
inst_1 : Monoid M
⊢ Eq.{u_1 + 1} (α := Associates M) (Associates.mk 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
⊢ Eq (α := Associates M) (Associates.mk a) 0 ↔ a = 0

Tactic:
⟨fun h => (associated_zero_iff_eq_zero a).1 <| Quotient.exact h, fun h => h.symm ▸ rfl⟩

Premises used: associated_zero_iff_eq_zero, Eq.rec, Iff.intro, Quotient.exact, Iff.mp, Eq.symm, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
rw : Eq.{u_1 + 1} (α := Associates M) (Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) 0)) 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Associates M) 0 0
⊢ Eq.{u_1 + 1} (α := M) (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) 0) 0

Tactic:
rw [← mk_eq_zero, quot_out]

Premises used: Associates.mk_eq_zero, Associates.quot_out
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
⊢ Ne (α := Associates M) (Associates.mk a) 0 ↔ a ≠ 0

Tactic:
not_congr mk_eq_zero

Premises used: Associates.mk_eq_zero, not_congr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : Nontrivial M
⊢ Nontrivial.{u_1} (Associates M)

Tactic:
⟨⟨1, 0, mk_ne_zero.2 one_ne_zero⟩⟩

Premises used: Iff.mpr, Nontrivial.mk, Exists.intro, Associates.mk_ne_zero, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : Associates M
⊢ a ≠ 0 → ∃ (a0 : M), a0 ≠ 0 ∧ Associates.mk a0 = a

Tactic:
Quotient.inductionOn a fun b nz => ⟨b, mt (congr_arg Quotient.mk'') nz, rfl⟩

Premises used: Quotient.inductionOn
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
rw : HMul.hMul (α := Associates M) (Associates.mk 0) (Associates.mk a) = Associates.mk 0
rw₁ : Eq (α := Associates M) (Associates.mk (0 * a)) (Associates.mk 0)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Associates M) (Associates.mk 0) (Associates.mk 0)
⊢ HMul.hMul (α := Associates M) 0 (Associates.mk a) = 0

Tactic:
rw [← mk_zero, mk_mul_mk, zero_mul]

Premises used: Associates.mk_zero, MulZeroClass.zero_mul, Associates.mk_mul_mk