-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_pow_right_dvd_pow_gcd [GCDMonoid α] {a b : α} {k : ℕ} :
    gcd a (b ^ k) ∣ gcd a b ^ k

Proof state:
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 ^ (k + 1)) ∣ gcd a b ^ (k + 1)

Tactic:
rw [pow_succ', pow_succ']

Result:
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

Proof state:
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

Tactic:
rw [gcd_eq_zero_iff] at hg

Result:
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

Proof state:
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1

Tactic:
exact (gcd_one_right' a).dvd

Result:
no goals

Proof state:
α : 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

Tactic:
exact (mul_dvd_mul_iff_left hg).mpr hk

Result:
no goals

Proof state:
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k : ℕ
⊢ gcd 0 (0 ^ k) ∣ gcd 0 0 ^ k

Tactic:
exact
  (gcd_zero_left' (0 ^ k : α)).dvd.trans
    (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)

Result:
no goals

Proof state:
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

Tactic:
trans gcd a b * gcd a (b ^ k)

Result:
α : 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

Proof state:
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a (b ^ 0) ∣ gcd a b ^ 0

Tactic:
rw [pow_zero, pow_zero]

Result:
case neg.zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ 1

Proof state:
α : 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)

Tactic:
exact gcd_mul_dvd_mul_gcd a b (b ^ k)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
by_cases hg : gcd a b = 0

Result:
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

Proof state:
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

Tactic:
rcases hg with ⟨rfl, rfl⟩

Result:
case pos.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
k : ℕ
⊢ gcd 0 (0 ^ k) ∣ gcd 0 0 ^ k