awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ ∃ (x : M), ∃ (x_1 : M), x ∣ b ∧ x_1 ∣ c ∧ Eq (α := Associates M) (Associates.mk a) (Associates.mk (x * x_1))
have 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))
Tactic: obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd
-- 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₁ 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₂
have 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
Tactic: obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm
Cleared hypotheses: a, h, dvd, eq
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
⊢ DecompositionMonoid.{u_1} (Associates M) ↔ DecompositionMonoid M
have simp_rw : (∀ (a : Associates M), IsPrimal a) ↔ ∀ (a : M), IsPrimal a
Tactic: simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
simp_rw : (∀ (a : Associates M), IsPrimal a) ↔ ∀ (a : M), IsPrimal a
⊢ DecompositionMonoid.{u_1} (Associates M) ↔ DecompositionMonoid M
have simp_rw₁ : (∀ (a : M), IsPrimal (α := Associates M) (Associates.mk a)) ↔ ∀ (a : M), IsPrimal a
Tactic: simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoid M
a b : M
⊢ IsRelPrime (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
have simp_rw : (∀ ⦃d : Associates M⦄, d ∣ Associates.mk a → d ∣ Associates.mk b → IsUnit d) ↔ ∀ ⦃d : M⦄, d ∣ a → d ∣ b → IsUnit d
Tactic: simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ IsRelPrime (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
have 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
Tactic: simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ IsRelPrime (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
have 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
Tactic: simp_rw [IsRelPrime, forall_associated, mk_dvd_mk, isUnit_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : MonoidWithZero M
⊢ Eq.{u_1 + 1} (α := M) (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) 0) 0
have rw : Eq.{u_1 + 1} (α := Associates M) (Associates.mk (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) 0)) 0
Tactic: rw [← mk_eq_zero, quot_out]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ Eq.{u_1 + 1} (α := M) (Quot.out (r := (⇑(Associated.setoid M) : M → M → Prop)) 0) 0
have rw₁ : Eq.{u_1 + 1} (α := Associates M) 0 0
Tactic: rw [← mk_eq_zero, quot_out]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
⊢ HMul.hMul (α := Associates M) 0 (Associates.mk a) = 0
have rw : HMul.hMul (α := Associates M) (Associates.mk 0) (Associates.mk a) = Associates.mk 0
Tactic: rw [← mk_zero, mk_mul_mk, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
rw : HMul.hMul (α := Associates M) (Associates.mk 0) (Associates.mk a) = Associates.mk 0
⊢ HMul.hMul (α := Associates M) 0 (Associates.mk a) = 0
have rw₁ : Eq (α := Associates M) (Associates.mk (0 * a)) (Associates.mk 0)
Tactic: rw [← mk_zero, mk_mul_mk, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ HMul.hMul (α := Associates M) 0 (Associates.mk a) = 0
have rw₂ : Eq.{u_1 + 1} (α := Associates M) (Associates.mk 0) (Associates.mk 0)
Tactic: rw [← mk_zero, mk_mul_mk, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
⊢ HMul.hMul (α := Associates M) (Associates.mk a) 0 = 0
have rw : HMul.hMul (α := Associates M) (Associates.mk a) (Associates.mk 0) = Associates.mk 0
Tactic: rw [← mk_zero, mk_mul_mk, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
rw : HMul.hMul (α := Associates M) (Associates.mk a) (Associates.mk 0) = Associates.mk 0
⊢ HMul.hMul (α := Associates M) (Associates.mk a) 0 = 0
have rw₁ : Eq (α := Associates M) (Associates.mk (a * 0)) (Associates.mk 0)
Tactic: rw [← mk_zero, mk_mul_mk, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ HMul.hMul (α := Associates M) (Associates.mk a) 0 = 0
have rw₂ : Eq.{u_1 + 1} (α := Associates M) (Associates.mk 0) (Associates.mk 0)
Tactic: rw [← mk_zero, mk_mul_mk, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p : M
⊢ Prime (M := Associates M) (Associates.mk p) ↔ Prime p
have 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
Tactic: rw [Prime, _root_.Prime, forall_associated]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
⊢ Irreducible (M := Associates M) (Associates.mk a) ↔ Irreducible a
have 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
Tactic: simp only [irreducible_iff, isUnit_mk, forall_associated, isUnit_mk, mk_mul_mk,
    mk_eq_mk_iff_associated, Associated.comm (x := a)]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
⊢ (¬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
have 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
Tactic: apply Iff.rfl.and
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : M
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
⊢ DvdNotUnit (α := Associates M) (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
have simp : (a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ b = a * x
Tactic: simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, 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 : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ (x : M), ¬IsUnit x ∧ b = a * x
have refine : (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ (x : M), ¬IsUnit x ∧ b = a * x
Tactic: refine Iff.rfl.and ?_
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : M
⊢ (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ (x : M), ¬IsUnit x ∧ b = a * x
have mp : (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ (x : M), ¬IsUnit x ∧ b = a * x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ (∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ (x : M), ¬IsUnit x ∧ b = a * x
have mpr : (∃ (x : M), ¬IsUnit x ∧ b = a * x) → ∃ (x : M), ¬IsUnit x ∧ a * x ~ᵤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
have mp : ¬IsUnit (x * (↑u : M))
Tactic: refine ⟨x * u, ?_, mul_assoc ..⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
w : M
⊢ ∃ (x_1 : M), ¬IsUnit x_1 ∧ a * x_1 ~ᵤ a * x
have h : ¬IsUnit x ∧ a * x ~ᵤ a * x
Tactic: use x
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ DvdNotUnit a b
have left : a ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : Associates M
hlt : a < b
left : a ≠ 0
⊢ DvdNotUnit a b
have right : ∃ (x : Associates M), ¬IsUnit x ∧ b = a * x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
b : Associates M
hlt : 0 < b
⊢ False
have apply : b ≤ 0
Tactic: apply not_lt_of_ge _ hlt
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a b : Associates M
hlt : a < b
⊢ ∃ (x : Associates M), ¬IsUnit x ∧ b = a * x
have right : ∀ (x : Associates M) (ndvd : ¬a * x ∣ a), ∃ (x_1 : Associates M), ¬IsUnit x_1 ∧ a * x = a * x_1
Tactic: rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩
Cleared hypotheses: b, hlt
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
have right : ¬IsUnit x
Tactic: refine ⟨x, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : ¬a * x ∣ a
⊢ ¬IsUnit x
have right : ∀ (ndvd : IsUnit x), a * x ∣ a
Tactic: contrapose ndvd
Cleared hypotheses: ndvd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
⊢ a * x ∣ a
have right : ∀ (u : (Associates M)ˣ), a * (↑u : Associates M) ∣ a
Tactic: rcases ndvd with ⟨u, rfl⟩
Cleared hypotheses: x, ndvd
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
have simp_rw : (∀ (a : M), Irreducible a ↔ Prime a) ↔
  ∀ (a : M), Irreducible (M := Associates M) (Associates.mk a) ↔ Prime (M := Associates M) (Associates.mk a)
Tactic: simp_rw [forall_associated, irreducible_mk, prime_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates M), Irreducible a ↔ Prime a
have simp_rw₁ : (∀ (a : M), Irreducible a ↔ Prime a) ↔ ∀ (a : M), Irreducible a ↔ Prime (M := Associates M) (Associates.mk a)
Tactic: simp_rw [forall_associated, irreducible_mk, prime_mk]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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))
⊢ Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
    (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)
have 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)
Tactic: rcases Quotient.exact' h with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
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
⊢ Eq (α := Associates M) (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) b)
    (Quot.mk (⇑(Associated.setoid M) : M → M → Prop) c)
have hu₁ : a * (b * (↑u : M)) = a * c
Tactic: have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p m : Associates M
hp : Prime p
hle : m ≤ p
⊢ m = 1 ∨ m = p
have rcases : ∀ (p : M) (hp : Prime (M := Associates M) (Associates.mk p)) (hle : m ≤ Associates.mk p), m = 1 ∨ m = Associates.mk p
Tactic: rcases mk_surjective p with ⟨p, rfl⟩
Cleared hypotheses: p, hp, hle
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ m = 1 ∨ m = Associates.mk p
have 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)
Tactic: rcases mk_surjective m with ⟨m, rfl⟩
Cleared hypotheses: m, hle
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
⊢ p ≤ 1 ↔ p = 1
have rw : p ≤ ⊥ ↔ p = ⊥
Tactic: rw [← Associates.bot_eq_one, le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
rw : p ≤ ⊥ ↔ p = ⊥
⊢ p ≤ 1 ↔ p = 1
have rw₁ : p = ⊥ ↔ p = ⊥
Tactic: rw [← Associates.bot_eq_one, le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : Nontrivial M
p q r : M
h : DvdNotUnit p q
h' : q ~ᵤ r
⊢ DvdNotUnit p r
have obtain : ∀ (u : Mˣ) (h : DvdNotUnit p (r * (↑u : M))) (h' : r * (↑u : M) ~ᵤ r), DvdNotUnit p r
Tactic: obtain ⟨u, rfl⟩ := Associated.symm h'
Cleared hypotheses: q, h, h'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ DvdNotUnit p r
have obtain : ∀ (hp : p ≠ 0) (x : M) (hx : ¬IsUnit x ∧ r * (↑u : M) = p * x), DvdNotUnit p r
Tactic: obtain ⟨hp, x, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
have refine : r = p * (x * (↑u⁻¹ : M))
Tactic: refine ⟨hp, x * ↑u⁻¹, DvdNotUnit.not_unit ⟨u⁻¹.ne_zero, x, hx.left, mul_comm _ _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ r = p * (x * (↑u⁻¹ : M))
have rw : r = p * x * (↑u⁻¹ : M)
Tactic: rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ r = p * (x * (↑u⁻¹ : M))
have rw₁ : r = r * (↑u : M) * (↑u⁻¹ : M)
Tactic: rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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)
⊢ r = p * (x * (↑u⁻¹ : M))
have rw₂ : r = r * ((↑u : M) * (↑u⁻¹ : M))
Tactic: rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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))
⊢ r = p * (x * (↑u⁻¹ : M))
have rw₃ : r = r * 1
Tactic: rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ r = p * (x * (↑u⁻¹ : M))
have rw₄ : r = r
Tactic: rw [← mul_assoc, ← hx.right, mul_assoc, Units.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b
have obtain : ∀ (a : Mˣ) (ha : p * b * (↑a : M) = p), IsUnit b
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
have refine : p * (b * (↑a : M)) = p * 1
Tactic: refine .of_mul_eq_one a ((mul_right_inj' hp).mp ?_)
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
⊢ p * (b * (↑a : M)) = p * 1
have rwa : p * b * (↑a : M) = p * 1
Tactic: rwa [← mul_assoc, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
a : Mˣ
h : DvdNotUnit p (p * (↑a : M))
⊢ False
have obtain : ∀ (hp : p ≠ 0) (x : M) (hx : ¬IsUnit x) (hx' : p * (↑a : M) = p * x), False
Tactic: obtain ⟨hp, x, hx, hx'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
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
⊢ False
have hx₁ : ¬IsUnit (↑a : M)
Tactic: rcases (mul_right_inj' hp).mp hx' with rfl
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
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)
⊢ False
have hx'₁ : p * (↑a : M) = p * (↑a : M)
Tactic: rcases (mul_right_inj' hp).mp hx' with rfl
Cleared hypotheses: x, hx, hx'
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (goal)
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
have succ : ∀ (h : 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)⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Associated (hypothesis)
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)
⊢ ∃ (i : ℕ), i ≤ n + 1 ∧ q ~ᵤ p ^ i
have h₁ : q ∣ p * p ^ n
Tactic: rw [pow_succ'] at h
Cleared hypotheses: h