awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
h : Nontrivial α
inl : Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑1 : α))) 1
inl₁ : Eq.{u_1 + 1} (α := αˣ) (normUnit 0) 1
inl₂ inl₃ : Eq.{u_1 + 1} (α := αˣ) 1 1
⊢ Eq (α := αˣ) (normUnit (HMul.hMul (α := α) 0 (↑(normUnit 0) : α))) 1

Tactic:
rw [normUnit_zero, zero_mul, normUnit_zero]

Premises used: MulZeroClass.zero_mul, NormalizationMonoid.normUnit_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a : α
h_1 : Nontrivial α
h : a ≠ 0
inr : HMul.hMul (α := αˣ) (normUnit a) (normUnit (↑(normUnit a) : α)) = 1
inr₁ : HMul.hMul (α := αˣ) (normUnit a) (normUnit a)⁻¹ = 1
inr₂ inr₃ : Eq (α := αˣ) (normUnit a) (normUnit a)
⊢ Eq (α := αˣ) (normUnit (a * (↑(normUnit a) : α))) 1

Tactic:
rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]

Premises used: mul_inv_eq_one, NormalizationMonoid.normUnit_coe_units, Units.ne_zero, NormalizationMonoid.normUnit_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
x : α
⊢ Eq (α := α) ((normalize : (a : α) → α) ((normalize : (a : α) → α) x : α) : α) ((normalize : (a : α) → α) x : α)

Tactic:
simp [normalize_apply]

Premises used: normalize_apply
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
hab : a ∣ b
hba : b ∣ a
h : Nontrivial α
rcases :
  ∀ (u : αˣ) (hab : a ∣ a * (↑u : α)) (hba : a * (↑u : α) ∣ a),
    Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) b : α)

Tactic:
rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩

Premises used: associated_of_dvd_dvd, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
h : Nontrivial α
u : αˣ
hab : 0 ∣ 0 * (↑u : α)
hba : 0 * (↑u : α) ∣ 0
⊢ Eq (α := α) ((normalize : (a : α) → α) 0 : α) ((normalize : (a : α) → α) (0 * (↑u : α)) : α)

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
⊢ a ≠ 0

Tactic:
refine by_cases (by rintro rfl; simp) fun ha : a ≠ 0 => ?_

Premises used: by_cases
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
this : a * (↑(normUnit a) : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)

Tactic:
simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]

Premises used: NormalizationMonoid.normUnit_coe_units, mul_assoc, Units.ne_zero, normalize_apply, NormalizationMonoid.normUnit_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
suffices : a * (↑(normUnit a) : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
⊢ Eq (α := α) ((normalize : (a : α) → α) a : α) ((normalize : (a : α) → α) (a * (↑u : α)) : α)

Tactic:
suffices a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹ by
    simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
⊢ a * (↑(normUnit a) : α) = a * (↑(normUnit a) : α) * (↑u : α) * (↑u⁻¹ : α)

Tactic:
(Units.mul_inv_cancel_right _ _).symm

Premises used: Units.mul_inv_cancel_right, Eq.symm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
rw rw₁ : a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
⊢ a * (↑(normUnit a) : α) * (↑u : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)

Tactic:
rw [mul_right_comm a]

Premises used: mul_right_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a : α
h : Nontrivial α
u : αˣ
hab : a ∣ a * (↑u : α)
hba : a * (↑u : α) ∣ a
ha : a ≠ 0
a₁ : a * (↑(normUnit a) : α) * (↑u : α) * (↑u⁻¹ : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)
⊢ a * (↑(normUnit a) : α) = a * (↑u : α) * (↑(normUnit a) : α) * (↑u⁻¹ : α)

Tactic:
calc
    a * ↑(normUnit a) = a * ↑(normUnit a) * ↑u * ↑u⁻¹ := (Units.mul_inv_cancel_right _ _).symm
    _ = a * ↑u * ↑(normUnit a) * ↑u⁻¹ := by rw [mul_right_comm a]

Premises used: Units.mul_inv_cancel_right, Eq.symm, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
x y : α
⊢ Eq (α := α) ((normalize : (a : α) → α) x : α) ((normalize : (a : α) → α) y : α) ↔ x ∣ y ∧ y ∣ x

Tactic:
⟨fun h => ⟨Units.dvd_mul_right.1 ⟨_, h.symm⟩, Units.dvd_mul_right.1 ⟨_, h⟩⟩, fun ⟨hxy, hyx⟩ =>
    normalize_eq_normalize hxy hyx⟩

Premises used: Units.val, normalize_eq_normalize, Units.dvd_mul_right, And.intro, Iff.intro, Exists.intro, Iff.mp, _private.0.normalize_eq_normalize_iff.match_1, normalize, Eq.symm, Eq, DFunLike.coe, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
x y : α
rw : x ∣ y ∧ y ∣ x ↔ Associated x y
rw₁ rw₂ : Associated x y ↔ Associated x y
⊢ Eq (α := α) ((normalize : (a : α) → α) x : α) ((normalize : (a : α) → α) y : α) ↔ Associated x y

Tactic:
rw [normalize_eq_normalize_iff, dvd_dvd_iff_associated]

Premises used: normalize_eq_normalize_iff, dvd_dvd_iff_associated
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
ha : (normalize : (a : α) → α) a = a
hb : (normalize : (a : α) → α) b = b
hab : a ∣ b
hba : b ∣ a
⊢ a = b

Tactic:
ha ▸ hb ▸ normalize_eq_normalize hab hba

Premises used: normalize_eq_normalize, Eq.rec
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : IsCancelMulZero α
a b : α
h : Associated a b
ha : (normalize : (a : α) → α) a = a
hb : (normalize : (a : α) → α) b = b
⊢ a = b

Tactic:
dvd_antisymm_of_normalize_eq ha hb h.dvd h.dvd'

Premises used: Associated.dvd, dvd_antisymm_of_normalize_eq, Associated.dvd'
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a b : α
⊢ a ∣ (normalize : (a : α) → α) b ↔ a ∣ b

Tactic:
Units.dvd_mul_right

Premises used: Units.dvd_mul_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
a b : α
⊢ (normalize : (a : α) → α) a ∣ b ↔ a ∣ b

Tactic:
Units.mul_right_dvd

Premises used: Units.mul_right_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : α
⊢ Associates.out (Associates.mk a) = (normalize : (a : α) → α) a

Tactic:
rfl

Premises used: Associates.out, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) (Associates.out 1) 1

Tactic:
normalize_one

Premises used: normalize_one, Associates.out
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a b : Associates α
x x_1 : α
⊢ (⟦x⟧ * ⟦x_1⟧).out = Associates.out ⟦x⟧ * Associates.out ⟦x_1⟧

Tactic:
simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]

Premises used: Associates.out_mk, Associates.quotient_mk_eq_mk, Associates.mk_mul_mk, normalize, MonoidWithZeroHom.map_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Premises used: Associates.mk_le_mk_iff_dvd, Associates.out_mk, Associates.quotient_mk_eq_mk
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : α
b : Associates α
⊢ ∀ (a_1 : α), Associates.out ⟦a_1⟧ ∣ a ↔ ⟦a_1⟧ ≤ Associates.mk a

Tactic:
simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

Premises used: Associates.mk_le_mk_iff_dvd, Associates.out_mk, Associates.quotient_mk_eq_mk
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) (Associates.out ⊤) 0

Tactic:
normalize_zero

Premises used: Associates.out, normalize_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : Associates α
⊢ (normalize : (a : α) → α) a.out = a.out

Tactic:
Quotient.inductionOn a normalize_idem

Premises used: Quotient.inductionOn
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : Associates α
⊢ Associates.mk a.out = a

Tactic:
Quotient.inductionOn a mk_normalize

Premises used: Quotient.inductionOn
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := Associates α) Associates.out

Tactic:
Function.LeftInverse.injective mk_out

Premises used: Function.LeftInverse.injective, Associates.mk_out
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
a : Associates α
⊢ ∀ (a : α), Associates.out ⟦a⟧ = 0 ↔ ⟦a⟧ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
⊢ Eq.{u_1 + 1} (α := α) (Associates.out 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
⊢ Nonempty.{u_1 + 1} (NormalizationMonoid α)

Tactic:
⟨‹_›⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
⊢ Nonempty.{u_1 + 1} (GCDMonoid α)

Tactic:
⟨‹_›⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
⊢ Nonempty.{u_1 + 1} (NormalizedGCDMonoid α)

Tactic:
⟨‹_›⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
h : Nonempty.{u_1 + 1} (NormalizedGCDMonoid α)
⊢ Nonempty.{u_1 + 1} (NormalizationMonoid α)

Tactic:
h.elim fun _ ↦ inferInstance

Premises used: Nonempty.elim, inferInstance
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
h : Nonempty.{u_1 + 1} (NormalizedGCDMonoid α)
⊢ Nonempty.{u_1 + 1} (GCDMonoid α)

Tactic:
h.elim fun _ ↦ inferInstance

Premises used: Nonempty.elim, inferInstance
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ IsUnit (@gcd _ inst _ a b) ↔ IsRelPrime a b

Tactic:
⟨fun h _ ha hb ↦ isUnit_of_dvd_unit (dvd_gcd ha hb) h, (· (gcd_dvd_left a b) (gcd_dvd_right a b))⟩

Premises used: isUnit_of_dvd_unit, GCDMonoid.dvd_gcd, Iff.intro, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
⊢ ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b

Tactic:
NormalizedGCDMonoid.normalize_gcd

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

Tactic:
GCDMonoid.gcd_mul_lcm

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

Tactic:
Iff.intro (fun h => ⟨h.trans (gcd_dvd_left _ _), h.trans (gcd_dvd_right _ _)⟩) fun ⟨hab, hac⟩ =>
    dvd_gcd hab hac

Premises used: Dvd.dvd, GCDMonoid.dvd_gcd, GCDMonoid.gcd, And.intro, Iff.intro, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right, _private.0.dvd_gcd_iff.match_1, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
⊢ @gcd _ inst _ a b = @gcd _ inst _ b a

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

Premises used: dvd_antisymm_of_normalize_eq, GCDMonoid.dvd_gcd, normalize_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 : α
⊢ Associated (@gcd _ inst _ a b) (@gcd _ inst _ b a)

Tactic:
associated_of_dvd_dvd (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

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_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
m n k : α
⊢ @gcd _ inst _ (@gcd _ inst _ m n) k = @gcd _ inst _ m (@gcd _ inst _ n k)

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
      (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
    (dvd_gcd
      (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
      ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))

Premises used: dvd_antisymm_of_normalize_eq, GCDMonoid.dvd_gcd, normalize_gcd, GCDMonoid.gcd, 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 α
m n k : α
⊢ Associated (@gcd _ inst _ (@gcd _ inst _ m n) k) (@gcd _ inst _ m (@gcd _ inst _ n k))

Tactic:
associated_of_dvd_dvd
    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
      (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
    (dvd_gcd
      (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
      ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))

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

Tactic:
normalize_gcd a b ▸ normalize_eq_normalize habc hcab

Premises used: normalize_eq_normalize, Eq.rec, normalize_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @gcd _ inst _ 0 a = (normalize : (a : α) → α) a

Tactic:
gcd_eq_normalize (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))

Premises used: dvd_zero, gcd_eq_normalize, GCDMonoid.dvd_gcd, OfNat.ofNat, GCDMonoid.gcd_dvd_right, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ Associated (@gcd _ inst _ 0 a) a

Tactic:
associated_of_dvd_dvd (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))

Premises used: dvd_zero, associated_of_dvd_dvd, GCDMonoid.dvd_gcd, OfNat.ofNat, GCDMonoid.gcd_dvd_right, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @gcd _ inst _ a 0 = (normalize : (a : α) → α) a

Tactic:
gcd_eq_normalize (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))

Premises used: dvd_zero, gcd_eq_normalize, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, OfNat.ofNat, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ Associated (@gcd _ inst _ a 0) a

Tactic:
associated_of_dvd_dvd (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))

Premises used: dvd_zero, associated_of_dvd_dvd, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, OfNat.ofNat, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
let : ∀ (ca : α) (ha : a = @gcd _ inst _ a b * ca), a = 0 ∧ b = 0
⊢ a = 0 ∧ b = 0

Tactic:
let ⟨ca, ha⟩ := gcd_dvd_left a b
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = @gcd _ inst _ a b * ca
let : ∀ (cb : α) (hb : b = @gcd _ inst _ a b * cb), a = 0 ∧ b = 0
⊢ a = 0 ∧ b = 0

Tactic:
let ⟨cb, hb⟩ := gcd_dvd_right a b
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = @gcd _ inst _ a b * ca
cb : α
hb : b = @gcd _ inst _ a b * cb
rw : ∀ (ha : a = 0) (cb : α) (hb : b = 0), a = 0 ∧ b = 0
⊢ a = 0 ∧ b = 0

Tactic:
rw [h, zero_mul] at ha hb

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0

Tactic:
⟨ha, hb⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @gcd _ inst _ a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0

Tactic:
exact ⟨ha, hb⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
rw : Dvd.dvd.{u_1} (α := α) 0 (@gcd _ inst _ 0 0)
⊢ @gcd _ inst _ a b = 0

Tactic:
rw [ha, hb, ← zero_dvd_iff]

Premises used: zero_dvd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
a₁ a₂ : Dvd.dvd.{u_1} (α := α) 0 0
⊢ Dvd.dvd.{u_1} (α := α) 0 (@gcd _ inst _ 0 0)

Tactic:
apply dvd_gcd

Premises used: GCDMonoid.dvd_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ Dvd.dvd.{u_1} (α := α) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
ha : a ≠ 0
⊢ @gcd _ inst _ a b ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
hb : b ≠ 0
⊢ @gcd _ inst _ a b ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @gcd _ inst _ 1 a = 1

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_left _ _) (one_dvd _)

Premises used: normalize_one, dvd_antisymm_of_normalize_eq, normalize_gcd, one_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ IsUnit (@gcd _ inst _ 1 a)

Tactic:
isUnit_of_dvd_one (gcd_dvd_left _ _)

Premises used: isUnit_of_dvd_one, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ Associated (@gcd _ inst _ 1 a) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a : α
⊢ @gcd _ inst _ a 1 = 1

Tactic:
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)

Premises used: normalize_one, dvd_antisymm_of_normalize_eq, normalize_gcd, one_dvd, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ IsUnit (@gcd _ inst _ a 1)

Tactic:
isUnit_of_dvd_one (gcd_dvd_right _ _)

Premises used: isUnit_of_dvd_one, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a : α
⊢ Associated (@gcd _ inst _ a 1) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c d : α
hab : a ∣ b
hcd : c ∣ d
⊢ @gcd _ inst _ a c ∣ @gcd _ inst _ b d

Tactic:
dvd_gcd ((gcd_dvd_left _ _).trans hab) ((gcd_dvd_right _ _).trans hcd)

Premises used: GCDMonoid.dvd_gcd, 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 α
a₁ a₂ b₁ b₂ : α
ha : Associated a₁ a₂
hb : Associated b₁ b₂
⊢ Associated (@gcd _ inst _ a₁ b₁) (@gcd _ inst _ a₂ b₂)

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

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

Tactic:
gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))

Premises used: gcd_eq_normalize, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
b c : α
⊢ @gcd _ inst _ (0 * b) (0 * c) = HMul.hMul (α := α) ((normalize : (a : α) → α) 0 : α) (@gcd _ 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 : @gcd _ inst _ (a * b) (a * c) = (normalize : (a : α) → α) (a * @gcd _ inst _ b c)
⊢ @gcd _ inst _ (a * b) (a * c) = HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (@gcd _ inst _ b c)

Tactic:
simpa
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
inl : Associated (@gcd _ inst _ (0 * b) (0 * c)) (0 * @gcd _ inst _ b c)
inr : ∀ (ha : a ≠ 0), 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 rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl