awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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)
⊢ IsUnit z
have h₁ : z * z * w ∣ z * w
Tactic: specialize h 2 (z * w) ⟨w, by simp_rw [pow_two, mul_left_comm, ← mul_assoc]⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ IsUnit z
have rwa : ∀ (h : z * (z * w) ∣ 1 * (z * w)), z * w ≠ 0
Tactic: rwa [← one_mul (z * w), mul_assoc, mul_dvd_mul_iff_right, ← isUnit_iff_dvd_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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 * w ≠ 0
have h0₁ : z ≠ 0 ∧ z * w ≠ 0
Tactic: rw [mul_assoc, mul_ne_zero_iff] at h0
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ p ^ k ∣ y
have pos : ∀ (hxp : p ∣ x), p ^ k ∣ y
Tactic: by_cases hxp : p ∣ x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ p ^ k ∣ y
have neg : ∀ (hxp : ¬p ∣ x), p ^ k ∣ y
Tactic: by_cases hxp : p ∣ x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
have pos : ∀ (x' : R) (hx : Squarefree (p * x')) (h : p ^ (k + 1) ∣ p * x' * y), p ^ k ∣ y
Tactic: obtain ⟨x', rfl⟩ := hxp
Cleared hypotheses: x, hx, h, hxp
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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 ^ k ∣ y
have hx' : ¬p ∣ x'
Tactic: have hx' : ¬ p ∣ x' := fun contra ↦ hp.not_unit <| hx p (mul_dvd_mul_left p contra)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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
have h₁ : p * p ^ k ∣ p * (x' * y)
Tactic: rw [pow_succ', mul_assoc] at h
Cleared hypotheses: h, hx'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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 ∣ y
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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 ∣ x
have h₁ : p ^ (k + 1) ∣ y * x
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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
⊢ d ∣ y
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ d ∣ y
have obtain : ∀ (a b : R) (ha : a ∣ x) (hb : b ∣ y) (eq : d * d = a * b), d ∣ y
Tactic: obtain ⟨a, b, ha, hb, eq⟩ := exists_dvd_and_dvd_of_dvd_mul h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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
⊢ d ∣ y
have ha₁ : Squarefree a
Tactic: replace ha : Squarefree a := hx.squarefree_of_dvd ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) d 2 = a * b
have rw₁ : a * b = a * b
Tactic: rw [sq, eq]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ d ∣ y
have obtain : ∀ (c : R) (hc : d = a * c), d ∣ y
Tactic: obtain ⟨c, hc⟩ : a ∣ d := ha.isRadical 2 d ⟨b, by rw [sq, eq]⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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
⊢ d ∣ y
have eq₁ : c * (a * c) = b
Tactic: rw [hc, mul_assoc, (mul_right_injective₀ ha.ne_zero).eq_iff] at eq
Cleared hypotheses: eq, hc
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ b = d * c
have rw : b = a * c * c
Tactic: rw [hc, ← eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ b = d * c
have rw₁ : c * (a * c) = a * c * c
Tactic: rw [hc, ← eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ b = d * c
have rw₂ : a * c * c = a * c * c
Tactic: rw [hc, ← eq, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ cons a s ha, f i)
have cons : IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
Tactic: rw [Finset.prod_cons, squarefree_mul_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
have hs₁ : (↑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
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
have cons : ∀ (i : ι) (hi : i ∈ s), IsRelPrime (f a) (f i)
Tactic: refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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)
⊢ IsRelPrime (f a) (∏ x ∈ s, f x) ∧ Squarefree (f a) ∧ Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
have cons₁ : Squarefree.{u_1} (R := R) (∏ x ∈ s, f x)
Tactic: refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
have empty : ∀ (hs : (↑∅ : Set ι).Pairwise (IsRelPrime on f))
  (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Squarefree (f i)), Squarefree.{u_1} (R := R) (∏ i ∈ ∅, 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
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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)
⊢ Squarefree.{u_1} (R := R) (∏ i ∈ s, f i)
have 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 : (↑(cons a s ha) : Set ι).Pairwise (IsRelPrime on f)) (hs' : ∀ i ∈ cons a s ha, Squarefree (f i)),
  Squarefree.{u_1} (R := R) (∏ i ∈ cons a s ha, 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
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
inst_2 : DecompositionMonoid R
⊢ IsRadical.{u_1} (R := R) 0
have rw : IsReduced R
Tactic: rw [zero_isRadical_iff]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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 : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
have 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
Tactic: obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
have mul : ∀ (hy' : z ∣ HPow.hPow (β := ℕ) y 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n, hy'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
have mul₁ : ∀ (hn : n > 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
have pos : ∀ (hp' : p ∣ y), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
Tactic: by_cases hp' : p ∣ y
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
have neg : ∀ (hp' : ¬p ∣ y), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n
Tactic: by_cases hp' : p ∣ y
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
have neg : Squarefree (p * y)
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'⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
x : R
hx : x ≠ 0
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
have zero : ∀ (hx : Ne.{u_1 + 1} (α := R) 0 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ 0 ∧ 0 ∣ 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⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
have unit : ∀ (u : R) (hu : IsUnit u) (hx : u ≠ 0), ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ u ∧ u ∣ 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⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
have 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
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⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ Squarefree x ↔ (normalizedFactors x).Nodup
have rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
have this : Nontrivial R
Tactic: haveI := nontrivial_of_ne x 0 x0
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
have mp : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) → ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
have mpr : (∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1) → ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have pos : ∀ (hmem : a ∈ normalizedFactors x), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: by_cases hmem : a ∈ normalizedFactors x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have neg : ∀ (hmem : a ∉ normalizedFactors x), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: by_cases hmem : a ∈ normalizedFactors x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
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
have ha : Irreducible a
Tactic: have ha := irreducible_of_normalized_factor _ hmem
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have pos : ∀ (h : emultiplicity a x ≤ 1), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: rcases h a with (h | h)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
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
⊢ Multiset.count a (normalizedFactors x) ≤ 1
have pos₁ : ∀ (h : IsUnit a), Multiset.count a (normalizedFactors x) ≤ 1
Tactic: rcases h a with (h | h)