awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
h : Associated x y
⊢ Squarefree x ↔ Squarefree y

Tactic:
⟨fun hx ↦ hx.squarefree_of_dvd h.dvd', fun hy ↦ hy.squarefree_of_dvd h.dvd⟩

Premises used: Associated.dvd, Squarefree.squarefree_of_dvd, Associated.dvd', Iff.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
contrapose! : ∀ (h' : n ≠ 0 ∧ n ≠ 1), IsUnit x
⊢ n = 0 ∨ n = 1

Tactic:
contrapose! h'
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ 2 ≤ n

Tactic:
replace h' : 2 ≤ n := by lia
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
rw : HPow.hPow (β := ℕ) x 2 ∣ x ^ n
⊢ x * x ∣ x ^ n

Tactic:
rw [← sq]

Premises used: sq
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ HPow.hPow (β := ℕ) x 2 ∣ x ^ n

Tactic:
pow_dvd_pow x h'

Premises used: pow_dvd_pow
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ HPow.hPow (β := ℕ) x 2 ∣ x ^ n

Tactic:
exact pow_dvd_pow x h'

Premises used: pow_dvd_pow
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n

Tactic:
have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
this : x * x ∣ x ^ n
⊢ IsUnit x

Tactic:
h.squarefree_of_dvd this x (refl _)

Premises used: Squarefree.squarefree_of_dvd, refl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
this : x * x ∣ x ^ n
⊢ IsUnit x

Tactic:
exact h.squarefree_of_dvd this x (refl _)

Premises used: Squarefree.squarefree_of_dvd, refl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
pos : ∀ (hu : IsUnit x), x ^ n ∣ x
neg : ∀ (hu : ¬IsUnit x), x ^ n ∣ x
⊢ x ^ n ∣ x

Tactic:
by_cases hu : IsUnit x

Premises used: IsUnit
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

Tactic:
(hu.pow n).dvd

Premises used: IsUnit.pow, IsUnit.dvd
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : IsUnit x
⊢ x ^ n ∣ x

Tactic:
exact (hu.pow n).dvd

Premises used: IsUnit.pow, IsUnit.dvd
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
neg : ∀ (h : HPow.hPow (β := ℕ) x 0 ∣ y), HPow.hPow (β := ℕ) x 0 ∣ x
neg₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 ∣ y), HPow.hPow (β := ℕ) x 1 ∣ x
⊢ x ^ n ∣ x

Tactic:
rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl

Premises used: Squarefree.eq_zero_or_one_of_pow_of_not_isUnit, Squarefree.squarefree_of_dvd, rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
hx : Squarefree y
hu : ¬IsUnit x
h : HPow.hPow (β := ℕ) x 0 ∣ y
⊢ HPow.hPow (β := ℕ) x 0 ∣ x

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
hx : Squarefree y
hu : ¬IsUnit x
h : HPow.hPow (β := ℕ) x 1 ∣ y
⊢ HPow.hPow (β := ℕ) x 1 ∣ x

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hb : Squarefree b
⊢ Squarefree (@gcd _ inst _ a b)

Tactic:
hb.squarefree_of_dvd (gcd_dvd_right _ _)

Premises used: Squarefree.squarefree_of_dvd, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
ha : Squarefree a
⊢ Squarefree (@gcd _ inst _ a b)

Tactic:
ha.squarefree_of_dvd (gcd_dvd_left _ _)

Premises used: Squarefree.squarefree_of_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
r : R
⊢ Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x

Tactic:
forall_congr' fun a => ?_

Premises used: forall_congr', Squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
r : R
refine : ∀ (a : R), a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a
⊢ Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x

Tactic:
refine forall_congr' fun a => ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
r a : R
rw : (↑2 : ℕ∞) ≤ emultiplicity a r ↔ 1 < emultiplicity a r
⊢ a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a

Tactic:
rw [← sq, pow_dvd_iff_le_emultiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]

Premises used: not_le, Iff.rfl, sq, pow_dvd_iff_le_emultiplicity, Classical.or_iff_not_imp_left, imp_congr
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
r a : R
⊢ ¬IsMax (α := ℕ∞) 1

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
r a : R
⊢ HAdd.hAdd (α := ℕ∞) 1 1 ≤ emultiplicity a r ↔ 1 < emultiplicity a r

Tactic:
exact Order.add_one_le_iff_of_not_isMax (by simp)

Premises used: Order.add_one_le_iff_of_not_isMax
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩

Premises used: Irreducible.not_isUnit, Iff.intro, by_contra
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
refine : ∀ (h : ∀ (p : R), Irreducible p → ¬p * p ∣ x) (d : R) (hd : d * d ∣ x) (hdu : ¬IsUnit d), False
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
refine ⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
⊢ d ≠ 0

Tactic:
have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
obtain : ∀ (p : R) (irr : Irreducible p) (dvd : p ∣ d), False
⊢ False

Tactic:
obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
p : R
irr : Irreducible p
dvd : p ∣ d
⊢ False

Tactic:
h p irr ((mul_dvd_mul dvd dvd).trans hd)

Premises used: mul_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
p : R
irr : Irreducible p
dvd : p ∣ d
⊢ False

Tactic:
exact h p irr ((mul_dvd_mul dvd dvd).trans hd)

Premises used: mul_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

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

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
refine_1 : ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ r), (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
refine_2 : (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
refine_1 :
  ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0),
    (Eq.{u_1 + 1} (α := R) 0 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree.{u_1} (R := R) 0
refine_1₁ : ∀ (hr : r ≠ 0), (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ Eq.{u_1 + 1} (α := R) 0 0 ∧ ∀ (x : R), ¬Irreducible x

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ (Eq.{u_1 + 1} (α := R) 0 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree.{u_1} (R := R) 0

Tactic:
exact .inl (by simpa using h)
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
.inr ((squarefree_iff_no_irreducibles hr).mpr h)

Premises used: Iff.mpr, squarefree_iff_no_irreducibles, Or.inr
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
exact .inr ((squarefree_iff_no_irreducibles hr).mpr h)
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ 0

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : Squarefree r
x : R
hx : Irreducible x
t : x * x ∣ r
⊢ False

Tactic:
hx.not_isUnit (h x t)

Premises used: Irreducible.not_isUnit
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : Squarefree r
x : R
hx : Irreducible x
t : x * x ∣ r
⊢ False

Tactic:
exact hx.not_isUnit (h x t)

Premises used: Irreducible.not_isUnit
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
simpa [hr] using (irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree r).symm

Premises used: irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, Iff.symm
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
hr : ∃ (x : R), Irreducible x
rw : Squarefree r ↔ (r = 0 ∧ ¬∃ (x : R), Irreducible x) ∨ Squarefree r
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]

Premises used: not_exists, irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
hr : ∃ (x : R), Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ (x : R), Irreducible x) ∨ Squarefree r

Tactic:
simp only [hr, not_true, false_or, and_false]

Premises used: false_or, not_true, and_false
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : DecompositionMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ HPow.hPow (β := ℕ) y 2
obtain :
  ∀ (a b : R) (ha : a ∣ y) (hb : b ∣ y) (hx : Squarefree (a * b)) (hy : a * b ∣ HPow.hPow (β := ℕ) y 2), a * b ∣ y
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)

Premises used: exists_dvd_and_dvd_of_dvd_mul, rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : DecompositionMonoid R
y a b : R
ha : a ∣ y
hb : b ∣ y
hx : Squarefree (a * b)
hy : a * b ∣ HPow.hPow (β := ℕ) y 2
⊢ a * b ∣ y

Tactic:
(IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

Premises used: IsRelPrime.mul_dvd, IsRelPrime.of_squarefree_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : DecompositionMonoid R
y a b : R
ha : a ∣ y
hb : b ∣ y
hx : Squarefree (a * b)
hy : a * b ∣ HPow.hPow (β := ℕ) y 2
⊢ a * b ∣ y

Tactic:
exact (IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

Premises used: IsRelPrime.mul_dvd, IsRelPrime.of_squarefree_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : DecompositionMonoid R
x y : R
n : ℕ
hsq : Squarefree x
h0 : n ≠ 0
⊢ x ∣ y ^ n ↔ x ∣ y

Tactic:
⟨hsq.isRadical n y, (·.pow h0)⟩

Premises used: Squarefree.isRadical, Dvd.dvd.pow, Iff.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
simp_rw : z * w * (z * w) = z * z * w * w
simp_rw₁ : z * (z * w * w) = z * z * w * w
⊢ HPow.hPow (β := ℕ) (z * w) 2 = z * z * w * w

Tactic:
simp_rw [pow_two, mul_left_comm, ← mul_assoc]

Premises used: pow_two, mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ z * z * w ∣ z * w

Tactic:
specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩

Premises used: HMul.hMul, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * z * w ∣ z * w
rwa : ∀ (h : z * (z * w) ∣ 1 * (z * w)), z * w ≠ 0
⊢ IsUnit z

Tactic:
rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h

Premises used: HMul.hMul, mul_dvd_mul_iff_right, mul_assoc, isUnit_iff_dvd_one, one_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z ≠ 0 ∧ z * w ≠ 0

Tactic:
rw [mul_assoc, mul_ne_zero_iff] at h0

Premises used: mul_assoc, mul_ne_zero_iff
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
h0₁ : z ≠ 0 ∧ z * w ≠ 0
⊢ z * (z * w) ∣ 1 * (z * w)

Tactic:
rw [mul_assoc, mul_ne_zero_iff] at h0

Premises used: mul_assoc, mul_ne_zero_iff
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
h0.2

Premises used: And.right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z ≠ 0 ∧ z * w ≠ 0
h : z * (z * w) ∣ 1 * (z * w)
⊢ z * w ≠ 0

Tactic:
exact h0.2

Premises used: And.right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
pos : ∀ (hxp : p ∣ x), p ^ k ∣ y
neg : ∀ (hxp : ¬p ∣ x), p ^ k ∣ y
⊢ p ^ k ∣ y

Tactic:
by_cases hxp : p ∣ x
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : p ∣ x
pos : ∀ (x' : R) (hx : Squarefree (p * x')) (h : p ^ (k + 1) ∣ p * x' * y), p ^ k ∣ y
⊢ p ^ k ∣ y

Tactic:
obtain ⟨x', rfl⟩ := hxp

Premises used: rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
⊢ ¬p ∣ x'

Tactic:
have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra)
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p * p ^ k ∣ p * (x' * y)

Tactic:
rw [pow_succ', mul_assoc] at h

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
h₁ : p * p ^ k ∣ p * (x' * y)
⊢ ¬p ∣ x'

Tactic:
rw [pow_succ', mul_assoc] at h

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
(mul_dvd_mul_iff_left hp.ne_zero).mp h

Premises used: mul_dvd_mul_iff_left, Prime.ne_zero, Iff.mp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p * p ^ k ∣ p * (x' * y)
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
exact (mul_dvd_mul_iff_left hp.ne_zero).mp h

Premises used: mul_dvd_mul_iff_left, Prime.ne_zero, Iff.mp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
replace h : p ^ k ∣ x' * y := by
      rw [pow_succ', mul_assoc] at h
      exact (mul_dvd_mul_iff_left hp.ne_zero).mp h
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
hx' : ¬p ∣ x'
h : p ^ k ∣ x' * y
⊢ p ^ k ∣ y

Tactic:
hp.pow_dvd_of_dvd_mul_left _ hx' h

Premises used: Prime.pow_dvd_of_dvd_mul_left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
hx' : ¬p ∣ x'
h : p ^ k ∣ x' * y
⊢ p ^ k ∣ y

Tactic:
exact hp.pow_dvd_of_dvd_mul_left _ hx' h

Premises used: Prime.pow_dvd_of_dvd_mul_left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : ¬p ∣ x
⊢ p ^ k ∣ y

Tactic:
(pow_dvd_pow _ k.le_succ).trans (hp.pow_dvd_of_dvd_mul_left _ hxp h)

Premises used: pow_dvd_pow, Nat.le_succ, Prime.pow_dvd_of_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
hxp : ¬p ∣ x
⊢ p ^ k ∣ y

Tactic:
exact (pow_dvd_pow _ k.le_succ).trans (hp.pow_dvd_of_dvd_mul_left _ hxp h)

Premises used: pow_dvd_pow, Nat.le_succ, Prime.pow_dvd_of_dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ x * y
⊢ p ^ (k + 1) ∣ y * x

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ y * x
⊢ p ^ k ∣ x

Tactic:
pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

Premises used: Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ y * x
⊢ p ^ k ∣ x

Tactic:
exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h

Premises used: Squarefree.pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
obtain : ∀ (a b : R) (ha : a ∣ x) (hb : b ∣ y) (eq : d * d = a * b), d ∣ y
⊢ d ∣ y

Tactic:
obtain ⟨a, b, ha, hb, eq⟩ := exists_dvd_and_dvd_of_dvd_mul h

Premises used: exists_dvd_and_dvd_of_dvd_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
ha : a ∣ x
hb : b ∣ y
eq : d * d = a * b
⊢ Squarefree a

Tactic:
replace ha : Squarefree a := hx.squarefree_of_dvd ha
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
rw : d * d = a * b
rw₁ rw₂ : a * b = a * b
⊢ HPow.hPow (β := ℕ) d 2 = a * b

Tactic:
rw [sq, eq]

Premises used: sq
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
obtain : ∀ (c : R) (hc : d = a * c), d ∣ y
⊢ d ∣ y

Tactic:
obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩

Premises used: Squarefree.isRadical, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
⊢ c * (a * c) = b

Tactic:
rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq

Premises used: mul_assoc, Function.Injective.eq_iff, mul_right_injective₀, Squarefree.ne_zero
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
c : R
hc : d = a * c
eq₁ : c * (a * c) = b
⊢ d = a * c

Tactic:
rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq

Premises used: mul_assoc, Function.Injective.eq_iff, mul_right_injective₀, Squarefree.ne_zero
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y d : R
inst_2 : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
h_1 : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
rw : b = a * c * c
rw₁ : c * (a * c) = a * c * c
rw₂ rw₃ : a * c * c = a * c * c
⊢ b = d * c

Tactic:
rw [hc, ← eq, mul_comm]

Premises used: mul_comm