awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg :
  lcm a b *
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    lcm a b * Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯
⊢ Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
      (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α) =
    Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯

Tactic:
apply mul_left_cancel₀ h0

Premises used: mul_left_cancel₀
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ lcm a b *
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    lcm a b * Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯

Tactic:
_root_.trans ?_ (Classical.choose_spec (exists_gcd a b))

Premises used: trans, Classical.choose_spec
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg :
  lcm a b *
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    (normalize : (a : α) → α) (a * b)
⊢ lcm a b *
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    lcm a b * Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯

Tactic:
refine _root_.trans ?_ (Classical.choose_spec (exists_gcd a b))

Premises used: trans, Classical.choose_spec
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
a₁ : lcm a b
a₂ :
  Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
    (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)
| lcm a b *
    (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
      (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α))

Tactic:
congr
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
a₁ : ((normalize : (a : α) → α) (lcm a b) : α)
| lcm a b

Tactic:
rw [← normalize_lcm a b]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
a₁ : ((normalize : (a : α) → α) (lcm a b) : α)
a₂ :
  Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
    (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)
| lcm a b *
    (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
      (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α))

Tactic:
congr
        rw [← normalize_lcm a b]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg :
  HMul.hMul (α := α) ((normalize : (a : α) → α) (lcm a b) : α)
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    (normalize : (a : α) → α) (a * b)
⊢ lcm a b *
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    (normalize : (a : α) → α) (a * b)

Tactic:
conv_lhs =>
        congr
        rw [← normalize_lcm a b]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ (normalize : (a : α) → α) (a * b) := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg :
  HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) (lcm a b) : α)
      ((normalize : (a : α) → α)
          (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯) :
        α) =
    (normalize : (a : α) → α) (a * b)
neg₁ :
  Eq (α := α)
    ((normalize : (a : α) → α)
        (lcm a b * Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯) :
      α)
    ((normalize : (a : α) → α) (a * b) : α)
neg₂ :
  Eq (α := α) ((normalize : (a : α) → α) ((normalize : (a : α) → α) (a * b) : α) : α)
    ((normalize : (a : α) → α) (a * b) : α)
neg₃ neg₄ : Eq (α := α) ((normalize : (a : α) → α) (a * b) : α) ((normalize : (a : α) → α) (a * b) : α)
⊢ HMul.hMul (α := α) ((normalize : (a : α) → α) (lcm a b) : α)
      (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯ *
        (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) : α)) =
    (normalize : (a : α) → α) (a * b)

Tactic:
rw [← normalize_apply, ← normalize.map_mul,
        ← Classical.choose_spec (exists_gcd a b), normalize_idem]

Premises used: normalize_apply, Classical.choose_spec, normalize, MonoidWithZeroHom.map_mul, normalize_idem
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
x y : G₀
x0 : x ≠ 0
y0 : y ≠ 0
⊢ (↑(if h : x * y = 0 then 1 else (Units.mk0 (x * y) h)⁻¹) : G₀) =
    (↑(HMul.hMul (α := G₀ˣ) (if h : x = 0 then 1 else (Units.mk0 x h)⁻¹) (if h : y = 0 then 1 else (Units.mk0 y h)⁻¹)) :
      G₀)

Tactic:
simp [x0, y0, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
u : G₀ˣ
⊢ (if h : (↑u : G₀) = 0 then 1 else (Units.mk0 (↑u : G₀) h)⁻¹) = u⁻¹

Tactic:
simp
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ a

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
⊢ (if a = 0 ∧ b = 0 then 0 else 1) ∣ b

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b c : G₀
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ if c = 0 ∧ b = 0 then 0 else 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
pos : a = 0 ∧ b = 0 → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 0 0) (a * b)
neg : a = 0 ∧ b = 0 → ¬(a = 0 ∨ b = 0) → Associated (HMul.hMul (α := G₀) 0 1) (a * b)
pos₁ : ¬(a = 0 ∧ b = 0) → a = 0 ∨ b = 0 → Associated (HMul.hMul (α := G₀) 1 0) (a * b)
neg₁ : ¬(a = 0 ∧ b = 0) → ¬(a = 0 ∨ b = 0) → Associated (HMul.hMul (α := G₀) 1 1) (a * b)
⊢ Associated (HMul.hMul (α := G₀) (if a = 0 ∧ b = 0 then 0 else 1) (if a = 0 ∨ b = 0 then 0 else 1)) (a * b)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : a = 0 ∧ b = 0
h_1 : a = 0 ∨ b = 0
⊢ Associated (HMul.hMul (α := G₀) 0 0) (a * b)

Tactic:
simp_all [Associated.comm]

Premises used: Associated.comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : a = 0 ∧ b = 0
h_1 : ¬(a = 0 ∨ b = 0)
⊢ Associated (HMul.hMul (α := G₀) 0 1) (a * b)

Tactic:
simp_all [Associated.comm]

Premises used: Associated.comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : ¬(a = 0 ∧ b = 0)
h_1 : a = 0 ∨ b = 0
⊢ Associated (HMul.hMul (α := G₀) 1 0) (a * b)

Tactic:
simp_all [Associated.comm]

Premises used: Associated.comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : ¬(a = 0 ∧ b = 0)
h_1 : ¬(a = 0 ∨ b = 0)
⊢ Associated (HMul.hMul (α := G₀) 1 1) (a * b)

Tactic:
simp_all [Associated.comm]

Premises used: Associated.comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : a = 0 ∧ b = 0
⊢ Eq.{u_2 + 1} (α := G₀) ((normalize : (a : G₀) → G₀) (if a = 0 ∧ b = 0 then 0 else 1) : G₀)
    (if a = 0 ∧ b = 0 then 0 else 1 : G₀)

Tactic:
simp [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : ¬(a = 0 ∧ b = 0)
⊢ Eq.{u_2 + 1} (α := G₀) ((normalize : (a : G₀) → G₀) (if a = 0 ∧ b = 0 then 0 else 1) : G₀)
    (if a = 0 ∧ b = 0 then 0 else 1 : G₀)

Tactic:
simp [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : a = 0 ∨ b = 0
⊢ Eq.{u_2 + 1} (α := G₀) ((normalize : (a : G₀) → G₀) (if a = 0 ∨ b = 0 then 0 else 1) : G₀)
    (if a = 0 ∨ b = 0 then 0 else 1 : G₀)

Tactic:
simp [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a b : G₀
h : ¬(a = 0 ∨ b = 0)
⊢ Eq.{u_2 + 1} (α := G₀) ((normalize : (a : G₀) → G₀) (if a = 0 ∨ b = 0 then 0 else 1) : G₀)
    (if a = 0 ∨ b = 0 then 0 else 1 : G₀)

Tactic:
simp [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ (↑(normUnit a) : G₀) = a⁻¹

Tactic:
simp [normUnit, h0]

Premises used: NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
G₀ : Type u_2
inst : CommGroupWithZero G₀
inst_1 : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ Eq (α := G₀) ((normalize : (a : G₀) → G₀) a : G₀) (1 : G₀)

Tactic:
simp [normalize_apply, h0]

Premises used: normalize_apply
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ Dvd.dvd (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)

Tactic:
mk_le_mk_of_dvd (gcd_dvd_left _ _)

Premises used: Quotient.map₂, Associates.mk_le_mk_of_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ Dvd.dvd (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)

Tactic:
exact mk_le_mk_of_dvd (gcd_dvd_left _ _)

Premises used: Associates.mk_le_mk_of_dvd, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ Dvd.dvd (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)

Tactic:
mk_le_mk_of_dvd (gcd_dvd_right _ _)

Premises used: Quotient.map₂, Associates.mk_le_mk_of_dvd, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ Dvd.dvd (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)

Tactic:
exact mk_le_mk_of_dvd (gcd_dvd_right _ _)

Premises used: Associates.mk_le_mk_of_dvd, GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
c_1 : Associates α
c : α
hac :
  Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) c)
hbc :
  Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)
⊢ Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) c) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))

Tactic:
mk_le_mk_of_dvd (dvd_gcd (dvd_of_mk_le_mk hac) (dvd_of_mk_le_mk hbc))

Premises used: Associates.dvd_of_mk_le_mk, Quotient.map₂, GCDMonoid.dvd_gcd, Associates.mk_le_mk_of_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
c_1 : Associates α
c : α
hac :
  Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) c)
hbc :
  Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)
⊢ Dvd.dvd (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) c) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))

Tactic:
exact mk_le_mk_of_dvd (dvd_gcd (dvd_of_mk_le_mk hac) (dvd_of_mk_le_mk hbc))

Premises used: Associates.dvd_of_mk_le_mk, GCDMonoid.dvd_gcd, Associates.mk_le_mk_of_dvd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
mk :
  HMul.hMul (α := Associates α)
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)) =
    HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)
⊢ Associated
    (HMul.hMul (α := Associates α)
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)))
    (HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))

Tactic:
rw [associated_iff_eq]

Premises used: associated_iff_eq
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ HMul.hMul (α := Associates α)
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)) =
    HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)

Tactic:
Quotient.sound <| gcd_mul_lcm _ _

Premises used: gcd_mul_lcm, Quotient.map₂, Quotient.sound
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
b_1 : Associates α
b : α
⊢ HMul.hMul (α := Associates α)
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@gcd _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b))
      (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
        (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)) =
    HMul.hMul (α := Associates α) (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a)
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) b)

Tactic:
exact Quotient.sound <| gcd_mul_lcm _ _

Premises used: gcd_mul_lcm, Quotient.sound
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
⊢ Eq (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯ 0
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a))
    0

Tactic:
congr_arg Associates.mk <| lcm_zero_left _

Premises used: Associates.mk, Quotient.map₂, congr_arg, GCDMonoid.lcm_zero_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
⊢ Eq (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯ 0
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a))
    0

Tactic:
exact congr_arg Associates.mk <| lcm_zero_left _

Premises used: Associates.mk, congr_arg, GCDMonoid.lcm_zero_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
⊢ Eq (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) 0)
    0

Tactic:
congr_arg Associates.mk <| lcm_zero_right _

Premises used: GCDMonoid.lcm_zero_right, Associates.mk, Quotient.map₂, congr_arg
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a_1 : Associates α
a : α
⊢ Eq (α := Associates α)
    (Quotient.map₂ (sa := Associated.setoid α) (sb := Associated.setoid α) (@lcm _ inst _) ⋯
      (Quot.mk (⇑(Associated.setoid α) : α → α → Prop) a) 0)
    0

Tactic:
exact congr_arg Associates.mk <| lcm_zero_right _

Premises used: GCDMonoid.lcm_zero_right, Associates.mk, congr_arg
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ Eq (α := Associates α) (@gcd _ instCommMonoidWithZero _ (Associates.mk a) (Associates.mk b))
    (Associates.mk (@gcd _ inst _ a b))

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
⊢ Eq (α := Associates α) (@lcm _ instCommMonoidWithZero _ (Associates.mk a) (Associates.mk b))
    (Associates.mk (@lcm _ inst _ a b))

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ s.lcm f = (Multiset.map f s.val).lcm

Tactic:
rfl

Premises used: Finset.lcm, Multiset.lcm, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Finset
Goal:
α : Type u_2
β : Type u_3
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
f : β → α
⊢ lcm ∅ f = 1

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.lcm, List.foldr, rfl, Multiset.fold