Theorem: Sieve.Nat.squarefree_dvd_pow (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
⊢ a ∣ b
Tactic:
by_cases hN : N=0
State after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : N = 0
⊢ a ∣ b

case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : ¬N = 0
⊢ a ∣ b

State before:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : ¬N = 0
⊢ a ∣ b
Tactic:
rw [Squarefree.dvd_pow_iff_dvd ha hN] at hab
State after:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b
hN : ¬N = 0
⊢ a ∣ b

State before:
case neg
a b N : ℕ
ha : Squarefree a
hab : a ∣ b
hN : ¬N = 0
⊢ a ∣ b
Tactic:
exact hab
State after:
no goals

State before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a ∣ b ^ N
hN : N = 0
⊢ a ∣ b
Tactic:
rw [hN, pow_zero, Nat.dvd_one] at hab
State after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ a ∣ b

State before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ a ∣ b
Tactic:
rw [hab]
State after:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ 1 ∣ b

State before:
case pos
a b N : ℕ
ha : Squarefree a
hab : a = 1
hN : N = 0
⊢ 1 ∣ b
Tactic:
simp
State after:
no goals