n : ℕ
⊢ MinSqFacProp n (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else minSqFacAux (n / 2) 3 else minSqFacAux n 3)
n : ℕ
⊢ MinSqFacProp n (minSqFac n)
dsimp only [minSqFac]
case inl.inl
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ MinSqFacProp n (some 2)

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

case inr
n : ℕ
d2 : ¬2 ∣ n
⊢ MinSqFacProp n (minSqFacAux n 3)
n : ℕ
⊢ MinSqFacProp n (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else minSqFacAux (n / 2) 3 else minSqFacAux n 3)
split_ifs with d2 d4
no goals
case inl.inl
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ MinSqFacProp n (some 2)
exact ⟨prime_two, (dvd_div_iff d2).1 d4, fun p pp _ => pp.two_le⟩
case inl.inr.inl
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)

case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
case inl.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
cases' Nat.eq_zero_or_pos n with n0 n0
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp (n / 2) (minSqFacAux (n / 2) 3)
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
refine' minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff d2).2 d4) _
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp (n / 2) (minSqFacAux (n / 2) 3)
refine' minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl _
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
refine' fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le _)
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p
rintro rfl
no goals
case inl.inr.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False
contradiction
case inl.inr.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 (minSqFacAux (0 / 2) 3)
case inl.inr.inl
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
subst n0
no goals
case inl.inr.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 (minSqFacAux (0 / 2) 3)
cases d4 (by decide)
no goals
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ 2 ∣ 0 / 2
decide
no goals
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ 0 < 2
decide
case inr.inl
n : ℕ
d2 : ¬2 ∣ n
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux n 3)

case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux n 3)
case inr
n : ℕ
d2 : ¬2 ∣ n
⊢ MinSqFacProp n (minSqFacAux n 3)
cases' Nat.eq_zero_or_pos n with n0 n0
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux n 3)
refine' minSqFacAux_has_prop _ n0 0 rfl _
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
refine' fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le _)
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p
rintro rfl
no goals
case inr.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False
contradiction
case inr.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)
case inr.inl
n : ℕ
d2 : ¬2 ∣ n
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux n 3)
subst n0
no goals
case inr.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)
cases d2 (by decide)
no goals
d2 : ¬2 ∣ 0
⊢ 2 ∣ 0
decide