n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (minSqFac n)
⊢ d ≤ m
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ d ≤ m
have := minSqFac_has_prop n
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
⊢ d ≤ m
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (minSqFac n)
⊢ d ≤ m
rw [h] at this
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
fd : minFac m ∣ m
⊢ d ≤ m
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
⊢ d ≤ m
have fd := minFac_dvd m
no goals
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
fd : minFac m ∣ m
⊢ d ≤ m
exact
  le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
    (minFac_le <| lt_of_lt_of_le (by decide) m2)
no goals
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
fd : minFac m ∣ m
⊢ 0 < 2
decide