case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : ¬gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
by_cases hg : gcd a b = 0
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : a = 0 ∧ b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
rw [gcd_eq_zero_iff] at hg
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k : ℕ
⊢ gcd 0 (0 ^ k) ∣ gcd 0 0 ^ k
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : a = 0 ∧ b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
rcases hg with ⟨rfl, rfl⟩
no goals
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k : ℕ
⊢ gcd 0 (0 ^ k) ∣ gcd 0 0 ^ k
exact
  (gcd_zero_left' (0 ^ k : α)).dvd.trans
    (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a (b ^ Nat.zero) ∣ gcd a b ^ Nat.zero

case neg.succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b ^ Nat.succ k) ∣ gcd a b ^ Nat.succ k
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : ¬gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
induction' k with k hk
case neg.succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a b ^ k
case neg.succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b ^ Nat.succ k) ∣ gcd a b ^ Nat.succ k
rw [pow_succ, pow_succ]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a (b ^ k)

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a b * gcd a (b ^ k) ∣ gcd a b * gcd a b ^ k
case neg.succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a b ^ k
trans gcd a b * gcd a (b ^ k)
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a (b ^ Nat.zero) ∣ gcd a b ^ Nat.zero
rw [pow_zero, pow_zero]
no goals
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1
exact (gcd_one_right' a).dvd
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a (b * b ^ k) ∣ gcd a b * gcd a (b ^ k)
exact gcd_mul_dvd_mul_gcd a b (b ^ k)
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
k : ℕ
hk : gcd a (b ^ k) ∣ gcd a b ^ k
⊢ gcd a b * gcd a (b ^ k) ∣ gcd a b * gcd a b ^ k
exact (mul_dvd_mul_iff_left hg).mpr hk