awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : (normalize : (a : α) → α) a = a
⊢ @lcm _ inst _ a b = a ↔ b ∣ a

Tactic:
(Iff.intro fun eq => eq ▸ dvd_lcm_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _)

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

Tactic:
simpa only [lcm_comm b a] using lcm_eq_left_iff b a h

Premises used: lcm_eq_left_iff, lcm_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n k : α
⊢ @lcm _ inst _ m n ∣ @lcm _ inst _ (k * m) n

Tactic:
lcm_dvd_lcm (dvd_mul_left _ _) dvd_rfl

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

Tactic:
lcm_dvd_lcm (dvd_mul_right _ _) dvd_rfl

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

Tactic:
lcm_dvd_lcm dvd_rfl (dvd_mul_left _ _)

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

Tactic:
lcm_dvd_lcm dvd_rfl (dvd_mul_right _ _)

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

Tactic:
dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd_lcm h.dvd dvd_rfl)
    (lcm_dvd_lcm h.symm.dvd dvd_rfl)

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

Tactic:
dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd_lcm dvd_rfl h.dvd)
    (lcm_dvd_lcm dvd_rfl h.symm.dvd)

Premises used: Associated.dvd, dvd_antisymm_of_normalize_eq, Associated.symm, normalize_lcm, lcm_dvd_lcm, dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n : α
⊢ m ∣ m * n

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
m n : α
⊢ n ∣ m * n

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

Tactic:
h.trans (dvd_lcm_left b c)

Premises used: dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : @lcm _ inst _ a b ∣ c
⊢ a ∣ c

Tactic:
(dvd_lcm_left a b).trans h

Premises used: dvd_lcm_left, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : a ∣ b
c : α
⊢ a ∣ @lcm _ inst _ c b

Tactic:
h.trans (dvd_lcm_right c b)

Premises used: dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : @lcm _ inst _ a b ∣ c
⊢ b ∣ c

Tactic:
(dvd_lcm_right a b).trans h

Premises used: dvd_lcm_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b p : α
hp : Prime p
h : p ∣ @lcm _ inst _ a b
⊢ p ∣ a ∨ p ∣ b

Tactic:
dvd_or_dvd hp (h.trans (lcm_dvd_mul a b))

Premises used: Prime.dvd_or_dvd, lcm_dvd_mul, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b p : α
hp : Prime p
⊢ p ∣ @lcm _ inst _ a b ↔ p ∣ a ∨ p ∣ b

Tactic:
⟨hp.dvd_or_dvd_of_dvd_lcm, (Or.elim · (dvd_lcm_of_dvd_left · _) (dvd_lcm_of_dvd_right · _))⟩

Premises used: dvd_lcm_of_dvd_left, Prime.dvd_or_dvd_of_dvd_lcm, Iff.intro, dvd_lcm_of_dvd_right, Or.elim
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b p : α
hp : Prime p
ha : ¬p ∣ a
hb : ¬p ∣ b
⊢ ¬p ∣ @lcm _ inst _ a b

Tactic:
hp.dvd_lcm.not.mpr <| not_or.mpr ⟨ha, hb⟩

Premises used: Iff.mpr, Iff.not, not_or, And.intro, Prime.dvd_lcm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
x : NormalizationMonoid α
u : α → αˣ
normUnit_zero : u 0 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → u (a * b) = u a * u b
normUnit_coe_units : ∀ (u_1 : αˣ), u (↑u_1 : α) = u_1⁻¹
e_normUnit : u = fun (x : α) ↦ 1
⊢ { normUnit := u, normUnit_zero := normUnit_zero, normUnit_mul := @normUnit_mul,
      normUnit_coe_units := normUnit_coe_units : NormalizationMonoid α } =
    NormalizationMonoid.ofUniqueUnits

Tactic:
congr
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
x : NormalizationMonoid α
u : α → αˣ
normUnit_zero : u 0 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → u (a * b) = u a * u b
normUnit_coe_units : ∀ (u_1 : αˣ), u (↑u_1 : α) = u_1⁻¹
⊢ u = fun (x : α) ↦ 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
h : ∀ (a b : α), @gcd _ inst _ a b = @gcd _ inst _ a b
⊢ Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)

Tactic:
ext a b
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ @gcd _ inst _ a b = @gcd _ inst _ a b

Tactic:
associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)

Premises used: associated_of_dvd_dvd, associated_iff_eq, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
a b : α
h : @gcd _ inst _ a b ∣ @gcd _ inst _ a b
h₁ : @gcd _ inst _ a b ∣ @gcd _ inst _ a b
⊢ @gcd _ inst _ a b = @gcd _ inst _ a b

Tactic:
refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)

Premises used: associated_of_dvd_dvd, associated_iff_eq, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ @gcd _ inst _ a b ∣ @gcd _ inst _ a b

Tactic:
apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]

Premises used: GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
⊢ Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)

Tactic:
have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
h : ∀ (a b : α), @lcm _ inst _ a b = @lcm _ inst _ a b
⊢ Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)

Tactic:
ext a b
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
a b : α
⊢ @lcm _ inst _ a b = @lcm _ inst _ a b

Tactic:
associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)

Premises used: associated_of_dvd_dvd, associated_iff_eq, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
a b : α
h : @lcm _ inst _ a b ∣ @lcm _ inst _ a b
h₁ : @lcm _ inst _ a b ∣ @lcm _ inst _ a b
⊢ @lcm _ inst _ a b = @lcm _ inst _ a b

Tactic:
refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)

Premises used: associated_of_dvd_dvd, associated_iff_eq, Iff.mp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
a b : α
⊢ @lcm _ inst _ a b ∣ @lcm _ inst _ a b

Tactic:
apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]

Premises used: dvd_lcm_right, lcm_dvd, dvd_lcm_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
⊢ Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)

Tactic:
have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
hlcm : Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)
mk :
  ∀ [toIsCancelMulZero : IsCancelMulZero α] (gcd lcm : α → α → α) (gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a)
    (gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b) (dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b)
    (gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)) (lcm_zero_left : ∀ (a : α), lcm 0 a = 0)
    (lcm_zero_right : ∀ (a : α), lcm a 0 = 0)
    (hgcd : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.gcd _ inst _) (@GCDMonoid.gcd _ inst _))
    (hlcm : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.lcm _ inst _) (@GCDMonoid.lcm _ inst _)),
    { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
        gcd_dvd_right := gcd_dvd_right, dvd_gcd := @dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
        lcm_zero_right := lcm_zero_right : GCDMonoid α } =
      g₂
⊢ g₁ = g₂

Tactic:
cases g₁
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₂ : GCDMonoid α
toIsCancelMulZero : IsCancelMulZero α
gcd lcm : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)
lcm_zero_left : ∀ (a : α), lcm 0 a = 0
lcm_zero_right : ∀ (a : α), lcm a 0 = 0
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.gcd _ inst _) (@GCDMonoid.gcd _ inst _)
hlcm : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.lcm _ inst _) (@GCDMonoid.lcm _ inst _)
mk :
  ∀ [toIsCancelMulZero_1 : IsCancelMulZero α] (gcd_1 lcm_1 : α → α → α) (gcd_dvd_left_1 : ∀ (a b : α), gcd_1 a b ∣ a)
    (gcd_dvd_right_1 : ∀ (a b : α), gcd_1 a b ∣ b) (dvd_gcd_1 : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd_1 c b)
    (gcd_mul_lcm_1 : ∀ (a b : α), Associated (gcd_1 a b * lcm_1 a b) (a * b))
    (lcm_zero_left_1 : ∀ (a : α), lcm_1 0 a = 0) (lcm_zero_right_1 : ∀ (a : α), lcm_1 a 0 = 0)
    (hgcd : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.gcd _ inst _) (@GCDMonoid.gcd _ inst _))
    (hlcm : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.lcm _ inst _) (@GCDMonoid.lcm _ inst _)),
    { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
        gcd_dvd_right := gcd_dvd_right, dvd_gcd := @dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
        lcm_zero_right := lcm_zero_right : GCDMonoid α } =
      { toIsCancelMulZero := toIsCancelMulZero_1, gcd := gcd_1, lcm := lcm_1, gcd_dvd_left := gcd_dvd_left_1,
        gcd_dvd_right := gcd_dvd_right_1, dvd_gcd := @dvd_gcd_1, gcd_mul_lcm := gcd_mul_lcm_1,
        lcm_zero_left := lcm_zero_left_1, lcm_zero_right := lcm_zero_right_1 }
⊢ { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
      gcd_dvd_right := gcd_dvd_right, dvd_gcd := @dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
      lcm_zero_right := lcm_zero_right : GCDMonoid α } =
    g₂

Tactic:
cases g₂
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
toIsCancelMulZero : IsCancelMulZero α
gcd lcm : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)
lcm_zero_left : ∀ (a : α), lcm 0 a = 0
lcm_zero_right : ∀ (a : α), lcm a 0 = 0
toIsCancelMulZero_1 : IsCancelMulZero α
gcd_1 lcm_1 : α → α → α
gcd_dvd_left_1 : ∀ (a b : α), gcd_1 a b ∣ a
gcd_dvd_right_1 : ∀ (a b : α), gcd_1 a b ∣ b
dvd_gcd_1 : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd_1 c b
gcd_mul_lcm_1 : ∀ (a b : α), Associated (gcd_1 a b * lcm_1 a b) (a * b)
lcm_zero_left_1 : ∀ (a : α), lcm_1 0 a = 0
lcm_zero_right_1 : ∀ (a : α), lcm_1 a 0 = 0
hgcd : gcd = gcd_1
hlcm : lcm = lcm_1
⊢ { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
      gcd_dvd_right := gcd_dvd_right, dvd_gcd := @dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
      lcm_zero_right := lcm_zero_right : GCDMonoid α } =
    { toIsCancelMulZero := toIsCancelMulZero_1, gcd := gcd_1, lcm := lcm_1, gcd_dvd_left := gcd_dvd_left_1,
      gcd_dvd_right := gcd_dvd_right_1, dvd_gcd := @dvd_gcd_1, gcd_mul_lcm := gcd_mul_lcm_1,
      lcm_zero_left := lcm_zero_left_1, lcm_zero_right := lcm_zero_right_1 }

Tactic:
simp only [hgcd, hlcm]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a b : NormalizedGCDMonoid α
mk :
  ∀ [toNormalizationMonoid : NormalizationMonoid α] [toGCDMonoid : GCDMonoid α]
    (normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
    (normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
    { toNormalizationMonoid := toNormalizationMonoid, toGCDMonoid := toGCDMonoid, normalize_gcd := normalize_gcd,
        normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
      b
⊢ a = b

Tactic:
cases a
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
b : NormalizedGCDMonoid α
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
mk :
  ∀ [toNormalizationMonoid : NormalizationMonoid α] [toGCDMonoid : GCDMonoid α]
    (normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
    (normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
        normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
      { toNormalizationMonoid := toNormalizationMonoid, toGCDMonoid := toGCDMonoid, normalize_gcd := normalize_gcd_1,
        normalize_lcm := normalize_lcm_1 }
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    b

Tactic:
cases b
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ a_gcd = b_gcd

Tactic:
have := Subsingleton.elim a_gcd b_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
this : a_gcd = b_gcd
mk :
  ∀ (normalize_gcd_2 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
    (normalize_lcm_2 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
        normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
      { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_2,
        normalize_lcm := normalize_lcm_2 }
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := b_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }

Tactic:
subst this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ a_norm = b_norm

Tactic:
have := Subsingleton.elim a_norm b_norm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
this : a_norm = b_norm
mk :
  ∀ (normalize_gcd_2 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
    (normalize_lcm_2 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
        normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
      { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_2,
        normalize_lcm := normalize_lcm_2 }
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }

Tactic:
subst this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }

Tactic:
rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
x : α
⊢ Eq (α := αˣ) (normUnit x) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
x : α
⊢ (normalize : (a : α) → α) x = x

Tactic:
mul_one x

Premises used: mul_one
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a c
hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c

Tactic:
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)

Premises used: dvd_antisymm_of_normalize_eq, normalize_gcd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a c

Tactic:
rw [dvd_gcd_iff]

Premises used: dvd_gcd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b

Tactic:
rw [dvd_gcd_iff]

Premises used: dvd_gcd_iff
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
⟨gcd_dvd_left _ _, ?_⟩

Premises used: And.intro, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
refine ⟨gcd_dvd_left _ _, ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
⟨gcd_dvd_left _ _, ?_⟩

Premises used: And.intro, GCDMonoid.gcd_dvd_left