n : ℕ
this : MinSqFacProp n (minSqFac n)
⊢ Squarefree n ↔ minSqFac n = none
n : ℕ
⊢ Squarefree n ↔ minSqFac n = none
have := minSqFac_has_prop n
case mp
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
⊢ minSqFac n = none

case mpr
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : minSqFac n = none
⊢ Squarefree n
n : ℕ
this : MinSqFacProp n (minSqFac n)
⊢ Squarefree n ↔ minSqFac n = none
constructor <;> intro H
case mp.none
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
e : minSqFac n = none
⊢ none = none

case mp.some
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
d : ℕ
e : minSqFac n = some d
⊢ some d = none
case mp
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
⊢ minSqFac n = none
cases' e : n.minSqFac with d
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : MinSqFacProp n (some d)
e : minSqFac n = some d
⊢ some d = none
case mp.some
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
d : ℕ
e : minSqFac n = some d
⊢ some d = none
rw [e] at this
no goals
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : MinSqFacProp n (some d)
e : minSqFac n = some d
⊢ some d = none
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1
no goals
case mp.none
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
e : minSqFac n = none
⊢ none = none
rfl
no goals
case mpr
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : minSqFac n = none
⊢ Squarefree n
rwa [H] at this