awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
⊢ @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')
have h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x (@gcd _ inst _ x y * y')
Tactic: rw [← ex, ← ey, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x (@gcd _ inst _ x y * y')
⊢ @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')
have h₂ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x y
Tactic: rw [← ex, ← ey, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y x' y' : α
ex : x = @gcd _ inst _ x y * x'
ey : y = @gcd _ inst _ x y * y'
h : @gcd _ inst _ x y ≠ 0
h₁ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x (@gcd _ inst _ x y * y')
h₂ : @gcd _ inst _ x y * 1 = @gcd _ inst _ x y
⊢ @gcd _ inst _ x y * 1 = @gcd _ inst _ (@gcd _ inst _ x y * x') (@gcd _ inst _ x y * y')
have h₃ : @gcd _ inst _ x y = @gcd _ inst _ x y
Tactic: rw [← ex, ← ey, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
have pos : ∀ (h : @gcd _ inst _ x y = 0),
  ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
Tactic: by_cases h : gcd x y = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
pos :
  ∀ (h : @gcd _ inst _ x y = 0),
    ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
have neg : ∀ (h : ¬@gcd _ inst _ x y = 0),
  ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
Tactic: by_cases h : gcd x y = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : @gcd _ inst _ x y = 0
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
have pos : ∀ (h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0),
  ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ IsUnit (@gcd _ inst _ x' y')
Tactic: obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
⊢ ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ IsUnit (@gcd _ inst _ x' y')
have pos : ∃ (x' : α), ∃ (y' : α), 0 = @gcd _ inst _ 0 0 * x' ∧ 0 = @gcd _ inst _ 0 0 * y' ∧ Associated (@gcd _ inst _ x' y') 1
Tactic: simp_rw [← associated_one_iff_isUnit]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
⊢ 0 = HMul.hMul (α := α) (@gcd _ inst _ 0 0) 1
have rw : 0 = HMul.hMul (α := α) 0 1
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
h : Eq.{u_2 + 1} (α := α) (@gcd _ inst _ 0 0) 0
rw : 0 = HMul.hMul (α := α) 0 1
⊢ 0 = HMul.hMul (α := α) (@gcd _ inst _ 0 0) 1
have rw₁ : Eq.{u_2 + 1} (α := α) 0 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
have neg : ∀ (x' : α) (ex : x = @gcd _ inst _ x y * x'),
  ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
Tactic: obtain ⟨x', ex⟩ := gcd_dvd_left x y
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
h : ¬@gcd _ inst _ x y = 0
x' : α
ex : x = @gcd _ inst _ x y * x'
⊢ ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
have neg : ∀ (y' : α) (ey : y = @gcd _ inst _ x y * y'),
  ∃ (x' : α), ∃ (y' : α), x = @gcd _ inst _ x y * x' ∧ y = @gcd _ inst _ x y * y' ∧ IsUnit (@gcd _ inst _ x' y')
Tactic: obtain ⟨y', ey⟩ := gcd_dvd_right x y
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
hx : Irreducible x
⊢ IsUnit (@gcd _ inst _ x y) ↔ ¬x ∣ y
have rw : ¬Associated x (@gcd _ inst _ x y) ↔ ¬x ∣ y
Tactic: rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
hx : Irreducible x
rw : ¬Associated x (@gcd _ inst _ x y) ↔ ¬x ∣ y
⊢ IsUnit (@gcd _ inst _ x y) ↔ ¬x ∣ y
have rw₁ : Associated x (@gcd _ inst _ x y) ↔ x ∣ y
Tactic: rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
x y : α
hx : Irreducible x
rw : ¬Associated x (@gcd _ inst _ x y) ↔ ¬x ∣ y
rw₁ : Associated x (@gcd _ inst _ x y) ↔ x ∣ y
⊢ IsUnit (@gcd _ inst _ x y) ↔ ¬x ∣ y
have rw₂ : x ∣ y ↔ x ∣ y
Tactic: rw [hx.isUnit_iff_not_associated_of_dvd (gcd_dvd_left x y), not_iff_not, associated_gcd_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ @gcd _ inst _ x y = 1 ↔ ¬x ∣ y
have rw : @gcd _ inst _ x y = 1 ↔ IsUnit (@gcd _ inst _ x y)
Tactic: rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
rw : @gcd _ inst _ x y = 1 ↔ IsUnit (@gcd _ inst _ x y)
⊢ @gcd _ inst _ x y = 1 ↔ ¬x ∣ y
have rw₁ : @gcd _ inst _ x y = 1 ↔ Eq (α := α) ((normalize : (a : α) → α) (@gcd _ inst _ x y) : α) (1 : α)
Tactic: rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
rw : @gcd _ inst _ x y = 1 ↔ IsUnit (@gcd _ inst _ x y)
rw₁ : @gcd _ inst _ x y = 1 ↔ Eq (α := α) ((normalize : (a : α) → α) (@gcd _ inst _ x y) : α) (1 : α)
⊢ @gcd _ inst _ x y = 1 ↔ ¬x ∣ y
have rw₂ : @gcd _ inst _ x y = 1 ↔ @gcd _ inst _ x y = 1
Tactic: rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have pos : ∀ (h : a = 0 ∨ b = 0), @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
Tactic: by_cases h : a = 0 ∨ b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
pos : ∀ (h : a = 0 ∨ b = 0), @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg : ∀ (h : ¬(a = 0 ∨ b = 0)), @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
Tactic: by_cases h : a = 0 ∨ b = 0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have pos : @lcm _ inst _ 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
pos : @lcm _ inst _ 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have pos₁ : @lcm _ inst _ a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c
Tactic: rcases h with (rfl | rfl)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have h1 : ¬a = 0
Tactic: obtain ⟨h1, h2⟩ := not_or.1 h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have h2 : ¬b = 0
Tactic: obtain ⟨h1, h2⟩ := not_or.1 h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have h₁ : @gcd _ inst _ a b ≠ 0
Tactic: have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₄ : a * b ∣ a * c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
neg₄ : a * b ∣ a * c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₅ : b ∣ c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
neg₄ : a * b ∣ a * c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
neg₅ : b ∣ c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₆ : b ∣ c ∧ a ∣ c ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b c : α
h_1 : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : @gcd _ inst _ a b ≠ 0
neg : @gcd _ inst _ a b * @lcm _ inst _ a b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₁ : a * b ∣ @gcd _ inst _ a b * c ↔ a ∣ c ∧ b ∣ c
neg₂ : a * b ∣ @gcd _ inst _ (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
neg₃ : a * b ∣ a * c ∧ a * b ∣ b * c ↔ a ∣ c ∧ b ∣ c
neg₄ : a * b ∣ a * c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
neg₅ : b ∣ c ∧ a * b ∣ c * b ↔ a ∣ c ∧ b ∣ c
neg₆ : b ∣ c ∧ a ∣ c ↔ a ∣ c ∧ b ∣ c
⊢ @lcm _ inst _ a b ∣ c ↔ a ∣ c ∧ b ∣ c
have neg₇ : a ∣ c ∧ b ∣ c ↔ a ∣ c ∧ b ∣ c
Tactic: rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
      (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
      mul_dvd_mul_iff_right h2, and_comm]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
⊢ Associated (@gcd _ inst _ a b * @lcm _ inst _ a b) 0
have rw : Associated (@gcd _ inst _ a b * 0) 0
Tactic: rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
rw : Associated (@gcd _ inst _ a b * 0) 0
⊢ Associated (@gcd _ inst _ a b * @lcm _ inst _ a b) 0
have rw₁ : Associated.{u_1} (M := α) 0 0
Tactic: rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
⊢ a = 0 ∨ b = 0
have this : Associated (a * b) 0
Tactic: have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : GCDMonoid α
a b : α
h : @lcm _ inst _ a b = 0
this : Associated (a * b) 0
⊢ a = 0 ∨ b = 0
have rwa : a * b = 0
Tactic: rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ @lcm _ inst _ (↑(Units.mkOfMulEqOne a c ⋯) : α) (↑(Units.mkOfMulEqOne b d ⋯) : α) = 1
have rw : Eq (α := α) ((normalize : (a : α) → α) (↑(Units.mkOfMulEqOne b d sorry) : α) : α) (1 : α)
Tactic: rw [lcm_units_coe_left, normalize_coe_units]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizedGCDMonoid α
a b : α
h : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
rw : Eq (α := α) ((normalize : (a : α) → α) (↑(Units.mkOfMulEqOne b d ⋯) : α) : α) (1 : α)
⊢ @lcm _ inst _ (↑(Units.mkOfMulEqOne a c ⋯) : α) (↑(Units.mkOfMulEqOne b d ⋯) : α) = 1
have rw₁ : Eq.{u_1 + 1} (α := α) 1 1
Tactic: rw [lcm_units_coe_left, normalize_coe_units]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
x : NormalizationMonoid α
u : α → αˣ
normUnit_zero : u 0 = 1
normUnit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → u (a * b) = u a * u b
normUnit_coe_units : ∀ (u_1 : αˣ), u (↑u_1 : α) = u_1⁻¹
⊢ { normUnit := u, normUnit_zero := normUnit_zero, normUnit_mul := @normUnit_mul,
      normUnit_coe_units := normUnit_coe_units : NormalizationMonoid α } =
    NormalizationMonoid.ofUniqueUnits
have e_normUnit : u = fun (x : α) ↦ 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
⊢ Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
have h : ∀ (a b : α), @gcd _ inst _ a b = @gcd _ inst _ a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ @gcd _ inst _ a b = @gcd _ inst _ a b
have h : @gcd _ inst _ a b ∣ @gcd _ inst _ a b
Tactic: refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
a b : α
h : @gcd _ inst _ a b ∣ @gcd _ inst _ a b
⊢ @gcd _ inst _ a b = @gcd _ inst _ a b
have h₁ : @gcd _ inst _ a b ∣ @gcd _ inst _ a b
Tactic: refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
⊢ g₁ = g₂
have hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
Tactic: have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
⊢ Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)
have h : ∀ (a b : α), @lcm _ inst _ a b = @lcm _ inst _ a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
a b : α
⊢ @lcm _ inst _ a b = @lcm _ inst _ a b
have h : @lcm _ inst _ a b ∣ @lcm _ inst _ a b
Tactic: refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
a b : α
h : @lcm _ inst _ a b ∣ @lcm _ inst _ a b
⊢ @lcm _ inst _ a b = @lcm _ inst _ a b
have h₁ : @lcm _ inst _ a b ∣ @lcm _ inst _ a b
Tactic: refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
⊢ g₁ = g₂
have hlcm : Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)
Tactic: have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
g₁ g₂ : GCDMonoid α
hgcd : Eq.{u_1 + 1} (α := α → α → α) (@gcd _ inst _) (@gcd _ inst _)
hlcm : Eq.{u_1 + 1} (α := α → α → α) (@lcm _ inst _) (@lcm _ inst _)
⊢ g₁ = g₂
have mk : ∀ [toIsCancelMulZero : IsCancelMulZero α] (gcd lcm : α → α → α) (gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a)
  (gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b) (dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b)
  (gcd_mul_lcm : ∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)) (lcm_zero_left : ∀ (a : α), lcm 0 a = 0)
  (lcm_zero_right : ∀ (a : α), lcm a 0 = 0)
  (hgcd : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.gcd _ inst _) (@GCDMonoid.gcd _ inst _))
  (hlcm : Eq.{u_1 + 1} (α := α → α → α) (@GCDMonoid.lcm _ inst _) (@GCDMonoid.lcm _ inst _)),
  { toIsCancelMulZero := toIsCancelMulZero, gcd := gcd, lcm := lcm, gcd_dvd_left := gcd_dvd_left,
      gcd_dvd_right := gcd_dvd_right, dvd_gcd := @dvd_gcd, gcd_mul_lcm := gcd_mul_lcm, lcm_zero_left := lcm_zero_left,
      lcm_zero_right := lcm_zero_right : GCDMonoid α } =
    g₂
Tactic: cases g₁
Cleared hypotheses: g₁, hgcd, hlcm