n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
⊢ MinSqFacProp n o
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
⊢ MinSqFacProp n o
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
  have :=
    (coprime_primes pk pp).2 fun e => by
      subst e
      contradiction
  (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : MinSqFacProp (n / k) none
⊢ MinSqFacProp n none

case some
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : MinSqFacProp (n / k) (some d)
⊢ MinSqFacProp n (some d)
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
⊢ MinSqFacProp n o
cases' o with d
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
pp : Prime k
dp : k * k ∣ n
⊢ False
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
p : ℕ
pp : Prime p
dp : p * p ∣ n
e : k = p
⊢ False
subst e
no goals
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
pp : Prime k
dp : k * k ∣ n
⊢ False
contradiction
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H :
  match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
  | some d => Prime d ∧ d * d ∣ n / k ∧ ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n
  | some d => Prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), Prime p → p * p ∣ n → d ≤ p
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : MinSqFacProp (n / k) none
⊢ MinSqFacProp n none
rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H⊢
no goals
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H :
  match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
  | some d => Prime d ∧ d * d ∣ n / k ∧ ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n
  | some d => Prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), Prime p → p * p ∣ n → d ≤ p
exact fun p pp dp => H p pp ((dvd_div_iff dk).2 (this _ pp dp))
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : d * d ∣ n / k
H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ MinSqFacProp n (some d)
case some
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : MinSqFacProp (n / k) (some d)
⊢ MinSqFacProp n (some d)
obtain ⟨H1, H2, H3⟩ := H
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ MinSqFacProp n (some d)
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : d * d ∣ n / k
H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ MinSqFacProp n (some d)
simp only [dvd_div_iff dk] at H2 H3
no goals
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ MinSqFacProp n (some d)
exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩