case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1
case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)
congr
no goals
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))