awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * a' = a
h₂ h₃ : d₁ ^ k * a' = d₁ ^ k * a'
⊢ d₁ ^ k * (↑(Units.mkOfMulEqOne a' b' h') : α) = a

Tactic:
rw [Units.val_mkOfMulEqOne, ha']

Premises used: Units.val_mkOfMulEqOne
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
inst_2 : Subsingleton.{u_1 + 1} αˣ
a b c : α
hab : IsUnit (@gcd _ inst _ a b)
k : ℕ
h : a * b = c ^ k
⊢ ∃ (d : α), a = d ^ k

Tactic:
let ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow hab h
  ⟨d, (associated_iff_eq.mp hd).symm⟩

Premises used: Exists, _private.0.exists_eq_pow_of_mul_eq_pow.match_1, associated_iff_eq, HPow.hPow, Exists.intro, Iff.mp, exists_associated_pow_of_mul_eq_pow, Eq.symm, Eq
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b d : α
hda : d ∣ a
hdb : d ∣ b
hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d
⊢ @gcd _ inst _ a b = (normalize : (a : α) → α) d

Tactic:
haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
  gcd_eq_normalize h (GCDMonoid.dvd_gcd hda hdb)

Premises used: gcd_eq_normalize, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b d : α
hda : d ∣ a
hdb : d ∣ b
hd : ∀ (e : α), e ∣ a → e ∣ b → e ∣ d
⊢ Associated d (@gcd _ inst _ a b)

Tactic:
haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
  associated_of_dvd_dvd (GCDMonoid.dvd_gcd hda hdb) h

Premises used: associated_of_dvd_dvd, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
rw : Associated (@gcd _ inst _ x' y') 1
⊢ IsUnit (@gcd _ inst _ x' y')

Tactic:
rw [← associated_one_iff_isUnit]

Premises used: associated_one_iff_isUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ Associated (@gcd _ inst _ x' y') 1

Tactic:
Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h

Premises used: GCDMonoid.gcd, Associated.refl, Associated.of_mul_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
refine : Associated (@gcd _ inst _ x y * @gcd _ inst _ x' y') (@gcd _ inst _ x y * 1)
⊢ Associated (@gcd _ inst _ x' y') 1

Tactic:
refine Associated.of_mul_left ?_ (Associated.refl <| gcd x y) h

Premises used: GCDMonoid.gcd, Associated.refl, Associated.of_mul_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ Associated (@gcd _ inst _ x y * @gcd _ inst _ x' y') (@gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y'))

Tactic:
(gcd_mul_left' (gcd x y) x' y').symm

Premises used: GCDMonoid.gcd, Associated.symm, gcd_mul_left'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')
⊢ Associated (@gcd _ inst _ x y * @gcd _ inst _ x' y') (@gcd _ inst _ x y * 1)

Tactic:
convert! (gcd_mul_left' (gcd x y) x' y').symm using 1

Premises used: GCDMonoid.gcd, Associated.symm, gcd_mul_left'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x (@gcd _ inst _ x y * y')
h₂ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x y
h₃ h₄ : @gcd _ inst _ x y = @gcd _ inst _ x y
⊢ @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')

Tactic:
rw [← ex, ← ey, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
pos :
  ∀ (h : @gcd _ inst _ x y = 0),
    ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
neg :
  ∀ (h : ¬@gcd _ inst _ x y = 0),
    ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
by_cases h : gcd x y = 0

Premises used: GCDMonoid.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : @gcd _ inst _ x y = 0
pos :
  ∀ (h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0),
    ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ IsUnit (@gcd _ inst _ x' y')
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h

Premises used: gcd_eq_zero_iff, Iff.mp, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
pos :
  ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ Associated (@gcd _ inst _ x' y') 1
⊢ ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
simp_rw [← associated_one_iff_isUnit]

Premises used: associated_one_iff_isUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
rw : 0 = HMul.hMul (α := α) 0 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := α) 0 0
⊢ 0 = HMul.hMul (α := α) (@gcd _ inst _ 0 0) 1

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
⊢ ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ Associated (@gcd _ inst _ x' y') 1

Tactic:
exact ⟨1, 1, by rw [h, zero_mul], by rw [h, zero_mul], gcd_one_left' 1⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
neg :
  ∀ (x' : α) (ex : x = @gcd _ inst _ x y * x'),
    ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
obtain ⟨x', ex⟩ := gcd_dvd_left x y

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
x' : α
ex : x = @gcd _ inst _ x y * x'
neg :
  ∀ (y' : α) (ey : y = @gcd _ inst _ x y * y'),
    ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
obtain ⟨y', ey⟩ := gcd_dvd_right x y

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
x' : α
ex : x = @gcd _ inst _ x y * x'
y' : α
ey : y = @gcd _ inst _ x y * y'
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩

Premises used: isUnit_gcd_of_eq_mul_gcd, And.intro, Exists.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
x' : α
ex : x = @gcd _ inst _ x y * x'
y' : α
ey : y = @gcd _ inst _ x y * y'
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')

Tactic:
exact ⟨x', y', ex, ey, isUnit_gcd_of_eq_mul_gcd ex ey h⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
⊢ Associated x (@gcd _ inst _ x y) ↔ x ∣ y

Tactic:
⟨fun hx => hx.dvd.trans (gcd_dvd_right x y),
    fun hxy => associated_of_dvd_dvd (dvd_gcd dvd_rfl hxy) (gcd_dvd_left x y)⟩

Premises used: Associated.dvd, associated_of_dvd_dvd, GCDMonoid.dvd_gcd, Iff.intro, dvd_rfl, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
⊢ Associated y (@gcd _ inst _ x y) ↔ y ∣ x

Tactic:
⟨fun hx => hx.dvd.trans (gcd_dvd_left x y),
    fun hxy => associated_of_dvd_dvd (dvd_gcd hxy dvd_rfl) (gcd_dvd_right x y)⟩

Premises used: Associated.dvd, associated_of_dvd_dvd, GCDMonoid.dvd_gcd, Iff.intro, dvd_rfl, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
hx : Irreducible x
rw : ¬Associated x (@gcd _ inst _ x y) ↔ ¬x ∣ y
rw₁ : Associated x (@gcd _ inst _ x y) ↔ x ∣ y
rw₂ rw₃ : x ∣ y ↔ x ∣ y
⊢ IsUnit (@gcd _ inst _ x y) ↔ ¬x ∣ y

Tactic:
rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]

Premises used: not_iff_not, Irreducible.isUnit_iff_not_associated_of_dvd, associated_gcd_left_iff, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
rw : @gcd _ inst _ x y = 1 ↔ IsUnit (@gcd _ inst _ x y)
rw₁ : @gcd _ inst _ x y = 1 ↔ Eq (α := α) ((normalize : (a : α) → α) (@gcd _ inst _ x y) : α) (1 : α)
rw₂ rw₃ : @gcd _ inst _ x y = 1 ↔ @gcd _ inst _ x y = 1
⊢ @gcd _ inst _ x y = 1 ↔ ¬x ∣ y

Tactic:
rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]

Premises used: Irreducible.isUnit_gcd_iff, NormalizedGCDMonoid.normalize_gcd, normalize_eq_one
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : HasDistribNeg α
inst_2 : GCDMonoid α
a b : α
⊢ Associated (@gcd _ inst _ a (-b)) (@gcd _ inst _ a b)

Tactic:
Associated.gcd .rfl (.neg_left .rfl)

Premises used: Associated.rfl, Associated.neg_left, Associated.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : HasDistribNeg α
inst_2 : NormalizedGCDMonoid α
a b : α
⊢ @gcd _ inst _ a (-b) = @gcd _ inst _ a b

Tactic:
gcd_neg'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)

Premises used: Associated.eq_of_normalized, normalize_gcd, gcd_neg'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : HasDistribNeg α
inst_2 : GCDMonoid α
a b : α
⊢ Associated (@gcd _ inst _ (-a) b) (@gcd _ inst _ a b)

Tactic:
Associated.gcd (.neg_left .rfl) .rfl

Premises used: Associated.rfl, Associated.neg_left, Associated.gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : HasDistribNeg α
inst_2 : NormalizedGCDMonoid α
a b : α
⊢ @gcd _ inst _ (-a) b = @gcd _ inst _ a b

Tactic:
neg_gcd'.eq_of_normalized (normalize_gcd _ _) (normalize_gcd _ _)

Premises used: Associated.eq_of_normalized, normalize_gcd, neg_gcd'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
pos : ∀ (h : a = 0 ∨ b = 0), @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
neg : ∀ (h : ¬(a = 0 ∨ b = 0)), @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
by_cases h : a = 0 ∨ b = 0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
pos : @lcm _ inst _ 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c
pos₁ : @lcm _ inst _ a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
rcases h with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
b c : α
⊢ @lcm _ inst _ 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c

Tactic:
simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
        zero_dvd_iff, dvd_zero, and_true, imp_true_iff]

Premises used: GCDMonoid.lcm_zero_right, dvd_zero, and_true, zero_dvd_iff, iff_def, imp_true_iff, GCDMonoid.lcm_zero_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a c : α
⊢ @lcm _ inst _ a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c

Tactic:
simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
        zero_dvd_iff, dvd_zero, and_true, imp_true_iff]

Premises used: GCDMonoid.lcm_zero_right, dvd_zero, and_true, zero_dvd_iff, iff_def, imp_true_iff, GCDMonoid.lcm_zero_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ ¬a = 0

Tactic:
obtain ⟨h1, h2⟩ := not_or.1 h

Premises used: not_or, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
⊢ ¬b = 0

Tactic:
obtain ⟨h1, h2⟩ := not_or.1 h

Premises used: not_or, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ @gcd _ inst _ a b ≠ 0

Tactic:
have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
neg₄ : a * b ∣ a * c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
neg₅ : b ∣ c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
neg₆ : b ∣ c ∧ a ∣ c ↔ a ∣ c ∧ b ∣ c
neg₇ neg₈ : a ∣ c ∧ b ∣ c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]

Premises used: gcd_mul_lcm, gcd_mul_right', mul_dvd_mul_iff_right, and_comm, mul_dvd_mul_iff_left, mul_comm, Associated.dvd_iff_dvd_left, Associated.dvd_iff_dvd_right, dvd_gcd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ a ∣ @lcm _ inst _ a b

Tactic:
(lcm_dvd_iff.1 (dvd_refl (lcm a b))).1

Premises used: lcm_dvd_iff, GCDMonoid.lcm, And.left, Iff.mp, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ b ∣ @lcm _ inst _ a b

Tactic:
(lcm_dvd_iff.1 (dvd_refl (lcm a b))).2

Premises used: lcm_dvd_iff, GCDMonoid.lcm, And.right, Iff.mp, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
hab : a ∣ b
hcb : c ∣ b
⊢ @lcm _ inst _ a c ∣ b

Tactic:
lcm_dvd_iff.2 ⟨hab, hcb⟩

Premises used: Iff.mpr, lcm_dvd_iff, And.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
rw : Associated (@gcd _ inst _ a b * 0) 0
rw₁ rw₂ : Associated.{u_1} (M := α) 0 0
⊢ Associated (@gcd _ inst _ a b * @lcm _ inst _ a b) 0

Tactic:
rw [h, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
⊢ Associated (a * b) 0

Tactic:
have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
this : Associated (a * b) 0
rwa : a * b = 0
rwa₁ rwa₂ rwa₃ rwa₄ : Associated (a * b) 0
⊢ a = 0 ∨ b = 0

Tactic:
rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero]

Premises used: associated_zero_iff_eq_zero, mul_eq_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
b : α
⊢ @lcm _ inst _ 0 b = 0

Tactic:
apply lcm_zero_left

Premises used: GCDMonoid.lcm_zero_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ @lcm _ inst _ a 0 = 0

Tactic:
apply lcm_zero_right

Premises used: GCDMonoid.lcm_zero_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
⊢ (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b

Tactic:
NormalizedGCDMonoid.normalize_lcm a b

Premises used: NormalizedGCDMonoid.normalize_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
⊢ @lcm _ inst _ a b = @lcm _ inst _ b a

Tactic:
dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

Premises used: dvd_lcm_right, lcm_dvd, dvd_antisymm_of_normalize_eq, dvd_lcm_left, normalize_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ Associated (@lcm _ inst _ a b) (@lcm _ inst _ b a)

Tactic:
associated_of_dvd_dvd (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

Premises used: dvd_lcm_right, lcm_dvd, associated_of_dvd_dvd, dvd_lcm_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
m n k : α
⊢ @lcm _ inst _ (@lcm _ inst _ m n) k = @lcm _ inst _ m (@lcm _ inst _ n k)

Tactic:
dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
    (lcm_dvd (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
      ((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
    (lcm_dvd ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
      (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))

Premises used: dvd_lcm_right, lcm_dvd, dvd_antisymm_of_normalize_eq, dvd_lcm_left, normalize_lcm, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ Associated (@lcm _ inst _ (@lcm _ inst _ m n) k) (@lcm _ inst _ m (@lcm _ inst _ n k))

Tactic:
associated_of_dvd_dvd
    (lcm_dvd (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
      ((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
    (lcm_dvd ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
      (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))

Premises used: dvd_lcm_right, lcm_dvd, associated_of_dvd_dvd, dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b c : α
habc : @lcm _ inst _ a b ∣ c
hcab : c ∣ @lcm _ inst _ a b
⊢ @lcm _ inst _ a b = (normalize : (a : α) → α) c

Tactic:
normalize_lcm a b ▸ normalize_eq_normalize habc hcab

Premises used: normalize_eq_normalize, Eq.rec, normalize_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d : α
hab : a ∣ b
hcd : c ∣ d
⊢ @lcm _ inst _ a c ∣ @lcm _ inst _ b d

Tactic:
lcm_dvd (hab.trans (dvd_lcm_left _ _)) (hcd.trans (dvd_lcm_right _ _))

Premises used: dvd_lcm_right, lcm_dvd, dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a₁ a₂ b₁ b₂ : α
ha : Associated a₁ a₂
hb : Associated b₁ b₂
⊢ Associated (@lcm _ inst _ a₁ b₁) (@lcm _ inst _ a₂ b₂)

Tactic:
associated_of_dvd_dvd (lcm_dvd_lcm ha.dvd hb.dvd) (lcm_dvd_lcm ha.dvd' hb.dvd')

Premises used: Associated.dvd, associated_of_dvd_dvd, Associated.dvd', lcm_dvd_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
u : αˣ
a : α
⊢ @lcm _ inst _ (↑u : α) a = (normalize : (a : α) → α) a

Tactic:
lcm_eq_normalize (lcm_dvd Units.coe_dvd dvd_rfl) (dvd_lcm_right _ _)

Premises used: dvd_lcm_right, lcm_dvd, Units.coe_dvd, dvd_rfl, lcm_eq_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
u : αˣ
⊢ @lcm _ inst _ a (↑u : α) = (normalize : (a : α) → α) a

Tactic:
(lcm_comm a u).trans <| lcm_units_coe_left _ _

Premises used: Units.val, lcm_units_coe_left, lcm_comm, Eq.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @lcm _ inst _ 1 a = (normalize : (a : α) → α) a

Tactic:
lcm_units_coe_left 1 a

Premises used: lcm_units_coe_left, OfNat.ofNat
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @lcm _ inst _ a 1 = (normalize : (a : α) → α) a

Tactic:
lcm_units_coe_right a 1

Premises used: OfNat.ofNat, lcm_units_coe_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @lcm _ inst _ a a = (normalize : (a : α) → α) a

Tactic:
lcm_eq_normalize (lcm_dvd dvd_rfl dvd_rfl) (dvd_lcm_left _ _)

Premises used: lcm_dvd, dvd_lcm_left, dvd_rfl, lcm_eq_normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
rw : Eq (α := α) ((normalize : (a : α) → α) (↑(Units.mkOfMulEqOne b d ⋯) : α) : α) (1 : α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) 1 1
⊢ @lcm _ inst _ (↑(Units.mkOfMulEqOne a c ⋯) : α) (↑(Units.mkOfMulEqOne b d ⋯) : α) = 1

Tactic:
rw [lcm_units_coe_left, normalize_coe_units]

Premises used: normalize_coe_units, lcm_units_coe_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
b c : α
⊢ @lcm _ inst _ (0 * b) (0 * c) = HMul.hMul (α := α) ((normalize : (a : α) → α) 0 : α) (@lcm _ inst _ b c)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : @lcm _ inst _ (a * b) (a * c) = (normalize : (a : α) → α) (a * @lcm _ inst _ b c)
⊢ @lcm _ inst _ (a * b) (a * c) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (@lcm _ inst _ b c)

Tactic:
simpa
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b c : α
⊢ @lcm _ inst _ (b * a) (c * a) = HMul.hMul (β := α) (@lcm _ inst _ b c) ((normalize : (a : α) → α) a : α)

Tactic:
simp only [mul_comm, lcm_mul_left]

Premises used: lcm_mul_left, mul_comm