awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ a
have neg : b ∣ lcm a b
Tactic: rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), mul_comm,
        mul_dvd_mul_iff_right h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : α
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) ∣ b
have pos : ∀ (h : a = 0), b ∣ b
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) ∣ b
have pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), a ∣ b
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) ∣ b
have neg : ∀ (h : ¬a = 0) (h_1 : ¬b = 0), Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) sorry ∣ b
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 ∣ b
have pos : a ∣ 0
Tactic: rw [h_1]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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
⊢ Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ b
have h0 : 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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ ∣ b
have neg : a ∣ lcm a b
Tactic: rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_dvd_mul_iff_right h_1]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ a ∣ if c = 0 then b else if b = 0 then c else Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
have pos : ∀ (h : c = 0), a ∣ b
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ a ∣ if c = 0 then b else if b = 0 then c else Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
have pos₁ : ∀ (h : ¬c = 0) (h_1 : b = 0), a ∣ c
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ a ∣ if c = 0 then b else if b = 0 then c else Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
have neg : ∀ (h : ¬c = 0) (h_1 : ¬b = 0), a ∣ Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) sorry
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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
⊢ False
have h₁ : lcm c b ∣ c * b
Tactic: have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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
⊢ False
have h₁ : c = 0 ∨ b = 0
Tactic: rw [con, zero_dvd_iff, mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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 ∣ Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
have h0 : 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
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
h0 : lcm c b ≠ 0
⊢ a ∣ Classical.choose (p := fun (x : α) ↦ c * b = lcm c b * x) ⋯
have neg : lcm c b * a ∣ c * b
Tactic: rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ c * b
have neg : ∀ (d : α) (h_1 : ¬a * d = 0) (h0 : lcm c (a * d) ≠ 0), lcm c (a * d) * a ∣ c * (a * d)
Tactic: rcases ab with ⟨d, rfl⟩
Cleared hypotheses: b, ab, h_1, h0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬a * d = 0
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
have h_1₁ : ¬(a = 0 ∨ d = 0)
Tactic: rw [mul_eq_zero] at ‹a * d ≠ 0›
Cleared hypotheses: h_1, h0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h_1 : ¬(a = 0 ∨ d = 0)
h0 : lcm c (a * d) ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
have h_1₁ : a ≠ 0 ∧ d ≠ 0
Tactic: push Not at h_1
Cleared hypotheses: h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (a * d) * a ∣ c * (a * d)
have neg : lcm c (d * a) ∣ c * d
Tactic: rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 c : α
ac : a ∣ c
h : ¬c = 0
d : α
h0 : lcm c (a * d) ≠ 0
h_1 : a ≠ 0 ∧ d ≠ 0
⊢ lcm c (d * a) ∣ c * d
have neg : d * a ∣ c * d
Tactic: apply lcm_dvd (Dvd.intro d rfl)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : α
⊢ Associated
    ((if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) * lcm a b)
    (a * b)
have pos : ∀ (h : a = 0), Associated (b * lcm a b) (a * b)
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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), Associated (b * lcm a b) (a * b)
⊢ Associated
    ((if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) * lcm a b)
    (a * b)
have pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), Associated (a * lcm a b) (a * b)
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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), Associated (b * lcm a b) (a * b)
pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), Associated (a * lcm a b) (a * b)
⊢ Associated
    ((if a = 0 then b else if b = 0 then a else Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) * lcm a b)
    (a * b)
have neg : ∀ (h : ¬a = 0) (h_1 : ¬b = 0),
  Associated (Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) sorry * lcm a b) (a * b)
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ Associated (b * lcm a b) (a * b)
have pos : Associated (b * lcm 0 b) (0 * b)
Tactic: rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : Associated (b * lcm 0 b) (0 * b)
⊢ Associated (b * lcm a b) (a * b)
have pos₁ : Associated (b * 0) (0 * b)
Tactic: rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : Associated (b * lcm 0 b) (0 * b)
pos₁ : Associated (b * 0) (0 * b)
⊢ Associated (b * lcm a b) (a * b)
have pos₂ : Associated 0 (0 * b)
Tactic: rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : Associated (b * lcm 0 b) (0 * b)
pos₁ : Associated (b * 0) (0 * b)
pos₂ : Associated 0 (0 * b)
⊢ Associated (b * lcm a b) (a * b)
have pos₃ : Associated.{u_1} (M := α) 0 0
Tactic: rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ Associated (a * lcm a b) (a * b)
have pos : Associated (a * lcm a 0) (a * 0)
Tactic: rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : Associated (a * lcm a 0) (a * 0)
⊢ Associated (a * lcm a b) (a * b)
have pos₁ : Associated (a * 0) (a * 0)
Tactic: rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ Associated (Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ * lcm a b) (a * b)
have neg : Associated (lcm a b * Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) sorry) (a * b)
Tactic: rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
neg : Associated (lcm a b * Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯) (a * b)
⊢ Associated (Classical.choose (p := fun (x : α) ↦ a * b = lcm a b * x) ⋯ * lcm a b) (a * b)
have neg₁ : Associated (a * b) (a * b)
Tactic: rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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 : α
⊢ (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) ⋯) ∣
    a
have pos : ∀ (h : a = 0), (normalize : (a : α) → α) b ∣ a
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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), (normalize : (a : α) → α) b ∣ 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) ⋯) ∣
    a
have pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), (normalize : (a : α) → α) a ∣ a
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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), (normalize : (a : α) → α) b ∣ a
pos₁ : ∀ (h : ¬a = 0) (h_1 : b = 0), (normalize : (a : α) → α) a ∣ 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) ⋯) ∣
    a
have neg : ∀ (h : ¬a = 0) (h_1 : ¬b = 0),
  Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) sorry ∣ a
Tactic: split_ifs with h h_1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ (normalize : (a : α) → α) b ∣ a
have pos : Dvd.dvd (α := α) ((normalize : (a : α) → α) b : α) (0 : α)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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
con : lcm a b = 0
⊢ False
have h₁ : lcm a b ∣ a * b
Tactic: have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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_2 : ¬a = 0
h_1 : ¬b = 0
con : lcm a b = 0
h : lcm a b ∣ a * b
⊢ False
have h₁ : a = 0 ∨ b = 0
Tactic: rw [con, zero_dvd_iff, mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
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
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = lcm a b * x) ⋯ ∣ a
have h0 : 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