awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
hu : IsUnit (@gcd _ inst _ d₁ b)
⊢ IsUnit (@gcd _ inst _ d₁ b ^ k)

Tactic:
apply IsUnit.pow

Premises used: IsUnit.pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
hu : @gcd _ inst _ d₁ b ∣ 1
⊢ IsUnit (@gcd _ inst _ d₁ b)

Tactic:
apply isUnit_of_dvd_one

Premises used: isUnit_of_dvd_one
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
hu : @gcd _ inst _ a b ∣ 1
hu₁ : Dvd.dvd.{u_1} (α := α) 1 1
grw : α
hu₂ : Dvd.dvd.{u_1} (α := α) 1 1
grw₁ : α
⊢ @gcd _ inst _ d₁ b ∣ 1

Tactic:
grw [hd₁, hab.dvd]

Premises used: IsUnit.dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (@gcd _ inst _ (d₁ ^ k) b)

Tactic:
have h1 : IsUnit (gcd (d₁ ^ k) b) := by
    apply isUnit_of_dvd_one
    trans gcd d₁ b ^ k
    · exact gcd_pow_left_dvd_pow_gcd
    · apply IsUnit.dvd
      apply IsUnit.pow
      apply isUnit_of_dvd_one
      grw [hd₁, hab.dvd]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h₁ : a * b = d₁ ^ k * d₂ ^ k
⊢ d₁ ^ k ∣ a * b

Tactic:
use d₂ ^ k
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h₁ : (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k
⊢ a * b = d₁ ^ k * d₂ ^ k

Tactic:
rw [h, hc]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k

Tactic:
mul_pow d₁ d₂ k

Premises used: mul_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k

Tactic:
exact mul_pow d₁ d₂ k

Premises used: mul_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
⊢ d₁ ^ k ∣ a * b

Tactic:
have h2 : d₁ ^ k ∣ a * b := by
    use d₂ ^ k
    rw [h, hc]
    exact mul_pow d₁ d₂ k
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ∣ b * a

Tactic:
rw [mul_comm] at h2

Premises used: mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
apply : @gcd _ inst _ (d₁ ^ k) b * a ∣ a
⊢ d₁ ^ k ∣ a

Tactic:
apply (dvd_gcd_mul_of_dvd_mul h2).trans

Premises used: dvd_gcd_mul_of_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
rw rw₁ : a ∣ a
⊢ @gcd _ inst _ (d₁ ^ k) b * a ∣ a

Tactic:
rw [h1.mul_left_dvd]

Premises used: IsUnit.mul_left_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ∣ a

Tactic:
have h3 : d₁ ^ k ∣ a := by
    apply (dvd_gcd_mul_of_dvd_mul h2).trans
    rw [h1.mul_left_dvd]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
⊢ 0 ∣ a

Tactic:
rw [hdk] at h3
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
hdk : d₁ ^ k = 0
h3₁ : 0 ∣ a
⊢ d₁ ^ k = 0

Tactic:
rw [hdk] at h3
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (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

Premises used: zero_dvd_iff, absurd, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0

Tactic:
have h4 : d₁ ^ k ≠ 0 := by
    intro hdk
    rw [hdk] at h3
    apply absurd (zero_dvd_iff.mp h3) ha
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
h4 : d₁ ^ k ≠ 0
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
⟨h4, h3⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (@gcd _ inst _ (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
h4 : d₁ ^ k ≠ 0
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
exact ⟨h4, h3⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
inl : Subsingleton α → ∃ (d : α), Associated (d ^ k) a
inr : Nontrivial α → ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Subsingleton α
h₁ : Associated (HPow.hPow (α := α) 0 k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
use 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Subsingleton α
h₁ h₂ : Associated (HPow.hPow (α := α) 0 k) (HPow.hPow (α := α) 0 k)
⊢ Associated (HPow.hPow (α := α) 0 k) a

Tactic:
rw [Subsingleton.elim a (0 ^ k)]

Premises used: HPow.hPow, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
pos : ∀ (ha : a = 0), ∃ (d : α), Associated (d ^ k) a
neg : ∀ (ha : ¬a = 0), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
h₁ : Associated (HPow.hPow (α := α) 0 k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
use 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
h₁ : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), Associated (HPow.hPow (α := α) (β := ℕ) 0 0) a
h₂ : ∀ (hk : k ≠ 0), Associated (HPow.hPow (α := α) 0 k) a
⊢ Associated (HPow.hPow (α := α) 0 k) a

Tactic:
obtain rfl | hk := eq_or_ne k 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : a = 0
h : a * b = HPow.hPow (β := ℕ) c 0
⊢ Associated (HPow.hPow (α := α) (β := ℕ) 0 0) a

Tactic:
simp [ha] at h
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : a = 0
hk : k ≠ 0
h₁ : Associated (HPow.hPow (α := α) 0 k) 0
h₂ h₃ : Associated.{u_1} (M := α) 0 0
⊢ Associated (HPow.hPow (α := α) 0 k) a

Tactic:
rw [ha, zero_pow hk]

Premises used: zero_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
pos : ∀ (hb : b = 0), ∃ (d : α), Associated (d ^ k) a
neg : ∀ (hb : ¬b = 0), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
h₁ : Associated (HPow.hPow (α := α) 1 k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
use 1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
h₁ : Associated 1 a
⊢ Associated (HPow.hPow (α := α) 1 k) a

Tactic:
rw [one_pow]

Premises used: one_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
h₁ : Associated (@gcd _ inst _ a b) a
⊢ Associated 1 a

Tactic:
apply (associated_one_iff_isUnit.mpr hab).symm.trans

Premises used: Iff.mpr, associated_one_iff_isUnit, Associated.trans, Associated.symm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
h₁ : Associated (@gcd _ inst _ a 0) a
⊢ Associated (@gcd _ inst _ a b) a

Tactic:
rw [hb]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (@gcd _ inst _ a 0) a

Tactic:
gcd_zero_right' a

Premises used: gcd_zero_right'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : b = 0
⊢ Associated (@gcd _ inst _ a 0) a

Tactic:
exact gcd_zero_right' a

Premises used: gcd_zero_right'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
neg : ∀ (h : a * b = HPow.hPow (β := ℕ) c 0), ∃ (d : α), Associated (HPow.hPow (β := ℕ) d 0) a
neg₁ : ∀ (hk : k > 0), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
obtain rfl | hk := k.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = HPow.hPow (β := ℕ) c 0
h₁ : Associated (HPow.hPow (α := α) (β := ℕ) 1 0) a
⊢ ∃ (d : α), Associated (HPow.hPow (β := ℕ) d 0) a

Tactic:
use 1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = HPow.hPow (β := ℕ) c 0
h₁ : ∀ (h : a * b = 1), Associated 1 a
⊢ Associated (HPow.hPow (α := α) (β := ℕ) 1 0) a

Tactic:
rw [pow_zero] at h ⊢

Premises used: pow_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
h₁ : 1 * (↑(Units.mkOfMulEqOne a b h) : α) = a
⊢ Associated 1 a

Tactic:
use Units.mkOfMulEqOne _ _ h

Premises used: Units.mkOfMulEqOne
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
h : a * b = 1
h₁ : 1 * a = a
h₂ h₃ : a = a
⊢ 1 * (↑(Units.mkOfMulEqOne a b h) : α) = a

Tactic:
rw [Units.val_mkOfMulEqOne, one_mul]

Premises used: one_mul, Units.val_mkOfMulEqOne
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
rw : c ∣ c ^ k
⊢ c ∣ a * b

Tactic:
rw [h]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ c ^ k

Tactic:
dvd_pow_self _ hk.ne'

Premises used: dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ c ^ k

Tactic:
exact dvd_pow_self _ hk.ne'

Premises used: dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
⊢ c ∣ a * b

Tactic:
have hc : c ∣ a * b := by
    rw [h]
    exact dvd_pow_self _ hk.ne'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc : c ∣ a * b
neg : ∀ (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b) (hc : c = d₁ * d₂), ∃ (d : α), Associated (d ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
obtain ⟨d₁, d₂, hd₁, hd₂, hc⟩ := exists_dvd_and_dvd_of_dvd_mul hc

Premises used: exists_dvd_and_dvd_of_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
h₁ : Associated (d₁ ^ k) a
⊢ ∃ (d : α), Associated (d ^ k) a

Tactic:
use d₁
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
h₁ : ∀ (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
⊢ Associated (d₁ ^ k) a

Tactic:
obtain ⟨h0₁, ⟨a', ha'⟩⟩ := pow_dvd_of_mul_eq_pow ha hab h hc hd₁

Premises used: pow_dvd_of_mul_eq_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h₁ :
  ∀ (h : b * a = c ^ k),
    Nontrivial α →
      ∀ (ha : ¬a = 0) (hb : ¬b = 0) (hk : k > 0) (hc : c ∣ a * b) (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b)
        (hc : c = d₂ * d₁) (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
⊢ Associated (d₁ ^ k) a

Tactic:
rw [mul_comm] at h hc

Premises used: mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h₁ :
  ∀ (hab : IsUnit (@gcd _ inst _ b a)) {k : ℕ} (h : b * a = c ^ k),
    Nontrivial α →
      ∀ (ha : ¬a = 0) (hb : ¬b = 0) (hk : k > 0) (hc : c ∣ a * b) (d₁ d₂ : α) (hd₁ : d₁ ∣ a) (hd₂ : d₂ ∣ b)
        (hc : c = d₂ * d₁) (h0₁ : d₁ ^ k ≠ 0) (a' : α) (ha' : a = d₁ ^ k * a'), Associated (d₁ ^ k) a
⊢ Associated (d₁ ^ k) a

Tactic:
rw [(gcd_comm' a b).isUnit_iff] at hab

Premises used: Associated.isUnit_iff, gcd_comm'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h₁ : ∀ (h0₂ : d₂ ^ k ≠ 0) (b' : α) (hb' : b = d₂ ^ k * b'), Associated (d₁ ^ k) a
⊢ Associated (d₁ ^ k) a

Tactic:
obtain ⟨h0₂, ⟨b', hb'⟩⟩ := pow_dvd_of_mul_eq_pow hb hab h hc hd₂

Premises used: pow_dvd_of_mul_eq_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h : b * a = c ^ k
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
hb' : b = d₂ ^ k * b'
h₁ :
  ∀ (ha' : a = d₁ ^ k * a') (h0₂ : d₂ ^ k ≠ 0) (b' : α) (h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k)
    (hb' : b = d₂ ^ k * b'), Associated (d₁ ^ k) a
⊢ Associated (d₁ ^ k) a

Tactic:
rw [ha', hb', hc, mul_pow] at h

Premises used: mul_pow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
apply : d₁ ^ k * (a' * b') = d₁ ^ k * 1
⊢ a' * b' = 1

Tactic:
apply (mul_right_inj' h0₁).mp

Premises used: Iff.mp, mul_right_inj'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₁ ^ k * (a' * b') = d₁ ^ k
⊢ d₁ ^ k * (a' * b') = d₁ ^ k * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
apply : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * d₁ ^ k
⊢ d₁ ^ k * (a' * b') = d₁ ^ k

Tactic:
apply (mul_right_inj' h0₂).mp

Premises used: Iff.mp, mul_right_inj'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * d₁ ^ k

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
rw : d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₁ : d₂ ^ k * (d₁ ^ k * (b' * a')) = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₂ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * (d₁ ^ k * a'))
rw₃ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (b' * d₁ ^ k * a')
rw₄ rw₅ : d₂ ^ k * (d₁ ^ k * b' * a') = d₂ ^ k * (d₁ ^ k * b' * a')
⊢ d₂ ^ k * (d₁ ^ k * (a' * b')) = d₂ ^ k * b' * (d₁ ^ k * a')

Tactic:
rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
⊢ a' * b' = 1

Tactic:
have h' : a' * b' = 1 := by
    apply (mul_right_inj' h0₁).mp
    rw [mul_one]
    apply (mul_right_inj' h0₂).mp
    rw [← h]
    rw [mul_assoc, mul_comm a', ← mul_assoc _ b', ← mul_assoc b', mul_comm b']
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : IsUnit (@gcd _ inst _ b a)
k : ℕ
h_1 : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc_1 : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = d₂ ^ k * d₁ ^ k
hb' : b = d₂ ^ k * b'
h' : a' * b' = 1
h₁ : d₁ ^ k * (↑(Units.mkOfMulEqOne a' b' h') : α) = a
⊢ Associated (d₁ ^ k) a

Tactic:
use Units.mkOfMulEqOne _ _ h'

Premises used: Units.mkOfMulEqOne