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 α
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
a b : α
a0 : a = 0
pos : Associated 0 (a * b)
pos₁ : Associated 0 (0 * b)
⊢ Associated (gcd a b * 0) (a * b)
have pos₂ : Associated.{u_1} (M := α) 0 0
Tactic: rw [mul_zero, a0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ a * b = gcd a b * x) ⋯) (a * b)
have neg : Associated (a * b) (a * b)
Tactic: rw [← Classical.choose_spec ((gcd_dvd_left a b).trans (Dvd.intro b rfl))]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯) = 0
have pos : ∀ (a0 : a = 0), Eq.{u_1 + 1} (α := α) 0 0
Tactic: split_ifs with a0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
pos : ∀ (a0 : a = 0), Eq.{u_1 + 1} (α := α) 0 0
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯) = 0
have neg : ∀ (a0 : ¬a = 0), Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) sorry = 0
Tactic: split_ifs with a0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
⊢ Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
have h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) sorry = a * 0
Tactic: have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
⊢ gcd a 0 ≠ 0
have contrapose : ∀ (a0 : gcd a 0 = 0), a = 0
Tactic: contrapose a0
Cleared hypotheses: a0
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
a0 : gcd a 0 = 0
⊢ a = 0
have rw : Associated a (gcd a 0)
Tactic: rw [← associated_zero_iff_eq_zero, ← a0]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
⊢ Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
have a0' : gcd a 0 ≠ 0
Tactic: have a0' : gcd a 0 ≠ 0 := by
        contrapose a0
        rw [← associated_zero_iff_eq_zero, ← a0]
        exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
a0' : gcd a 0 ≠ 0
⊢ Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
have apply : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) sorry = 0
Tactic: apply Or.resolve_left (mul_eq_zero.1 _) a0'
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
a0' : gcd a 0 ≠ 0
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
have rw : a * 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 : IsCancelMulZero α
inst_2 : 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
a : α
a0 : ¬a = 0
h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0
a0' : gcd a 0 ≠ 0
rw : a * 0 = 0
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
have rw₁ : Eq.{u_1 + 1} (α := α) 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 : 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 : α
⊢ Associated
    (gcd a b *
      if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯)
    (a * b)
have pos : ∀ (a0 : a = 0), Associated (gcd a b * 0) (a * b)
Tactic: split_ifs with a0
-- 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 α
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 : α
pos : ∀ (a0 : a = 0), Associated (gcd a b * 0) (a * b)
⊢ Associated
    (gcd a b *
      if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯)
    (a * b)
have neg : ∀ (a0 : ¬a = 0),
  Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) sorry) (a * b)
Tactic: split_ifs with a0
-- 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 α
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
⊢ Associated (gcd a b * 0) (a * b)
have pos : Associated 0 (a * b)
Tactic: rw [mul_zero, a0, zero_mul]
-- 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 α
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
pos : Associated 0 (a * b)
⊢ Associated (gcd a b * 0) (a * b)
have pos₁ : Associated 0 (0 * b)
Tactic: rw [mul_zero, a0, zero_mul]
-- 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 α
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
pos : Associated 0 (a * b)
pos₁ : Associated 0 (0 * b)
⊢ Associated (gcd a b * 0) (a * b)
have pos₂ : Associated.{u_1} (M := α) 0 0
Tactic: rw [mul_zero, a0, zero_mul]
-- 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 α
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
⊢ Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯) (a * b)
have neg : Associated ((normalize : (a : α) → α) (a * b)) (a * b)
Tactic: rw [← Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (.intro b rfl)))]
-- 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 α
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 : α
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯) = 0
have pos : ∀ (a0 : a = 0), Eq.{u_1 + 1} (α := α) 0 0
Tactic: split_ifs with a0
-- 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 α
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 : α
pos : ∀ (a0 : a = 0), Eq.{u_1 + 1} (α := α) 0 0
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯) = 0
have neg : ∀ (a0 : ¬a = 0), Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) sorry = 0
Tactic: split_ifs with a0
-- 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 α
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 : α
a0 : ¬a = 0
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have a0₁ : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
Tactic: rw [← normalize_eq_zero] at a0
Cleared hypotheses: a0
-- 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 α
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 : α
a0 : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have h : gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) sorry =
  (normalize : (a : α) → α) (a * 0)
Tactic: have h :=
        (Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a 0).trans (.intro 0 rfl)))).symm
-- 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 α
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 : α
a0 : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
⊢ gcd a 0 = (normalize : (a : α) → α) a
have rw : Eq (α := α) ((normalize : (a : α) → α) (gcd a 0) : α) ((normalize : (a : α) → α) a : α)
Tactic: rw [← normalize_gcd]
-- 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 α
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 : α
a0 : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have gcd0 : gcd a 0 = (normalize : (a : α) → α) a
Tactic: have gcd0 : gcd a 0 = normalize a := by
        rw [← normalize_gcd]
        exact normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a))
-- 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 α
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 : α
a0 : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
gcd0 : gcd a 0 = (normalize : (a : α) → α) a
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have a0₁ : ¬gcd a 0 = 0
Tactic: rw [← gcd0] at a0
Cleared hypotheses: a0, h, gcd0
-- 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 α
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 : α
a0 : ¬gcd a 0 = 0
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
gcd0 : gcd a 0 = (normalize : (a : α) → α) a
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have apply : gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) sorry = 0
Tactic: apply Or.resolve_left (mul_eq_zero.1 _) a0
-- 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 α
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 : α
a0 : ¬gcd a 0 = 0
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
gcd0 : gcd a 0 = (normalize : (a : α) → α) a
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have rw : Eq (α := α) ((normalize : (a : α) → α) (a * 0) : α) (0 : α)
Tactic: rw [h, mul_zero, normalize_zero]
-- 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 α
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 : α
a0 : ¬gcd a 0 = 0
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
gcd0 : gcd a 0 = (normalize : (a : α) → α) a
rw : Eq (α := α) ((normalize : (a : α) → α) (a * 0) : α) (0 : α)
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have rw₁ : Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 0 : α) (0 : α)
Tactic: rw [h, mul_zero, normalize_zero]
-- 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 α
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 : α
a0 : ¬gcd a 0 = 0
h :
  gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)
gcd0 : gcd a 0 = (normalize : (a : α) → α) a
rw : Eq (α := α) ((normalize : (a : α) → α) (a * 0) : α) (0 : α)
rw₁ : Eq.{u_1 + 1} (α := α) ((normalize : (a : α) → α) 0 : α) (0 : α)
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
have rw₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [h, mul_zero, normalize_zero]
-- 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 α
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 : α
⊢ (normalize : (a : α) → α)
      (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯) =
    if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯
have dsimp : (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry) *
    (↑(normUnit
          (if a = 0 then 0
          else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry)) :
      α) =
  if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry
Tactic: dsimp [normalize]
-- 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 α
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 : α
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯) *
      (↑(normUnit
            (if a = 0 then 0
            else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯)) :
        α) =
    if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯
have pos : ∀ (a0 : a = 0), HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0
Tactic: split_ifs with a0
-- 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 α
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 : α
pos : ∀ (a0 : a = 0), HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯) *
      (↑(normUnit
            (if a = 0 then 0
            else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯)) :
        α) =
    if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯
have neg : ∀ (a0 : ¬a = 0),
  Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry *
      (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry)) : α) =
    Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) sorry
Tactic: split_ifs with a0
-- 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 α
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
⊢ Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯ *
      (↑(normUnit (Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯)) : α) =
    Classical.choose (p := fun (x : α) ↦ a * b * (↑(normUnit (a * b)) : α) = gcd a b * x) ⋯
have this : gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) sorry =
  (normalize : (a : α) → α) (a * b)
Tactic: have := (Classical.choose_spec
          (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))).symm