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 α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
⊢ a * b ≠ 0

Tactic:
have hab : a * b ≠ 0 := mul_ne_zero a0 hb
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
hab : a * b ≠ 0
contrapose : ∀ (hab : gcd a b = 0), a * b = 0
⊢ gcd a b ≠ 0

Tactic:
contrapose hab
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
hab : gcd a b = 0
rw : Eq (α := α) ((normalize : (a : α) → α) (a * b) : α) (0 : α)
rw₁ : gcd a b * l = 0
rw₂ : 0 * l = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) 0 0
⊢ a * b = 0

Tactic:
rw [← normalize_eq_zero, ← this, hab, zero_mul]

Premises used: MulZeroClass.zero_mul, normalize_eq_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
⊢ gcd a b ≠ 0

Tactic:
have h1 : gcd a b ≠ 0 := by
          have hab : a * b ≠ 0 := mul_ne_zero a0 hb
          contrapose hab
          rw [← normalize_eq_zero, ← this, hab, zero_mul]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
rw :
  Eq (α := α) ((normalize : (a : α) → α) ((normalize : (a : α) → α) (a * b) : α) : α)
    ((normalize : (a : α) → α) (a * b) : α)
rw₁ rw₂ : Eq (α := α) ((normalize : (a : α) → α) (a * b) : α) ((normalize : (a : α) → α) (a * b) : α)
⊢ (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l

Tactic:
rw [this, 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 α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
⊢ (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l

Tactic:
have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
h2 : (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l
⊢ HMul.hMul (α := α) ((normalize : (a : α) → α) (gcd a b) : α) l = (normalize : (a : α) → α) (a * b)

Tactic:
rw [← normalize_gcd] at this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
h2 : (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l
this₁ : HMul.hMul (α := α) ((normalize : (a : α) → α) (gcd a b) : α) l = (normalize : (a : α) → α) (a * b)
⊢ b ≠ 0

Tactic:
rw [← normalize_gcd] at this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
h2 : (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l
this₁ : HMul.hMul (α := α) ((normalize : (a : α) → α) (gcd a b) : α) l = (normalize : (a : α) → α) (a * b)
hb₁ : b ≠ 0
⊢ gcd a b ≠ 0

Tactic:
rw [← normalize_gcd] at this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : gcd a b * l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
h2 : (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l
this₁ : HMul.hMul (α := α) ((normalize : (a : α) → α) (gcd a b) : α) l = (normalize : (a : α) → α) (a * b)
hb₁ : b ≠ 0
h1₁ : gcd a b ≠ 0
⊢ (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l

Tactic:
rw [← normalize_gcd] at this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
gcd : α → α → α
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
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
this : HMul.hMul (α := α) ((normalize : (a : α) → α) (gcd a b) : α) l = (normalize : (a : α) → α) (a * b)
hb : b ≠ 0
h1 : gcd a b ≠ 0
h2 : (normalize : (a : α) → α) (gcd a b * l) = gcd a b * l
neg :
  ∀
    (h2 :
      HMul.hMul (α := α) (β := α) ((normalize : (a : α) → α) (gcd a b) : α) ((normalize : (a : α) → α) l : α) =
        gcd a b * l),
    l * (↑(normUnit l) : α) = l
neg₁ :
  ∀ (h2 : HMul.hMul (β := α) (gcd a b) ((normalize : (a : α) → α) l : α) = gcd a b * l), l * (↑(normUnit l) : α) = l
neg₂ neg₃ neg₄ neg₅ : ∀ (h2 : (normalize : (a : α) → α) l = l), l * (↑(normUnit l) : α) = l
⊢ l * (↑(normUnit l) : α) = l

Tactic:
rwa [normalize.map_mul, normalize_gcd, mul_right_inj' h1] at h2

Premises used: mul_right_inj', normalize, MonoidWithZeroHom.map_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
pos : ∀ (h : a = 0), b ∣ a
pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), a ∣ a
neg : ∀ (h : ¬a = 0) (h_1 : ¬b = 0), Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ a
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) ∣ a

Tactic:
split_ifs with h h_1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : a = 0
pos : b ∣ 0
⊢ b ∣ a

Tactic:
rw [h]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : a = 0
⊢ b ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ a ∣ a

Tactic:
dvd_rfl

Premises used: dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ a ∣ a

Tactic:
exact dvd_rfl

Premises used: dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
⊢ lcm a b ∣ a * b

Tactic:
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h_2 : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
h : lcm a b ∣ a * b
⊢ a = 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h_2 : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
h : a = 0 ∨ b = 0
inl : a = 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
h_2 : a = 0
⊢ False

Tactic:
absurd ‹a = 0› h

Premises used: absurd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
h_2 : a = 0
⊢ False

Tactic:
exact absurd ‹a = 0› h

Premises used: absurd
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
con : lcm a 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
con : lcm a 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ lcm a b ≠ 0

Tactic:
have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg : b ∣ lcm a b
⊢ Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ a

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

Premises used: mul_dvd_mul_iff_right, Classical.choose_spec, mul_dvd_mul_iff_left, mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
⊢ b ∣ lcm a b

Tactic:
apply dvd_lcm_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
pos : ∀ (h : a = 0), b ∣ b
pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), a ∣ b
neg : ∀ (h : ¬a = 0) (h_1 : ¬b = 0), Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ b
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) ∣ b

Tactic:
split_ifs with h h_1
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : a = 0
⊢ b ∣ b

Tactic:
dvd_rfl

Premises used: dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : a = 0
⊢ b ∣ b

Tactic:
exact dvd_rfl

Premises used: dvd_rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
pos : a ∣ 0
⊢ a ∣ b

Tactic:
rw [h_1]
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ a ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
h0 : lcm a b ≠ 0
neg : a ∣ lcm a b
⊢ Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ b

Tactic:
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_dvd_mul_iff_right h_1]

Premises used: mul_dvd_mul_iff_right, Classical.choose_spec, mul_dvd_mul_iff_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
pos : ∀ (h : c = 0), a ∣ b
pos₁ : ∀ (h : ¬c = 0) (h_1 : b = 0), a ∣ c
neg : ∀ (h : ¬c = 0) (h_1 : ¬b = 0), a ∣ Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
⊢ a ∣ if c = 0 then b else if b = 0 then c else Classical.choose (p := fun (x : α) ↦ 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : c = 0
⊢ a ∣ b

Tactic:
ab
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : c = 0
⊢ a ∣ b

Tactic:
exact ab
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ c

Tactic:
ac
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : b = 0
⊢ a ∣ c

Tactic:
exact ac
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ 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 : 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
exists_gcd : ∀ (a b : α), lcm a b ∣ 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