awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
b c : α
⊢ Associated (@gcd _ inst _ (0 * b) (0 * c)) (0 * @gcd _ inst _ b c)

Tactic:
simp only [zero_mul, gcd_zero_left']

Premises used: MulZeroClass.zero_mul, gcd_zero_left'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
inr :
  ∀ (d : α) (eq : @gcd _ inst _ (a * b) (a * c) = a * d),
    Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)

Tactic:
obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)

Premises used: GCDMonoid.dvd_gcd, dvd_mul_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
inr : @gcd _ inst _ (a * b) (a * c) ∣ a * @gcd _ inst _ b c
inr₁ : a * @gcd _ inst _ b c ∣ @gcd _ inst _ (a * b) (a * c)
⊢ Associated (@gcd _ inst _ (a * b) (a * c)) (a * @gcd _ inst _ b c)

Tactic:
apply associated_of_dvd_dvd

Premises used: associated_of_dvd_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
inr : a * d ∣ a * @gcd _ inst _ b c
⊢ @gcd _ inst _ (a * b) (a * c) ∣ a * @gcd _ inst _ b c

Tactic:
rw [eq]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
inr : d ∣ @gcd _ inst _ b c
⊢ a * d ∣ a * @gcd _ inst _ b c

Tactic:
gcongr
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ d ∣ @gcd _ inst _ b c

Tactic:
dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
        ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)

Premises used: Eq.rec, GCDMonoid.dvd_gcd, mul_dvd_mul_iff_left, Iff.mp, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ d ∣ @gcd _ inst _ b c

Tactic:
exact
      dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
        ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)

Premises used: GCDMonoid.dvd_gcd, mul_dvd_mul_iff_left, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ a * @gcd _ inst _ b c ∣ @gcd _ inst _ (a * b) (a * c)

Tactic:
dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)

Premises used: mul_dvd_mul_left, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
ha : a ≠ 0
d : α
eq : @gcd _ inst _ (a * b) (a * c) = a * d
⊢ a * @gcd _ inst _ b c ∣ @gcd _ inst _ (a * b) (a * c)

Tactic:
exact dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)

Premises used: mul_dvd_mul_left, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b c : α
⊢ @gcd _ inst _ (b * a) (c * a) = HMul.hMul (β := α) (@gcd _ inst _ b c) ((normalize : (a : α) → α) a : α)

Tactic:
simp only [mul_comm, gcd_mul_left]

Premises used: gcd_mul_left, mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
⊢ Associated (@gcd _ inst _ (b * a) (c * a)) (@gcd _ inst _ b c * a)

Tactic:
simp only [mul_comm, gcd_mul_left']

Premises used: gcd_mul_left', mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : (normalize : (a : α) → α) a = a
⊢ @gcd _ inst _ a b = a ↔ a ∣ b

Tactic:
(Iff.intro fun eq => eq ▸ gcd_dvd_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab)

Premises used: dvd_antisymm_of_normalize_eq, GCDMonoid.dvd_gcd, normalize_gcd, Iff.intro, GCDMonoid.gcd_dvd_left, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : (normalize : (a : α) → α) b = b
⊢ @gcd _ inst _ a b = b ↔ b ∣ a

Tactic:
simpa only [gcd_comm a b] using gcd_eq_left_iff b a h

Premises used: gcd_comm, gcd_eq_left_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
grw grw₁ : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ (k * m) n

Tactic:
grw [← dvd_mul_left]

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
grw grw₁ : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ (m * k) n

Tactic:
grw [← dvd_mul_right]

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
grw grw₁ : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ m (k * n)

Tactic:
grw [← dvd_mul_left]

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
grw grw₁ : @gcd _ inst _ m n ∣ @gcd _ inst _ m n
⊢ @gcd _ inst _ m n ∣ @gcd _ inst _ m (n * k)

Tactic:
grw [← dvd_mul_right]

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
m n : α
h : Associated m n
k : α
⊢ @gcd _ inst _ m k = @gcd _ inst _ n k

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (gcd_dvd_gcd h.dvd dvd_rfl)
    (gcd_dvd_gcd h.symm.dvd dvd_rfl)

Premises used: Associated.dvd, dvd_antisymm_of_normalize_eq, normalize_gcd, Associated.symm, dvd_rfl, gcd_dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
m n : α
h : Associated m n
k : α
⊢ @gcd _ inst _ k m = @gcd _ inst _ k n

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (gcd_dvd_gcd dvd_rfl h.dvd)
    (gcd_dvd_gcd dvd_rfl h.symm.dvd)

Premises used: Associated.dvd, dvd_antisymm_of_normalize_eq, normalize_gcd, Associated.symm, dvd_rfl, gcd_dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ @gcd _ inst _ k m * n

Tactic:
(dvd_gcd (dvd_mul_right _ n) H).trans (gcd_mul_right' n k m).dvd

Premises used: Associated.dvd, gcd_mul_right', GCDMonoid.dvd_gcd, dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ k ∣ @gcd _ inst _ k m * n ↔ k ∣ m * n

Tactic:
⟨fun h => h.trans (mul_dvd_mul (gcd_dvd_right k m) dvd_rfl), dvd_gcd_mul_of_dvd_mul⟩

Premises used: mul_dvd_mul, Iff.intro, dvd_rfl, dvd_gcd_mul_of_dvd_mul, GCDMonoid.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
H : k ∣ m * n
rw : ∀ (H : k ∣ n * m), k ∣ @gcd _ inst _ k n * m
⊢ k ∣ m * @gcd _ inst _ k n

Tactic:
rw [mul_comm] at H ⊢

Premises used: mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ @gcd _ inst _ k n * m

Tactic:
dvd_gcd_mul_of_dvd_mul H

Premises used: dvd_gcd_mul_of_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ @gcd _ inst _ k n * m

Tactic:
exact dvd_gcd_mul_of_dvd_mul H

Premises used: dvd_gcd_mul_of_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ k ∣ m * @gcd _ inst _ k n ↔ k ∣ m * n

Tactic:
⟨fun h => h.trans (mul_dvd_mul dvd_rfl (gcd_dvd_right k n)), dvd_mul_gcd_of_dvd_mul⟩

Premises used: mul_dvd_mul, dvd_mul_gcd_of_dvd_mul, Iff.intro, dvd_rfl, GCDMonoid.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
h : Nonempty.{u_1 + 1} (GCDMonoid α)
k m n : α
H : k ∣ m * n
intro : ∀ (val : GCDMonoid α), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
cases h
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
pos : ∀ (h0 : @gcd _ inst _ k m = 0), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
neg : ∀ (h0 : ¬@gcd _ inst _ k m = 0), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
by_cases h0 : gcd k m = 0

Premises used: GCDMonoid.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : @gcd _ inst _ k m = 0
⊢ k = 0 ∧ m = 0

Tactic:
rw [gcd_eq_zero_iff] at h0

Premises used: gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : k = 0 ∧ m = 0
pos : ∀ (H : 0 ∣ 0 * n), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ 0 ∧ a₂ ∣ n ∧ 0 = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
rcases h0 with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
n : α
val : GCDMonoid α
H : 0 ∣ 0 * n
⊢ 0 = 0 * n

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
n : α
val : GCDMonoid α
H : 0 ∣ 0 * n
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ 0 ∧ a₂ ∣ n ∧ 0 = a₁ * a₂

Tactic:
exact ⟨0, n, dvd_refl 0, dvd_refl n, by simp⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
neg : ∀ (a : α) (ha : k = @gcd _ inst _ k m * a), ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
obtain ⟨a, ha⟩ := gcd_dvd_left k m

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩

Premises used: GCDMonoid.gcd, And.intro, Exists.intro, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
neg : a ∣ n
⊢ ∃ (a₁ : α), ∃ (a₂ : α), a₁ ∣ m ∧ a₂ ∣ n ∧ k = a₁ * a₂

Tactic:
refine ⟨gcd k m, a, gcd_dvd_right _ _, ?_, ha⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
neg : k ∣ @gcd _ inst _ k m * n
⊢ a ∣ n

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← ha]

Premises used: mul_dvd_mul_iff_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
⊢ k ∣ @gcd _ inst _ k m * n

Tactic:
dvd_gcd_mul_of_dvd_mul H

Premises used: dvd_gcd_mul_of_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
k m n : α
H : k ∣ m * n
val : GCDMonoid α
h0 : ¬@gcd _ inst _ k m = 0
a : α
ha : k = @gcd _ inst _ k m * a
⊢ k ∣ @gcd _ inst _ k m * n

Tactic:
exact dvd_gcd_mul_of_dvd_mul H

Premises used: dvd_gcd_mul_of_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n : α
obtain :
  ∀ (m' n' : α) (hm' : m' ∣ m) (hn' : n' ∣ n) (h : @gcd _ inst _ k (m * n) = m' * n'),
    @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
⊢ @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n

Tactic:
obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))

Premises used: HMul.hMul, exists_dvd_and_dvd_of_dvd_mul, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
⊢ @gcd _ inst _ k (m * n) = m' * n'

Tactic:
replace h : gcd k (m * n) = m' * n' := h
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
rw : m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n
⊢ @gcd _ inst _ k (m * n) ∣ @gcd _ inst _ k m * @gcd _ inst _ k n

Tactic:
rw [h]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
⊢ m' * n' ∣ k

Tactic:
have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
a : m' ∣ @gcd _ inst _ k m
a₁ : n' ∣ @gcd _ inst _ k n
⊢ m' * n' ∣ @gcd _ inst _ k m * @gcd _ inst _ k n

Tactic:
apply mul_dvd_mul

Premises used: mul_dvd_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ k

Tactic:
have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hm'k : m' ∣ k
⊢ m' ∣ @gcd _ inst _ k m

Tactic:
dvd_gcd hm'k hm'

Premises used: GCDMonoid.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hm'k : m' ∣ k
⊢ m' ∣ @gcd _ inst _ k m

Tactic:
exact dvd_gcd hm'k hm'

Premises used: GCDMonoid.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ k

Tactic:
have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hn'k : n' ∣ k
⊢ n' ∣ @gcd _ inst _ k n

Tactic:
dvd_gcd hn'k hn'

Premises used: GCDMonoid.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : @gcd _ inst _ k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
hn'k : n' ∣ k
⊢ n' ∣ @gcd _ inst _ k n

Tactic:
exact dvd_gcd hn'k hn'

Premises used: GCDMonoid.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
pos : ∀ (hg : @gcd _ inst _ a b = 0), @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
neg : ∀ (hg : ¬@gcd _ inst _ a b = 0), @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k

Tactic:
by_cases hg : gcd a b = 0

Premises used: GCDMonoid.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : @gcd _ inst _ a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
rw [gcd_eq_zero_iff] at hg

Premises used: gcd_eq_zero_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : a = 0 ∧ b = 0
pos : @gcd _ inst _ 0 (HPow.hPow (α := α) 0 k) ∣ HPow.hPow (α := α) (@gcd _ inst _ 0 0) k
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k

Tactic:
rcases hg with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k : ℕ
⊢ @gcd _ inst _ 0 (HPow.hPow (α := α) 0 k) ∣ HPow.hPow (α := α) (@gcd _ inst _ 0 0) k

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

Premises used: Associated.dvd, pow_dvd_pow_of_dvd, Associated.symm, HPow.hPow, OfNat.ofNat, gcd_zero_left', Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
k : ℕ
⊢ @gcd _ inst _ 0 (HPow.hPow (α := α) 0 k) ∣ HPow.hPow (α := α) (@gcd _ inst _ 0 0) k

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

Premises used: Associated.dvd, pow_dvd_pow_of_dvd, Associated.symm, HPow.hPow, OfNat.ofNat, gcd_zero_left', Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
neg : @gcd _ inst _ a 1 ∣ 1
⊢ @gcd _ inst _ a (HPow.hPow (β := ℕ) b 0) ∣ HPow.hPow (β := ℕ) (@gcd _ inst _ a b) 0

Tactic:
rw [pow_zero, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
⊢ @gcd _ inst _ a 1 ∣ 1

Tactic:
(gcd_one_right' a).dvd

Premises used: Associated.dvd, gcd_one_right'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
⊢ @gcd _ inst _ a 1 ∣ 1

Tactic:
exact (gcd_one_right' a).dvd

Premises used: Associated.dvd, gcd_one_right'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
neg : @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b ^ (k + 1)) ∣ @gcd _ inst _ a b ^ (k + 1)

Tactic:
rw [pow_succ', pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
trans : @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k)
trans₁ : @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k

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

Premises used: GCDMonoid.gcd, HPow.hPow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k)

Tactic:
gcd_mul_dvd_mul_gcd a b (b ^ k)

Premises used: gcd_mul_dvd_mul_gcd, HPow.hPow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a (b * b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k)

Tactic:
exact gcd_mul_dvd_mul_gcd a b (b ^ k)

Premises used: gcd_mul_dvd_mul_gcd, HPow.hPow
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k

Tactic:
(mul_dvd_mul_iff_left hg).mpr hk

Premises used: Iff.mpr, mul_dvd_mul_iff_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hg : ¬@gcd _ inst _ a b = 0
k : ℕ
hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k
⊢ @gcd _ inst _ a b * @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b * @gcd _ inst _ a b ^ k

Tactic:
exact (mul_dvd_mul_iff_left hg).mpr hk

Premises used: Iff.mpr, mul_dvd_mul_iff_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
hg : ¬@gcd _ inst _ a b = 0
neg : @gcd _ inst _ a (HPow.hPow (β := ℕ) b 0) ∣ HPow.hPow (β := ℕ) (@gcd _ inst _ a b) 0
neg₁ :
  ∀ (k : ℕ) (hk : @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k),
    @gcd _ inst _ a (b ^ (k + 1)) ∣ @gcd _ inst _ a b ^ (k + 1)
⊢ @gcd _ inst _ a (b ^ k) ∣ @gcd _ inst _ a b ^ k

Tactic:
induction k with
    | zero => rw [pow_zero, pow_zero]; exact (gcd_one_right' a).dvd
    | succ k hk =>
      rw [pow_succ', pow_succ']
      trans gcd a b * gcd a (b ^ k)
      · exact gcd_mul_dvd_mul_gcd a b (b ^ k)
      · exact (mul_dvd_mul_iff_left hg).mpr hk

Premises used: Associated.dvd, pow_zero, gcd_mul_dvd_mul_gcd, GCDMonoid.gcd, HPow.hPow, gcd_one_right', pow_succ'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
k : ℕ
⊢ @gcd _ inst _ (a ^ k) b ∣ @gcd _ inst _ a b ^ k

Tactic:
calc
    gcd (a ^ k) b ∣ gcd b (a ^ k) := (gcd_comm' _ _).dvd
    _ ∣ gcd b a ^ k := gcd_pow_right_dvd_pow_gcd
    _ ∣ gcd a b ^ k := pow_dvd_pow_of_dvd (gcd_comm' _ _).dvd _

Premises used: Trans.trans, Associated.dvd, pow_dvd_pow_of_dvd, gcd_comm', gcd_pow_right_dvd_pow_gcd
-- 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
h₁ : @gcd _ inst _ (d₁ ^ k) b ∣ 1
⊢ IsUnit (@gcd _ inst _ (d₁ ^ k) 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
trans : @gcd _ inst _ (d₁ ^ k) b ∣ @gcd _ inst _ d₁ b ^ k
trans₁ : @gcd _ inst _ d₁ b ^ k ∣ 1
⊢ @gcd _ inst _ (d₁ ^ k) b ∣ 1

Tactic:
trans gcd d₁ b ^ k

Premises used: GCDMonoid.gcd
-- 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
⊢ @gcd _ inst _ (d₁ ^ k) b ∣ @gcd _ inst _ d₁ b ^ k

Tactic:
gcd_pow_left_dvd_pow_gcd

Premises used: gcd_pow_left_dvd_pow_gcd
-- 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
⊢ @gcd _ inst _ (d₁ ^ k) b ∣ @gcd _ inst _ d₁ b ^ k

Tactic:
exact gcd_pow_left_dvd_pow_gcd

Premises used: gcd_pow_left_dvd_pow_gcd
-- 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 ^ k)
⊢ @gcd _ inst _ d₁ b ^ k ∣ 1

Tactic:
apply IsUnit.dvd

Premises used: IsUnit.dvd