-- Mathlib/Data/Nat/Squarefree.lean
theorem minSqFac_has_prop (n : ℕ) : MinSqFacProp n (minSqFac n)

Proof state:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
refine minSqFacAux_has_prop _ n0 0 rfl ?_

Result:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m

Proof state:
case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with n0 | n0

Result:
case neg.inl
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n = 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Proof state:
case neg.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 ((0 / 2).minSqFacAux 3)

Tactic:
cases d4 (by decide)

Result:
no goals

Proof state:
case pos
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

Tactic:
exact ⟨prime_two, (dvd_div_iff_mul_dvd d2).1 d4, fun p pp _ => pp.two_le⟩

Result:
no goals

Proof state:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case neg.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)

Tactic:
cases d2 (by decide)

Result:
no goals

Proof state:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Result:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p

Proof state:
case neg.inl
n : ℕ
d2 : ¬2 ∣ n
n0 : n = 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
subst n0

Result:
case neg.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)

Proof state:
case neg.inl
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n = 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
subst n0

Result:
case neg.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 ((0 / 2).minSqFacAux 3)

Proof state:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p

Tactic:
rintro rfl

Result:
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False

Proof state:
d2 : ¬2 ∣ 0
⊢ 2 ∣ 0

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)

Tactic:
split_ifs with d2 d4

Result:
case pos
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ n.MinSqFacProp (some 2)

case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Proof state:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p

Tactic:
rintro rfl

Result:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False

Proof state:
n : ℕ
⊢ n.MinSqFacProp n.minSqFac

Tactic:
dsimp only [minSqFac]

Result:
n : ℕ
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)

Proof state:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m

Tactic:
refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)

Result:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p

Proof state:
case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with n0 | n0

Result:
case neg.inl
n : ℕ
d2 : ¬2 ∣ n
n0 : n = 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)

case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Proof state:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
refine minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl ?_

Result:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m

Proof state:
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ 2 ∣ 0 / 2

Tactic:
decide

Result:
no goals

Proof state:
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ n.MinSqFacProp ((n / 2).minSqFacAux 3)

Tactic:
refine minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff_mul_dvd d2).2 d4) ?_

Result:
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ (n / 2).MinSqFacProp ((n / 2).minSqFacAux 3)