-- Mathlib/Algebra/Squarefree/Basic.lean
theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree (r : R) :
    (∀ x : R, Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ x : R, ¬Irreducible x) ∨ Squarefree r

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

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

Result:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r

Proof state:
case refine_2.inl.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ 0 = 0 ∧ ∀ (x : R), ¬Irreducible x

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_1.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : 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)

Result:
no goals

Proof state:
case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
intro x hx t

Result:
case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
x : R
hx : Irreducible x
t : x * x ∣ r
⊢ False

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
rintro (⟨rfl, h⟩ | h)

Result:
case refine_2.inl.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), ¬Irreducible x
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ 0

case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
⊢ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Proof state:
case refine_1.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ (0 = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree 0

Tactic:
exact .inl (by simpa using h)

Result:
no goals

Proof state:
case refine_2.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : Squarefree r
x : R
hx : Irreducible x
t : x * x ∣ r
⊢ False

Tactic:
exact hx.not_unit (h x t)

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

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

Result:
case refine_1.inl
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ (0 = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree 0

case refine_1.inr
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
hr : r ≠ 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r