-- Mathlib/Algebra/Squarefree/Basic.lean
lemma _root_.exists_squarefree_dvd_pow_of_ne_zero {x : R} (hx : x ≠ 0) :
    ∃ (y : R) (n : ℕ), Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

Proof state:
case hi.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Result:
case hi.intro.intro.intro.intro.inl
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

case hi.intro.intro.intro.intro.inr
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Proof state:
case pos
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 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'⟩

Result:
no goals

Proof state:
case hu
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
u : R
hu : IsUnit u
hx : u ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n

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

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 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'⟩

Result:
case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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)

Proof state:
case hi.intro.intro.intro.intro.inr
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
by_cases hp' : p ∣ y

Result:
case pos
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Proof state:
case hi
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Tactic:
obtain ⟨y, n, hy, hyx, hy'⟩ := ih hz

Result:
case hi.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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 n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Proof state:
case hi.intro.intro.intro.intro.inl
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ ∃ y 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')]⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x : R
hx : x ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

Tactic:
induction' x using WfDvdMonoid.induction_on_irreducible with u hu z p hz hp ih

Result:
case h0
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
hx : 0 ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ 0 ∧ 0 ∣ y ^ n

case hu
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
u : R
hu : IsUnit u
hx : u ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ u ∧ u ∣ y ^ n

case hi
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ p * z ∧ p * z ∣ y ^ n

Proof state:
case h0
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
hx : 0 ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ 0 ∧ 0 ∣ y ^ n

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ p * z ∣ p ^ 1

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

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y 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⟩

Result:
no goals