-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem pow_dvd_of_mul_eq_pow [GCDMonoid α] {a b c d₁ d₂ : α} (ha : a ≠ 0) (hab : IsUnit (gcd a b))
    {k : ℕ} (h : a * b = c ^ k) (hc : c = d₁ * d₂) (hd₁ : d₁ ∣ a) : d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ∣ a

Tactic:
apply (dvd_gcd_mul_of_dvd_mul h2).trans

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ gcd (d₁ ^ k) b * a ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ gcd (d₁ ^ k) b * a ∣ a

Tactic:
rw [h1.mul_left_dvd]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0

Tactic:
intro hdk

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
⊢ False

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : 0 ∣ a
hdk : d₁ ^ k = 0
⊢ False

Tactic:
apply absurd (zero_dvd_iff.mp h3) ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ∣ gcd a b

Tactic:
apply gcd_dvd_gcd hd₁ (dvd_refl b)

Result:
no goals

Proof state:
case hu.a.h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ∣ 1

Tactic:
apply dvd_trans _ hab.dvd

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ∣ gcd a b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd (d₁ ^ k) b)

Tactic:
apply isUnit_of_dvd_one

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd (d₁ ^ k) b ∣ 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
have h2 : d₁ ^ k ∣ a * b := by
  use d₂ ^ k
  rw [h, hc]
  exact mul_pow d₁ d₂ k

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1

Tactic:
apply IsUnit.dvd

Result:
case hu
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b ^ k)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
have h4 : d₁ ^ k ≠ 0 := by
  intro hdk
  rw [hdk] at h3
  apply absurd (zero_dvd_iff.mp h3) ha

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
h4 : d₁ ^ k ≠ 0
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd (d₁ ^ k) b ∣ gcd d₁ b ^ k

Tactic:
exact gcd_pow_left_dvd_pow_gcd

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
rw [mul_comm] at h2

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ d₁ ^ k ∣ a * b

Tactic:
use d₂ ^ k

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ a * b = d₁ ^ k * d₂ ^ k

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
⊢ False

Tactic:
rw [hdk] at h3

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : 0 ∣ a
hdk : d₁ ^ k = 0
⊢ False

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ a * b = d₁ ^ k * d₂ ^ k

Tactic:
rw [h, hc]

Result:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k

Proof state:
case h
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd (d₁ ^ k) b ∣ 1

Tactic:
trans gcd d₁ b ^ k

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd (d₁ ^ k) b ∣ gcd d₁ b ^ k

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1