awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a c d : M
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False

Tactic:
apply ha0 a_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 * c ≠ 0

Tactic:
have hac0 : a * c ≠ 0 := by
    intro con
    rw [con, zero_mul] at a_eq
    apply ha0 a_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
rw₂ rw₃ : a = a
⊢ a * (c * d) = a * 1

Tactic:
rw [← mul_assoc, ← a_eq, mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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

Tactic:
have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
⊢ c * d = 1

Tactic:
have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
rw₂ rw₃ : a * c = a * c
⊢ a * c * (d * c) = a * c * 1

Tactic:
rw [← mul_assoc, ← a_eq, mul_one]

Premises used: mul_assoc, mul_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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

Tactic:
have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
⊢ d * c = 1

Tactic:
have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
hdc : d * c = 1
⊢ a ~ᵤ a * c

Tactic:
⟨⟨c, d, hcd, hdc⟩, rfl⟩

Premises used: Associated, Units.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
hdc : d * c = 1
⊢ a ~ᵤ a * c

Tactic:
exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
inst_1 : IsLeftCancelMulZero M
a b : M
⊢ a ∣ b ∧ b ∣ a ↔ a ~ᵤ b

Tactic:
⟨fun ⟨h1, h2⟩ => associated_of_dvd_dvd h1 h2, Associated.dvd_dvd⟩

Premises used: associated_of_dvd_dvd, Associated.dvd_dvd, Associated, _private.0.dvd_dvd_iff_associated.match_1, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : a ~ᵤ b
⊢ a ∣ c ↔ b ∣ c

Tactic:
let ⟨_, hu⟩ := h
  hu ▸ Units.mul_right_dvd.symm

Premises used: Dvd.dvd, Units.mul_right_dvd, Eq.rec, Iff, _private.0.Associated.dvd.match_1, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b c : M
h : b ~ᵤ c
⊢ a ∣ b ↔ a ∣ c

Tactic:
let ⟨_, hu⟩ := h
  hu ▸ Units.dvd_mul_right.symm

Premises used: Dvd.dvd, Eq.rec, Iff, Units.dvd_mul_right, _private.0.Associated.dvd.match_1, Iff.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a b : M
h : a ~ᵤ b
obtain : ∀ (u : Mˣ), a = 0 ↔ a * (↑u : M) = 0
⊢ a = 0 ↔ b = 0

Tactic:
obtain ⟨u, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a : M
u : Mˣ
rw : a = 0 ↔ a = 0 * (↑u⁻¹ : M)
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ a = 0 ↔ a * (↑u : M) = 0

Tactic:
rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]

Premises used: MulZeroClass.zero_mul, Units.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : MonoidWithZero M
a b : M
h : a ~ᵤ b
⊢ a ≠ 0 ↔ b ≠ 0

Tactic:
not_congr h.eq_zero_iff

Premises used: Associated.eq_zero_iff, not_congr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * (↑u : M) = q
h_1 : IsUnit q
v : Mˣ
hv : (↑v : M) = q
⊢ (↑(v * u⁻¹) : M) = p

Tactic:
simp [hv, hu.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * (↑u : M) = q
rw : ∀ (a b : M), p * (↑u : M) ∣ a * b → p * (↑u : M) ∣ a ∨ p * (↑u : M) ∣ b
⊢ ∀ (a b : M), q ∣ a * b → q ∣ a ∨ q ∣ b

Tactic:
rw [← hu]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * (↑u : M) = q
simp : ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ∀ (a b : M), p * (↑u : M) ∣ a * b → p * (↑u : M) ∣ a ∨ p * (↑u : M) ∣ b

Tactic:
simp only [Units.isUnit, IsUnit.mul_right_dvd]

Premises used: Units.isUnit, IsUnit.mul_right_dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
hp.dvd_or_dvd

Premises used: Prime.dvd_or_dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
exact hp.dvd_or_dvd

Premises used: Prime.dvd_or_dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
refine_2 : Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)
⊢ Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
refine_1₁ : ∀ (hy : IsUnit y), Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
rcases of_irreducible_mul h.irreducible with hx | hy

Premises used: Prime.irreducible, of_irreducible_mul
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩

Premises used: And.intro, associated_unit_mul_left, Associated.prime, Or.inr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩

Premises used: associated_mul_unit_left, And.intro, Associated.prime, Or.inl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩

Premises used: Or.inl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

Tactic:
(associated_mul_unit_left x y hy).symm.prime hx

Premises used: Associated.symm, associated_mul_unit_left, Associated.prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

Tactic:
exact (associated_mul_unit_left x y hy).symm.prime hx

Premises used: Associated.symm, associated_mul_unit_left, Associated.prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
(associated_unit_mul_right y x hx).prime hy

Premises used: associated_unit_mul_right, Associated.prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
exact (associated_unit_mul_right y x hx).prime hy

Premises used: associated_unit_mul_right, Associated.prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
h : Prime p ∧ n = 1
hp : Prime p
hn : n = 1
⊢ Prime (p ^ n)

Tactic:
simpa [hn]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
refine : ∀ (hp : Prime (p ^ n)), Prime p ∧ n = 1
⊢ Prime (p ^ n) ↔ Prime p ∧ n = 1

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨hp, hn⟩ ↦ by simpa [hn]⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
this : n = 1
⊢ Prime p ∧ n = 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
suffices : n = 1
⊢ Prime p ∧ n = 1

Tactic:
suffices n = 1 by simp_all
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
⊢ n = 1

Tactic:
grind [not_prime_pow, Nat.zero_eq_one_mod_iff]

Premises used: Nat.zero_eq_one_mod_iff, not_prime_pow
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
mp : y ∣ x → IsUnit y ∨ x ~ᵤ y
mpr : IsUnit y ∨ x ~ᵤ y → y ∣ x
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
mp₁ : ∀ (h : IsUnit z), IsUnit y ∨ x ~ᵤ y
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
obtain (h | h) := hx.isUnit_or_isUnit hz

Premises used: Irreducible.isUnit_or_isUnit
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
mp : IsUnit y ∨ y * z ~ᵤ y
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
rw [hz]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ∨ y * z ~ᵤ y

Tactic:
Or.inr (associated_mul_unit_left _ _ h)

Premises used: associated_mul_unit_left, Or.inr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ∨ y * z ~ᵤ y

Tactic:
exact Or.inr (associated_mul_unit_left _ _ h)

Premises used: associated_mul_unit_left, Or.inr
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

Tactic:
hy.dvd

Premises used: IsUnit.dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

Tactic:
exact hy.dvd

Premises used: IsUnit.dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
h.symm.dvd

Premises used: Associated.dvd, Associated.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
exact h.symm.dvd

Premises used: Associated.dvd, Associated.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p q : M
p_irr : Irreducible p
q_irr : Irreducible q
dvd : p ∣ q
⊢ p ~ᵤ q

Tactic:
((q_irr.dvd_iff.mp dvd).resolve_left p_irr.not_isUnit).symm

Premises used: Irreducible.not_isUnit, Or.resolve_left, Associated.symm, Iff.mp, Irreducible.dvd_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p q : M
pp : Irreducible p
qp : Irreducible q
⊢ p ∣ q ↔ p ~ᵤ q

Tactic:
⟨Irreducible.associated_of_dvd pp qp, Associated.dvd⟩

Premises used: Irreducible.associated_of_dvd, Associated.dvd, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
p_prime : Prime p
q_prime : Prime q
dvd : p ∣ q
⊢ p ~ᵤ q

Tactic:
p_prime.irreducible.associated_of_dvd q_prime.irreducible dvd

Premises used: Prime.irreducible, Irreducible.associated_of_dvd
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p q : M
pp : Prime p
qp : Prime q
⊢ p ∣ q ↔ p ~ᵤ q

Tactic:
pp.irreducible.dvd_irreducible_iff_associated qp.irreducible

Premises used: Prime.irreducible, Irreducible.dvd_irreducible_iff_associated
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
⊢ Prime p ↔ Prime q

Tactic:
⟨h.prime, h.symm.prime⟩

Premises used: Associated.symm, Iff.intro, Associated.prime
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a ~ᵤ b
u : Mˣ
hu : a * (↑u : M) = b
h_1 : IsUnit a
v : Mˣ
hv : (↑v : M) = a
⊢ (↑(v * u) : M) = b

Tactic:
simp [hv, hu.symm]

Premises used: Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
a b : M
h : a ~ᵤ b
⊢ IsUnit a ↔ IsUnit b

Tactic:
⟨h.isUnit, h.symm.isUnit⟩

Premises used: Associated.isUnit, Associated.symm, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
x y : M
hx : Irreducible x
hy : y ∣ x
⊢ IsUnit y ↔ ¬x ~ᵤ y

Tactic:
⟨fun hy hxy => hx.1 (hxy.symm.isUnit hy), (hx.dvd_iff.mp hy).resolve_right⟩

Premises used: Irreducible.not_isUnit, Associated.isUnit, Associated.symm, Iff.intro, Iff.mp, Irreducible.dvd_iff, Or.resolve_right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 = p * (↑u : M) * (↑u⁻¹ : M)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
rw : q * (↑u⁻¹ : M) = a * (b * (↑u⁻¹ : M))
⊢ p * (↑u : M) * (↑u⁻¹ : M) = a * (b * (↑u⁻¹ : M))

Tactic:
rw [hu]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
⊢ q * (↑u⁻¹ : M) = a * (b * (↑u⁻¹ : M))

Tactic:
simp [hab, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
hpab : p = a * (b * (↑u⁻¹ : M))
h_1 : IsUnit (b * (↑u⁻¹ : M))
v : Mˣ
hv : (↑v : M) = b * (↑u⁻¹ : M)
⊢ (↑(v * u) : M) = b

Tactic:
simp [hv]
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p q : M
h : p ~ᵤ q
⊢ Irreducible p ↔ Irreducible q

Tactic:
⟨h.irreducible, h.symm.irreducible⟩

Premises used: Associated.irreducible, Associated.symm, Iff.intro
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
rw : c * (↑v : M) * (b * (↑(u * v) : M)) = (↑v : M) * (a * b * (↑u : M))
⊢ a * (b * (↑(u * v) : M)) = a * d

Tactic:
rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]

Premises used: Units.val, mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
⊢ c * (↑v : M) * (b * (↑(u * v) : M)) = (↑v : M) * (a * b * (↑u : M))

Tactic:
simp [hv.symm, mul_comm, mul_left_comm]

Premises used: mul_left_comm, mul_comm, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c d : M
rw : b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
rw [mul_comm a, mul_comm c]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
Associated.of_mul_left

Premises used: Associated.of_mul_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
exact Associated.of_mul_left

Premises used: Associated.of_mul_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂
rw : p₁ ∣ p₁ ^ k₁
⊢ p₁ ∣ p₂ ^ k₂

Tactic:
rw [← h.dvd_iff_dvd_right]

Premises used: Associated.dvd_iff_dvd_right
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₁

Tactic:
apply dvd_pow_self _ hk₁.ne'

Premises used: dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂

Tactic:
have : p₁ ∣ p₂ ^ k₂ := by
    rw [← h.dvd_iff_dvd_right]
    apply dvd_pow_self _ hk₁.ne'
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂
rw : p₁ ∣ p₂
⊢ p₁ ~ᵤ p₂

Tactic:
rw [← hp₁.dvd_prime_iff_associated hp₂]

Premises used: Prime.dvd_prime_iff_associated
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂

Tactic:
hp₁.dvd_of_dvd_pow this

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂

Tactic:
exact hp₁.dvd_of_dvd_pow this

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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₂

Tactic:
(h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm

Premises used: Associated.of_pow_associated_of_prime, Associated.symm
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n

Tactic:
⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩

Premises used: Irreducible.not_isUnit, Iff.intro, dvd_rfl
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
refine : ∀ (hpn : ¬p ∣ n) (d : M) (hdp : d ∣ p) (hdn : d ∣ n), IsUnit d
⊢ IsRelPrime p n ↔ ¬p ∣ n

Tactic:
refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
contrapose : ∀ (hpn : ¬IsUnit d), p ∣ n
⊢ IsUnit d

Tactic:
contrapose hpn
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
suffices : p ~ᵤ d
⊢ p ∣ n

Tactic:
suffices Associated p d from this.dvd.trans hdn
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ~ᵤ d

Tactic:
(hp.dvd_iff.mp hdp).resolve_left hpn

Premises used: Or.resolve_left, Iff.mp, Irreducible.dvd_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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 ~ᵤ d

Tactic:
exact (hp.dvd_iff.mp hdp).resolve_left hpn

Premises used: Or.resolve_left, Iff.mp, Irreducible.dvd_iff
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
p n : M
hp : Irreducible p
⊢ p ∣ n ∨ IsRelPrime p n

Tactic:
Classical.or_iff_not_imp_left.mpr hp.isRelPrime_iff_not_dvd.2

Premises used: Iff.mpr, Irreducible.isRelPrime_iff_not_dvd, Classical.or_iff_not_imp_left
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
x y : M
⊢ x ~ᵤ y ↔ x = y

Tactic:
simp [Associated, Units.eq_one]

Premises used: Associated, Units.eq_one
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
h : ∀ (x x_1 : M), x ~ᵤ x_1 ↔ x = x_1
⊢ Eq.{u_1 + 1} (α := (x y : M) → Prop) Associated Eq

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Associated
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
x x_1 : M
h h₁ : x = x_1 ↔ x = x_1
⊢ x ~ᵤ x_1 ↔ x = x_1

Tactic:
rw [associated_iff_eq]

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GroupWithZero.Associated
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
rw₁ rw₂ : p ~ᵤ q ↔ p ~ᵤ q
⊢ p ∣ q ↔ p = q

Tactic:
rw [pp.dvd_prime_iff_associated qp, ← associated_eq_eq]

Premises used: associated_eq_eq, Prime.dvd_prime_iff_associated