n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (minSqFac n)
⊢ Prime d
n d : ℕ
h : minSqFac n = some d
⊢ Prime d
have := minSqFac_has_prop n
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (some d)
⊢ Prime d
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (minSqFac n)
⊢ Prime d
rw [h] at this
no goals
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (some d)
⊢ Prime d
exact this.1