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