α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
⊢ Finite a b ↔ a ≠ 1 ∧ 0 < b
rw [← not_iff_not, not_finite_iff_forall, not_and_or, Ne.def, Classical.not_not, not_lt,
  le_zero_iff]
no goals
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
⊢ (∀ (n : ℕ), a ^ n ∣ b) ↔ a = 1 ∨ b = 0
exact
  ⟨fun h =>
    or_iff_not_imp_right.2 fun hb =>
      have ha : a ≠ 0 := fun ha => hb <| zero_dvd_iff.mp <| by rw [ha] at h; exact h 1
      Classical.by_contradiction fun ha1 : a ≠ 1 =>
        have ha_gt_one : 1 < a :=
          lt_of_not_ge fun _ =>
            match a with
            | 0 => ha rfl
            | 1 => ha1 rfl
            | b+2 => by linarith
        not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero hb) (h b)) (lt_pow_self ha_gt_one b),
    fun h => by cases h <;> simp [*]⟩
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
rw [ha] at h
no goals
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
exact h 1
no goals
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : 1 ≥ b + 2
⊢ False
linarith
no goals
α : Type ?u.1244493
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
cases h <;> simp [*]