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 : α
pos : ∀ (a0 : a = 0), Associated (gcd a b * 0) (a * b)
neg :
  ∀ (a0 : ¬a = 0),
    Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯)
      (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)

Tactic:
split_ifs with a0
-- 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
pos : Associated 0 (a * b)
pos₁ : Associated 0 (0 * b)
pos₂ pos₃ : Associated.{u_1} (M := α) 0 0
⊢ Associated (gcd a b * 0) (a * b)

Tactic:
rw [mul_zero, a0, zero_mul]

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

Tactic:
rw [← Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (.intro b rfl)))]

Premises used: Iff.mpr, Classical.choose_spec, Exists.intro, dvd_normalize_iff, rfl, Dvd.dvd.trans
-- 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
⊢ Associated ((normalize : (a : α) → α) (a * b)) (a * b)

Tactic:
normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
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 ((normalize : (a : α) → α) (a * b)) (a * b)

Tactic:
exact normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
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
neg : ∀ (a0 : ¬a = 0), Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯) = 0

Tactic:
split_ifs with a0
-- 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 : α
a0 : a = 0
⊢ Eq.{u_1 + 1} (α := α) 0 0

Tactic:
rfl
-- 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 : α
a0 : ¬a = 0
⊢ ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)

Tactic:
rw [← normalize_eq_zero] at a0

Premises used: 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 : α
a0 : ¬Eq (α := α) ((normalize : (a : α) → α) a : α) (0 : α)
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)

Tactic:
have h :=
        (Classical.choose_spec (dvd_normalize_iff.2 ((gcd_dvd_left a 0).trans (.intro 0 rfl)))).symm
-- 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 : α
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)
rw : Eq (α := α) ((normalize : (a : α) → α) (gcd a 0) : α) ((normalize : (a : α) → α) a : α)
⊢ gcd a 0 = (normalize : (a : α) → α) a

Tactic:
rw [← normalize_gcd]
-- 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 : α
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)
⊢ Eq (α := α) ((normalize : (a : α) → α) (gcd a 0) : α) ((normalize : (a : α) → α) a : α)

Tactic:
normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a))

Premises used: dvd_zero, normalize_eq_normalize, dvd_refl
-- 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 : α
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)
⊢ Eq (α := α) ((normalize : (a : α) → α) (gcd a 0) : α) ((normalize : (a : α) → α) a : α)

Tactic:
exact normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a))

Premises used: dvd_zero, normalize_eq_normalize, dvd_refl
-- 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 : α
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

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))
-- 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 : α
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
⊢ ¬gcd a 0 = 0

Tactic:
rw [← gcd0] at a0
-- 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 : α
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
a0₁ : ¬gcd a 0 = 0
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ =
    (normalize : (a : α) → α) (a * 0)

Tactic:
rw [← gcd0] at a0
-- 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 : α
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
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)
⊢ gcd a 0 = (normalize : (a : α) → α) a

Tactic:
rw [← gcd0] at a0
-- 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 : α
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
apply : gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0
⊢ Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0

Tactic:
apply Or.resolve_left (mul_eq_zero.1 _) a0

Premises used: Or.resolve_left, mul_eq_zero, Iff.mp
-- 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 : α
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 : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯ = 0

Tactic:
rw [h, mul_zero, normalize_zero]

Premises used: MulZeroClass.mul_zero, normalize_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 : α
dsimp :
  (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) ⋯
⊢ (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) ⋯

Tactic:
dsimp [normalize]

Premises used: normalize
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : NormalizationMonoid α
inst_3 : DecidableEq α
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
neg :
  ∀ (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) ⋯
⊢ (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) ⋯

Tactic:
split_ifs with a0
-- 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
⊢ HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0

Tactic:
@normalize_zero α _ _

Premises used: normalize_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
⊢ HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0

Tactic:
exact @normalize_zero α _ _

Premises used: normalize_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
⊢ gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯ =
    (normalize : (a : α) → α) (a * b)

Tactic:
have := (Classical.choose_spec
          (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))).symm
-- 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
this :
  gcd a b * Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯ =
    (normalize : (a : α) → α) (a * b)
neg :
  let l := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * b) = gcd a b * x) ⋯;
  ∀ (this : gcd a b * l = (normalize : (a : α) → α) (a * b)), l * (↑(normUnit l) : α) = l
⊢ 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) ⋯

Tactic:
set l := Classical.choose (dvd_normalize_iff.2 ((gcd_dvd_left a b).trans (Dvd.intro b rfl)))

Premises used: Iff.mpr, Dvd.intro, dvd_normalize_iff, Classical.choose, rfl, Dvd.dvd.trans
-- 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)
neg :
  let l := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯;
  ∀ (this : gcd a 0 * l = (normalize : (a : α) → α) (a * 0)), l * (↑(normUnit l) : α) = l
neg₁ : ∀ (hb : b ≠ 0), l * (↑(normUnit l) : α) = l
⊢ l * (↑(normUnit l) : α) = l

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
this : gcd a 0 * l = (normalize : (a : α) → α) (a * 0)
⊢ gcd a 0 = 0 ∨ l = 0

Tactic:
rw [mul_zero a, normalize_zero, mul_eq_zero] at this

Premises used: mul_eq_zero, MulZeroClass.mul_zero, normalize_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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
this : gcd a 0 = 0 ∨ l = 0
neg : ∀ (ha : gcd a 0 = 0), l * (↑(normUnit l) : α) = l
neg₁ : ∀ (hl : l = 0), l * (↑(normUnit l) : α) = l
⊢ l * (↑(normUnit l) : α) = l

Tactic:
obtain ha | hl := 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
ha : gcd a 0 = 0
apply : a = 0
⊢ l * (↑(normUnit l) : α) = l

Tactic:
apply (a0 _).elim

Premises used: False.elim
-- 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
ha : gcd a 0 = 0
rw : gcd a 0 ∣ a
⊢ a = 0

Tactic:
rw [← zero_dvd_iff, ← ha]

Premises used: zero_dvd_iff
-- 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
ha : gcd a 0 = 0
⊢ gcd a 0 ∣ a

Tactic:
gcd_dvd_left _ _
-- 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
ha : gcd a 0 = 0
⊢ gcd a 0 ∣ a

Tactic:
exact gcd_dvd_left _ _
-- 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 : α
a0 : ¬a = 0
l : α := Classical.choose (p := fun (x : α) ↦ (normalize : (a : α) → α) (a * 0) = gcd a 0 * x) ⋯
hl : l = 0
neg : HMul.hMul (α := α) 0 (↑(normUnit 0) : α) = 0
neg₁ neg₂ : Eq.{u_1 + 1} (α := α) 0 0
⊢ l * (↑(normUnit l) : α) = l

Tactic:
rw [hl, zero_mul]

Premises used: MulZeroClass.zero_mul