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
⊢ a ∣ lcm a b

Tactic:
apply dvd_lcm_left
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
pos : ∀ (h : c = 0), a ∣ (normalize : (a : α) → α) b
pos₁ : ∀ (h : ¬c = 0) (h_1 : b = 0), a ∣ (normalize : (a : α) → α) c
neg :
  ∀ (h : ¬c = 0) (h_1 : ¬b = 0),
    a ∣ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (c * b) = lcm c b * x) ⋯
⊢ a ∣
    if c = 0 then (normalize : (a : α) → α) b
    else
      if b = 0 then (normalize : (a : α) → α) c
      else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (c * b) = lcm c b * x) ⋯

Tactic:
split_ifs with h h_1
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : c = 0
⊢ a ∣ (normalize : (a : α) → α) b

Tactic:
apply dvd_normalize_iff.2 ab

Premises used: Iff.mpr, dvd_normalize_iff
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ (normalize : (a : α) → α) c

Tactic:
apply dvd_normalize_iff.2 ac

Premises used: Iff.mpr, dvd_normalize_iff
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
⊢ lcm c b ∣ c * b

Tactic:
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h_2 : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h : lcm c b ∣ c * b
⊢ c = 0 ∨ b = 0

Tactic:
rw [con, zero_dvd_iff, mul_eq_zero] at h

Premises used: zero_dvd_iff, mul_eq_zero
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h_2 : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h : c = 0 ∨ b = 0
inl : c = 0 → False
inr : b = 0 → False
⊢ False

Tactic:
cases h
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h_2 : c = 0
⊢ False

Tactic:
absurd ‹c = 0› h

Premises used: absurd
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h_2 : c = 0
⊢ False

Tactic:
exact absurd ‹c = 0› h

Premises used: absurd
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h_2 : b = 0
⊢ False

Tactic:
absurd ‹b = 0› h_1

Premises used: absurd
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
con : lcm c b = 0
h_2 : b = 0
⊢ False

Tactic:
exact absurd ‹b = 0› h_1

Premises used: absurd
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
⊢ lcm c b ≠ 0

Tactic:
have h0 : lcm c b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹c = 0› h
        · exact absurd ‹b = 0› h_1
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
neg : lcm c b * a ∣ c * b
⊢ a ∣ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (c * b) = lcm c b * x) ⋯

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec
        (dvd_normalize_iff.2 (lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl))),
      dvd_normalize_iff]

Premises used: Iff.mpr, Dvd.intro, Dvd.intro_left, Classical.choose_spec, mul_dvd_mul_iff_left, dvd_normalize_iff, rfl
-- 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 c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
neg : ∀ (d : α) (h_1 : ¬a * d = 0) (h0 : lcm c (a * d) ≠ 0), lcm c (a * d) * a ∣ c * (a * d)
⊢ lcm c b * a ∣ c * b

Tactic:
rcases ab with ⟨d, rfl⟩

Premises used: rfl
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
⊢ ¬(a = 0 ∨ d = 0)

Tactic:
rw [mul_eq_zero] at h_1

Premises used: mul_eq_zero
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
h_1₁ : ¬(a = 0 ∨ d = 0)
⊢ lcm c (a * d) ≠ 0

Tactic:
rw [mul_eq_zero] at h_1

Premises used: mul_eq_zero
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬(a = 0 ∨ d = 0)
h0 : lcm c (a * d) ≠ 0
⊢ a ≠ 0 ∧ d ≠ 0

Tactic:
push Not at h_1

Premises used: Not
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
neg : lcm c (d * a) ∣ c * d
⊢ lcm c (a * d) * a ∣ c * (a * d)

Tactic:
rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]

Premises used: mul_dvd_mul_iff_right, mul_assoc, And.left, mul_comm
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
neg : d * a ∣ c * d
⊢ lcm c (d * a) ∣ c * d

Tactic:
apply lcm_dvd (Dvd.intro d rfl)

Premises used: Dvd.intro, rfl
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
neg : a ∣ c
⊢ d * a ∣ c * d

Tactic:
rw [mul_comm, mul_dvd_mul_iff_right h_1.2]

Premises used: mul_dvd_mul_iff_right, And.right, mul_comm
-- 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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ a ∣ c

Tactic:
apply ac
-- 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 : α
pos : ∀ (h : a = 0), Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) b : α) (lcm a b)) (a * b)
pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (lcm a b)) (a * b)
neg :
  ∀ (h : ¬a = 0) (h_1 : ¬b = 0),
    Associated (Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ * lcm a b)
      (a * b)
⊢ Associated
    (HMul.hMul (α := α)
      (if a = 0 then (normalize : (a : α) → α) b
        else
          if b = 0 then (normalize : (a : α) → α) a
          else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ :
        α)
      (lcm a b))
    (a * b)

Tactic:
split_ifs with h h_1
-- 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
pos : Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) b : α) (lcm 0 b)) (0 * b)
pos₁ : Associated (HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) b : α) (0 : α)) (0 * b)
pos₂ : Associated 0 (0 * b)
pos₃ pos₄ : Associated.{u_1} (M := α) 0 0
⊢ Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) b : α) (lcm a b)) (a * b)

Tactic:
rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, eq_zero_of_zero_dvd
-- 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
pos : Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (lcm a 0)) (a * 0)
pos₁ : Associated (HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) a : α) (0 : α)) (a * 0)
pos₂ : Associated 0 (a * 0)
pos₃ pos₄ : Associated.{u_1} (M := α) 0 0
⊢ Associated (HMul.hMul (α := α) ((normalize : (a : α) → α) a : α) (lcm a b)) (a * b)

Tactic:
rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _), mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, eq_zero_of_zero_dvd
-- 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
neg : Associated ((normalize : (a : α) → α) (a * b)) (a * b)
⊢ Associated (Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ * lcm a b) (a * b)

Tactic:
rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]

Premises used: Classical.choose_spec, mul_comm
-- 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
⊢ Associated ((normalize : (a : α) → α) (a * b)) (a * b)

Tactic:
normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- 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
⊢ Associated ((normalize : (a : α) → α) (a * b)) (a * b)

Tactic:
exact normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- 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 : α
dsimp :
  (if a = 0 then b * (↑(normUnit b) : α)
      else
        if b = 0 then a * (↑(normUnit a) : α)
        else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯) *
      (↑(normUnit
            (if a = 0 then b * (↑(normUnit b) : α)
            else
              if b = 0 then a * (↑(normUnit a) : α)
              else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) :
        α) =
    if a = 0 then b * (↑(normUnit b) : α)
    else
      if b = 0 then a * (↑(normUnit a) : α)
      else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯
⊢ Eq (α := α)
    ((normalize : (a : α) → α)
        (if a = 0 then (normalize : (a : α) → α) b
          else
            if b = 0 then (normalize : (a : α) → α) a
            else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ :
          α) :
      α)
    (if a = 0 then (normalize : (a : α) → α) b
      else
        if b = 0 then (normalize : (a : α) → α) a
        else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ :
      α)

Tactic:
dsimp [normalize]

Premises used: normalize
-- 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 : α
pos : ∀ (h : a = 0), b * (↑(normUnit b) : α) * (↑(normUnit (b * (↑(normUnit b) : α))) : α) = b * (↑(normUnit b) : α)
pos₁ :
  ∀ (h : ¬a = 0) (h_1 : b = 0),
    a * (↑(normUnit a) : α) * (↑(normUnit (a * (↑(normUnit a) : α))) : α) = a * (↑(normUnit a) : α)
neg :
  ∀ (h : ¬a = 0) (h_1 : ¬b = 0),
    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) ⋯
⊢ (if a = 0 then b * (↑(normUnit b) : α)
      else
        if b = 0 then a * (↑(normUnit a) : α)
        else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯) *
      (↑(normUnit
            (if a = 0 then b * (↑(normUnit b) : α)
            else
              if b = 0 then a * (↑(normUnit a) : α)
              else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯)) :
        α) =
    if a = 0 then b * (↑(normUnit b) : α)
    else
      if b = 0 then a * (↑(normUnit a) : α)
      else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = lcm a b * x) ⋯

Tactic:
split_ifs with h h_1
-- 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
⊢ b * (↑(normUnit b) : α) * (↑(normUnit (b * (↑(normUnit b) : α))) : α) = b * (↑(normUnit b) : α)

Tactic:
apply normalize_idem

Premises used: normalize_idem
-- 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
⊢ a * (↑(normUnit a) : α) * (↑(normUnit (a * (↑(normUnit a) : α))) : α) = a * (↑(normUnit a) : α)

Tactic:
apply normalize_idem

Premises used: normalize_idem