awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ d ∣ y

Tactic:
exact dvd_trans ⟨c, by rw [hc, ← eq, mul_comm]⟩ hb

Premises used: dvd_trans, Exists.intro
-- 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
hy : Squarefree y
h : d * d ∣ x * y
⊢ d ∣ x

Tactic:
dvd_of_squarefree_of_mul_dvd_mul_right hy (mul_comm x y ▸ h)

Premises used: Eq.rec, Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right, mul_comm
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y : R
inst_2 : DecompositionMonoid R
⊢ Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y

Tactic:
⟨fun h ↦ ⟨IsRelPrime.of_squarefree_mul h, h.of_mul_left, h.of_mul_right⟩,
    fun ⟨hp, sqx, sqy⟩ _ dvd ↦ hp (sqy.dvd_of_squarefree_of_mul_dvd_mul_left dvd)
      (sqx.dvd_of_squarefree_of_mul_dvd_mul_right dvd)⟩

Premises used: Squarefree.of_mul_left, IsUnit, _private.0.squarefree_mul_iff.match_1, Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left, Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right, And.intro, Iff.intro, Squarefree.of_mul_right, IsRelPrime.of_squarefree_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
hs : (↑∅ : Set ι).Pairwise (IsRelPrime on f)
hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Squarefree (f i)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ ∅, f i)

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ Finset.cons a s ha, Squarefree (f i)
cons : IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ Finset.cons a s ha, f i)

Tactic:
rw [Finset.prod_cons, squarefree_mul_iff]

Premises used: squarefree_mul_iff, Finset.prod_cons
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑(cons a s ha) : Set ι).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a

Tactic:
rw [Finset.coe_cons, Set.pairwise_insert] at hs

Premises used: Finset.coe_cons, Set.pairwise_insert
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑(cons a s ha) : Set ι).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
hs₁ :
  (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
⊢ ∀ i ∈ cons a s ha, Squarefree (f i)

Tactic:
rw [Finset.coe_cons, Set.pairwise_insert] at hs

Premises used: Finset.coe_cons, Set.pairwise_insert
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ a ∈ cons a s ha

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ Finset.cons a s ha, Squarefree (f i)
cons : ∀ (i : ι) (hi : i ∈ s), IsRelPrime (f a) (f i)
cons₁ : Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)

Tactic:
refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
i : ι
hi : i ∈ s
⊢ i ∈ (↑s : Set ι)

Tactic:
simp [hi]
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
i : ι
hi : i ∈ s
⊢ IsRelPrime (f a) (f i)

Tactic:
exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left

Premises used: Eq.rec, And.right, And.left, Eq.symm
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)

Tactic:
ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

Premises used: Finset.mem_cons_of_mem, And.left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
    Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
hs : (↑s : Set ι).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ (↑s : Set ι), a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)

Tactic:
exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

Premises used: Finset.mem_cons_of_mem, And.left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
ι : Type u_2
s : Finset ι
f : ι → R
hs : (↑s : Set ι).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ s, Squarefree (f i)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise (IsRelPrime on f))
    (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Squarefree (f i)), Squarefree.{u_1} (R := R) (∏ i ∈ ∅, f i)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      ∀ (hs : (↑s : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ s, Squarefree (f i)),
        Squarefree.{u_1} (R := R) (∏ i ∈ s, f i))
    (hs : (↑(Finset.cons a s ha) : Set ι).Pairwise (IsRelPrime on f))
    (hs' : ∀ i ∈ Finset.cons a s ha, Squarefree (f i)), Squarefree.{u_1} (R := R) (∏ i ∈ Finset.cons a s ha, f i)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.prod_cons, squarefree_mul_iff]
    rw [Finset.coe_cons, Set.pairwise_insert] at hs
    refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
    · exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left
    · exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

Premises used: Finset.cons, Finset.coe_cons, Set.pairwise_insert, squarefree_mul_iff, Finset.prod_cons
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
rw : IsReduced R
⊢ IsRadical.{u_1} (R := R) 0

Tactic:
rw [zero_isRadical_iff]

Premises used: zero_isRadical_iff
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
⊢ IsReduced R

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x : R
inst_2 : DecompositionMonoid R
h : x ≠ 0
⊢ IsRadical x ↔ Squarefree x

Tactic:
⟨IsRadical.squarefree h, Squarefree.isRadical⟩

Premises used: Squarefree.isRadical, IsRadical.squarefree, Iff.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
hx : Ne.{u_1 + 1} (α := R) 0 0
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ 0 ∧ 0 ∣ y ^ n

Tactic:
contradiction
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
u : R
hu : IsUnit u
hx : u ≠ 0
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n

Tactic:
⟨1, 0, squarefree_one, one_dvd u, hu.dvd⟩

Premises used: squarefree_one, IsUnit.dvd, one_dvd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
u : R
hu : IsUnit u
hx : u ≠ 0
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n

Tactic:
exact ⟨1, 0, squarefree_one, one_dvd u, hu.dvd⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
mul :
  ∀ (y : R) (n : ℕ) (hy : Squarefree y) (hyx : y ∣ z) (hy' : z ∣ y ^ n),
    ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
mul : ∀ (hy' : z ∣ HPow.hPow (β := ℕ) y 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
mul₁ : ∀ (hn : n > 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ HPow.hPow (β := ℕ) y 0
⊢ p * z ∣ HPow.hPow (β := ℕ) p 1

Tactic:
simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]

Premises used: isUnit_of_dvd_one
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ HPow.hPow (β := ℕ) y 0
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
exact ⟨p, 1, hp.squarefree, dvd_mul_right p z, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
pos : ∀ (hp' : p ∣ y), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
neg : ∀ (hp' : ¬p ∣ y), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
by_cases hp' : p ∣ y
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : p ∣ y
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
        mul_comm p z ▸ pow_succ y n ▸ mul_dvd_mul hy' hp'⟩

Premises used: dvd_mul_of_dvd_right, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : p ∣ y
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
exact ⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
        mul_comm p z ▸ pow_succ y n ▸ mul_dvd_mul hy' hp'⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : ¬p ∣ y
neg : Squarefree (p * y)
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
suffices Squarefree (p * y) from ⟨p * y, n, this,
        mul_dvd_mul_left p hyx, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : ¬p ∣ y
⊢ Squarefree (p * y)

Tactic:
squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Premises used: Iff.mpr, Irreducible.isRelPrime_iff_not_dvd, Irreducible.squarefree, squarefree_mul_iff, And.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
n : ℕ
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ n
hn : n > 0
hp' : ¬p ∣ y
⊢ Squarefree (p * y)

Tactic:
exact squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Premises used: Iff.mpr, Irreducible.isRelPrime_iff_not_dvd, Irreducible.squarefree, squarefree_mul_iff, And.intro
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
x : R
hx : x ≠ 0
zero : ∀ (hx : Ne.{u_1 + 1} (α := R) 0 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ 0 ∧ 0 ∣ y ^ n
unit : ∀ (u : R) (hu : IsUnit u) (hx : u ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n
mul :
  ∀ (z p : R) (hz : z ≠ 0) (hp : Irreducible p)
    (ih : ∀ (hx : z ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n) (hx : p * z ≠ 0),
    ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

Tactic:
induction x using WfDvdMonoid.induction_on_irreducible with
  | zero => contradiction
  | unit u hu => exact ⟨1, 0, squarefree_one, one_dvd u, hu.dvd⟩
  | mul z p hz hp ih =>
    obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
    rcases n.eq_zero_or_pos with rfl | hn
    · exact ⟨p, 1, hp.squarefree, dvd_mul_right p z, by simp [isUnit_of_dvd_one (pow_zero y ▸ hy')]⟩
    by_cases hp' : p ∣ y
    · exact ⟨y, n + 1, hy, dvd_mul_of_dvd_right hyx _,
        mul_comm p z ▸ pow_succ y n ▸ mul_dvd_mul hy' hp'⟩
    · suffices Squarefree (p * y) from ⟨p * y, n, this,
        mul_dvd_mul_left p hyx, mul_pow p y n ▸ mul_dvd_mul (dvd_pow_self p hn.ne') hy'⟩
      exact squarefree_mul_iff.mpr ⟨hp.isRelPrime_iff_not_dvd.mpr hp', hp.squarefree, hy⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
⊢ Squarefree x ↔ (normalizedFactors x).Nodup

Tactic:
rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]

Premises used: Multiset.nodup_iff_count_le_one, squarefree_iff_emultiplicity_le_one
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_ne x 0 x0
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
mp : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) → ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
mpr : (∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1) → ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
constructor
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
pos : ∀ (hmem : a ∈ normalizedFactors x), Multiset.count a (normalizedFactors x) ≤ 1
neg : ∀ (hmem : a ∉ normalizedFactors x), Multiset.count a (normalizedFactors x) ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
by_cases hmem : a ∈ normalizedFactors x

Premises used: UniqueFactorizationMonoid.normalizedFactors
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
⊢ Irreducible a

Tactic:
have ha := irreducible_of_normalized_factor _ hmem
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
pos : ∀ (h : emultiplicity a x ≤ 1), Multiset.count a (normalizedFactors x) ≤ 1
pos₁ : ∀ (h : IsUnit a), Multiset.count a (normalizedFactors x) ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
rcases h a with (h | h)
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
pos : Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
rw [← normalize_normalized_factor _ hmem]

Premises used: UniqueFactorizationMonoid.normalize_normalized_factor
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : emultiplicity a x ≤ 1
⊢ LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x)) : ℕ∞) 1

Tactic:
rw [emultiplicity_eq_count_normalizedFactors ha x0] at h

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x)) : ℕ∞) 1
pos pos₁ pos₂ pos₃ :
  ∀ (h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1)
    (h : Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1),
    Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1
⊢ Multiset.count ((normalize : (a : R) → R) a) (normalizedFactors x) ≤ 1

Tactic:
assumption_mod_cast
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
⊢ ¬IsUnit a

Tactic:
have := ha.1
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this_1 : Nontrivial R
h_1 : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : IsUnit a
this : ¬IsUnit a
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
contradiction
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∉ normalizedFactors x
⊢ Multiset.count a (normalizedFactors x) ≤ 1

Tactic:
simp [Multiset.count_eq_zero_of_notMem hmem]

Premises used: Multiset.count_eq_zero_of_notMem
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
mpr : ¬IsUnit a → emultiplicity a x ≤ 1
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
mpr : ∀ (hu : ¬IsUnit.{u_1} (M := R) 0), emultiplicity 0 x ≤ 1
mpr₁ : ∀ (h0 : a ≠ 0), emultiplicity a x ≤ 1
⊢ emultiplicity a x ≤ 1

Tactic:
rcases eq_or_ne a 0 with rfl | h0

Premises used: eq_or_ne, OfNat.ofNat, rfl