awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
pos : ∀ (ha0 : a = 0), a ~ᵤ a * c
⊢ a ~ᵤ a * c
have neg : ∀ (ha0 : ¬a = 0), a ~ᵤ a * c
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
⊢ False
have a_eq₁ : a = 0
Tactic: rw [con, zero_mul] at a_eq
Cleared hypotheses: a_eq, ha0, con
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c
have hac0 : a * c ≠ 0
Tactic: have hac0 : a * c ≠ 0 := by
    intro con
    rw [con, zero_mul] at a_eq
    apply ha0 a_eq
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a * (c * d) = a * 1
have rw : a * c * d = a * 1
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
rw : a * c * d = a * 1
⊢ a * (c * d) = a * 1
have rw₁ : a = a * 1
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
rw : a * c * d = a * 1
rw₁ : a = a * 1
⊢ a * (c * d) = a * 1
have rw₂ : a = a
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c
have this : a * (c * d) = a * 1
Tactic: have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
⊢ a ~ᵤ a * c
have hcd : c * d = 1
Tactic: have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c * (d * c) = a * c * 1
have rw : a * c * d * c = a * c * 1
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
rw : a * c * d * c = a * c * 1
⊢ a * c * (d * c) = a * c * 1
have rw₁ : a * c = a * c * 1
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
rw : a * c * d * c = a * c * 1
rw₁ : a * c = a * c * 1
⊢ a * c * (d * c) = a * c * 1
have rw₂ : a * c = a * c
Tactic: rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a ~ᵤ a * c
have this₁ : a * c * (d * c) = a * c * 1
Tactic: have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this_1 : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
⊢ a ~ᵤ a * c
have hdc : d * c = 1
Tactic: have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
a b : M
h : a ~ᵤ b
⊢ a = 0 ↔ b = 0
have obtain : ∀ (u : Mˣ), a = 0 ↔ a * (↑u : M) = 0
Tactic: obtain ⟨u, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
u : Mˣ
⊢ a = 0 ↔ a * (↑u : M) = 0
have rw : a = 0 ↔ a = 0 * (↑u⁻¹ : M)
Tactic: rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
u : Mˣ
rw : a = 0 ↔ a = 0 * (↑u⁻¹ : M)
⊢ a = 0 ↔ a * (↑u : M) = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * (↑u : M) = q
⊢ ∀ (a b : M), q ∣ a * b → q ∣ a ∨ q ∣ b
have rw : ∀ (a b : M), p * (↑u : M) ∣ a * b → p * (↑u : M) ∣ a ∨ p * (↑u : M) ∣ b
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * (↑u : M) = q
⊢ ∀ (a b : M), p * (↑u : M) ∣ a * b → p * (↑u : M) ∣ a ∨ p * (↑u : M) ∣ b
have simp : ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b
Tactic: simp only [Units.isUnit, IsUnit.mul_right_dvd]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
⊢ Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
have refine_1 : ∀ (h : Prime (x * y)), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
refine_1 : ∀ (h : Prime (x * y)), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
⊢ Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
have refine_2 : Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
have refine_1 : ∀ (hx : IsUnit x), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Tactic: rcases of_irreducible_mul h.irreducible with hx | hy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
refine_1 : ∀ (hx : IsUnit x), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
have refine_1₁ : ∀ (hy : IsUnit y), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
Tactic: rcases of_irreducible_mul h.irreducible with hx | hy
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
⊢ Prime (p ^ n) ↔ Prime p ∧ n = 1
have refine : ∀ (hp : Prime (p ^ n)), Prime p ∧ n = 1
Tactic: refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ Prime p ∧ n = 1
have suffices : n = 1
Tactic: suffices n = 1 by simp_all
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y
have mp : y ∣ x → IsUnit y ∨ x ~ᵤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
mp : y ∣ x → IsUnit y ∨ x ~ᵤ y
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y
have mpr : IsUnit y ∨ x ~ᵤ y → y ∣ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
⊢ IsUnit y ∨ x ~ᵤ y
have mp : ∀ (h : IsUnit y), IsUnit y ∨ x ~ᵤ y
Tactic: obtain (h | h) := hx.isUnit_or_isUnit hz
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
mp : ∀ (h : IsUnit y), IsUnit y ∨ x ~ᵤ y
⊢ IsUnit y ∨ x ~ᵤ y
have mp₁ : ∀ (h : IsUnit z), IsUnit y ∨ x ~ᵤ y
Tactic: obtain (h | h) := hx.isUnit_or_isUnit hz
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y
have mp : IsUnit y ∨ y * z ~ᵤ y
Tactic: rw [hz]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * (↑u : M) = q
a b : M
hab : q = a * b
⊢ p * (↑u : M) * (↑u⁻¹ : M) = a * (b * (↑u⁻¹ : M))
have rw : q * (↑u⁻¹ : M) = a * (b * (↑u⁻¹ : M))
Tactic: rw [hu]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c d : M
h : a * b ~ᵤ c * d
h₁ : a ~ᵤ c
ha : a ≠ 0
u : Mˣ
hu : a * b * (↑u : M) = c * d
v : Mˣ
hv : c * (↑v : M) = a
⊢ a * (b * (↑(u * v) : M)) = a * d
have rw : c * (↑v : M) * (b * (↑(u * v) : M)) = (↑v : M) * (a * b * (↑u : M))
Tactic: rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c d : M
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
have rw : b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
Tactic: rw [mul_comm a, mul_comm c]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ∣ p₂ ^ k₂
have rw : p₁ ∣ p₁ ^ k₁
Tactic: rw [← h.dvd_iff_dvd_right]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
have this : p₁ ∣ p₂ ^ k₂
Tactic: have : p₁ ∣ p₂ ^ k₂ := by
    rw [← h.dvd_iff_dvd_right]
    apply dvd_pow_self _ hk₁.ne'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p₁ p₂ : M
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₁
h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂
this : p₁ ∣ p₂ ^ k₂
⊢ p₁ ~ᵤ p₂
have rw : p₁ ∣ p₂
Tactic: rw [← hp₁.dvd_prime_iff_associated hp₂]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n
have refine : ∀ (hpn : ¬p ∣ n) (d : M) (hdp : d ∣ p) (hdn : d ∣ n), IsUnit d
Tactic: refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
hpn : ¬p ∣ n
d : M
hdp : d ∣ p
hdn : d ∣ n
⊢ IsUnit d
have contrapose : ∀ (hpn : ¬IsUnit d), p ∣ n
Tactic: contrapose hpn
Cleared hypotheses: hpn
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
d : M
hdp : d ∣ p
hdn : d ∣ n
hpn : ¬IsUnit d
⊢ p ∣ n
have suffices : p ~ᵤ d
Tactic: suffices Associated p d from this.dvd.trans hdn
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
⊢ Eq.{u_1 + 1} (α := (x y : M) → Prop) Associated Eq
have h : ∀ (x x_1 : M), x ~ᵤ x_1 ↔ x = x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
x x_1 : M
⊢ x ~ᵤ x_1 ↔ x = x_1
have h : x = x_1 ↔ x = x_1
Tactic: rw [associated_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p = q
have rw : p ~ᵤ q ↔ p = q
Tactic: rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_2
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
inst_2 : Subsingleton.{u_2 + 1} Mˣ
p q : M
pp : Prime p
qp : Prime q
rw : p ~ᵤ q ↔ p = q
⊢ p ∣ q ↔ p = q
have rw₁ : p ~ᵤ q ↔ p ~ᵤ q
Tactic: rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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₂
have rw : ∀ (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂), p₁ ~ᵤ p₂
Tactic: rw [← associated_iff_eq] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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₂
have rw : ∀ (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂), p₁ ~ᵤ p₂
Tactic: rw [← associated_iff_eq] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a : Associates M
⊢ Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) a) = a
have rw : Quot.mk (⇑(Associated.setoid M) : M → M → Prop) (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) a) = a
Tactic: rw [← quot_mk_eq_mk, Quot.out_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) a) = a
have rw₁ : a = a
Tactic: rw [← quot_mk_eq_mk, Quot.out_eq]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) (Associates.mk a) ~ᵤ a
have rw : Eq (α := Associates M) (Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) (Associates.mk a)))
  (Associates.mk a)
Tactic: rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) (Associates.mk a) ~ᵤ a
have rw₁ : Eq (α := Associates M) (Associates.mk a) (Associates.mk a)
Tactic: rw [← Associates.mk_eq_mk_iff_associated, Associates.quot_out]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
⊢ Eq (α := Associates M) (Associates.mk a) 1 ↔ IsUnit a
have rw : Eq (α := Associates M) (Associates.mk a) (Associates.mk 1) ↔ IsUnit a
Tactic: rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : Monoid M
a : M
rw : Eq (α := Associates M) (Associates.mk a) (Associates.mk 1) ↔ IsUnit a
⊢ Eq (α := Associates M) (Associates.mk a) 1 ↔ IsUnit a
have rw₁ : a ~ᵤ 1 ↔ IsUnit a
Tactic: rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ Eq (α := Associates M) (Associates.mk a) 1 ↔ IsUnit a
have rw₂ : IsUnit a ↔ IsUnit a
Tactic: rw [← mk_one, mk_eq_mk_iff_associated, associated_one_iff_isUnit]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a' b' c' : Associates M
a b c : M
⊢ ⟦a * b * c⟧ = ⟦a * (b * c)⟧
have rw : ⟦a * (b * c)⟧ = ⟦a * (b * c)⟧
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a' b' : Associates M
a b : M
⊢ ⟦a * b⟧ = ⟦b * a⟧
have rw : ⟦b * a⟧ = ⟦b * a⟧
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : M
n : ℕ
⊢ Associates.mk (a ^ n) = HPow.hPow (α := Associates M) (Associates.mk a) n
have zero : Associates.mk (HPow.hPow (β := ℕ) a 0) = HPow.hPow (α := Associates M) (β := ℕ) (Associates.mk a) 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ Associates.mk (a ^ n) = HPow.hPow (α := Associates M) (Associates.mk a) n
have 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)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
hab : a * b = 1
hba : b * a = 1
⊢ { val := a, inv := b, val_inv := hab, inv_val := hba : (Associates M)ˣ } = default
have 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
Tactic: induction a, b using Quotient.inductionOn₂ with | _ a b
Cleared hypotheses: a, b, hab, hba
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = ⊥
have rw : a = 1 ↔ a = ⊥
Tactic: rw [Associates.isUnit_iff_eq_one, bot_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : Associates M
rw : a = 1 ↔ a = ⊥
⊢ IsUnit a ↔ a = ⊥
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [Associates.isUnit_iff_eq_one, bot_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ IsUnit (M := Associates M) (Associates.mk a) ↔ a ~ᵤ 1
have rw : Eq (α := Associates M) (Associates.mk a) 1 ↔ a ~ᵤ 1
Tactic: rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : M
rw : Eq (α := Associates M) (Associates.mk a) 1 ↔ a ~ᵤ 1
⊢ IsUnit (M := Associates M) (Associates.mk a) ↔ a ~ᵤ 1
have rw₁ : Eq (α := Associates M) (Associates.mk a) (Associates.mk 1) ↔ a ~ᵤ 1
Tactic: rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ IsUnit (M := Associates M) (Associates.mk a) ↔ a ~ᵤ 1
have rw₂ : a ~ᵤ 1 ↔ a ~ᵤ 1
Tactic: rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : Associates M
⊢ a ≤ b * a
have rw : a ≤ a * b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ Dvd.dvd (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ a ∣ b
have simp : (∃ (x : M), a * x ~ᵤ b) ↔ ∃ (c : M), b = a * c
Tactic: simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := b)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ (∃ (x : M), a * x ~ᵤ b) ↔ ∃ (c : M), b = a * c
have mp : (∃ (x : M), a * x ~ᵤ b) → ∃ (c : M), b = a * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
mp : (∃ (x : M), a * x ~ᵤ b) → ∃ (c : M), b = a * c
⊢ (∃ (x : M), a * x ~ᵤ b) ↔ ∃ (c : M), b = a * c
have mpr : (∃ (c : M), b = a * c) → ∃ (x : M), a * x ~ᵤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a c w : M
⊢ ∃ (x : M), a * x ~ᵤ a * c
have h : a * c ~ᵤ a * c
Tactic: use c
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ IsPrimal (α := Associates M) (Associates.mk a) ↔ IsPrimal a
have 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₂
Tactic: simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a : M
⊢ (∀ (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₂
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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₂
⊢ (∀ (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₂
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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₁ : M), ∃ (a₂ : M), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have 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₂
Tactic: obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd