awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
refine ⟨gcd_dvd_left _ _, ?_⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hab : ∀ (d : α) (hd : b - c = a * d), @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
rcases h with ⟨d, hd⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
hab :
  ∀ (e : α) (he : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e),
    @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
rcases gcd_dvd_right a b with ⟨e, he⟩

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e
hab :
  ∀ (f : α) (hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f),
    @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
rcases gcd_dvd_left a b with ⟨f, hf⟩

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e
f : α
hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f
h : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c

Tactic:
use e - f * d
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e
f : α
hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f
h : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (f * d)
h₁ : c = b - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (f * d)
h₂ : c = b - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f * d
h₃ : c = b - a * d
h₄ : c = b - (b - c)
h₅ h₆ : c = c
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)

Tactic:
rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]

Premises used: mul_sub, mul_assoc, sub_sub_cancel
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hba : ∀ (d : α) (hd : b - c = a * d), @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
rcases h with ⟨d, hd⟩
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
hba :
  ∀ (e : α) (he : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e),
    @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
rcases gcd_dvd_right a c with ⟨e, he⟩

Premises used: GCDMonoid.gcd_dvd_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e
hba :
  ∀ (f : α) (hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f),
    @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
rcases gcd_dvd_left a c with ⟨f, hf⟩

Premises used: GCDMonoid.gcd_dvd_left
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e
f : α
hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f
h : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b

Tactic:
use e + f * d
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e
f : α
hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f
h : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (f * d)
h₁ : b = c + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (f * d)
h₂ : b = c + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f * d
h₃ : b = c + a * d
h₄ : b = c + (b - c)
h₅ : b = c + b - c
h₆ : b = b + c - c
h₇ h₈ : b = b
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)

Tactic:
rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]

Premises used: add_sub_assoc, mul_assoc, add_comm, mul_add, add_sub_cancel_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b = @gcd _ CommSemiring.toCommMonoidWithZero _ c a
rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c
rw₂ rw₃ : @gcd _ CommSemiring.toCommMonoidWithZero _ a c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ b a = @gcd _ CommSemiring.toCommMonoidWithZero _ c a

Tactic:
rw [gcd_comm _ a, gcd_comm _ a, gcd_eq_of_dvd_sub_right h]

Premises used: gcd_comm, gcd_eq_of_dvd_sub_right
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a : α
⊢ a * (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) =
    (f : (a : Associates α) → α) (Associates.mk a)

Tactic:
Classical.choose_spec (associated_map_mk hinv a)

Premises used: Classical.choose_spec, Associates.associated_map_mk
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
simp_rw :
  (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b))) ⋯) :
      α) =
    (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α)
⊢ (if a * b = 0 then 1
    else
      Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
        ⋯) =
    (if a = 0 then 1
      else Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) *
      if b = 0 then 1
      else Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯

Tactic:
simp_rw [if_neg (mul_ne_zero ha hb), if_neg ha, if_neg hb, Units.ext_iff, Units.val_mul]

Premises used: Units.ext_iff, mul_ne_zero, if_neg, Units.val_mul
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this :
  a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) :
          α) *
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
apply :
  a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a * b *
      ((↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
⊢ (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b))) ⋯) :
      α) =
    (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α)

Tactic:
apply mul_left_cancel₀ (mul_ne_zero ha hb) _

Premises used: mul_left_cancel₀, mul_ne_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
this :
  a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) :
          α) *
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
⊢ a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a * b *
      ((↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))

Tactic:
simpa only [mul_assoc, mul_comm, mul_left_comm] using this

Premises used: mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
suffices :
  a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) :
          α) *
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
⊢ (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b))) ⋯) :
      α) =
    (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α)

Tactic:
suffices a * b * ↑(Classical.choose (associated_map_mk hinv (a * b))) =
        a * ↑(Classical.choose (associated_map_mk hinv a)) *
        (b * ↑(Classical.choose (associated_map_mk hinv b))) by
      apply mul_left_cancel₀ (mul_ne_zero ha hb) _
      simpa only [mul_assoc, mul_comm, mul_left_comm] using this
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
rw :
  a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    HMul.hMul (α := α) ((f : (a : Associates α) → α) (Associates.mk a) : α)
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
rw₁ :
  (f : (a : Associates α) → α) (Associates.mk (a * b)) =
    HMul.hMul (α := α) ((f : (a : Associates α) → α) (Associates.mk a) : α)
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))
rw₂ :
  (f : (a : Associates α) → α) (Associates.mk (a * b)) =
    HMul.hMul (α := α) (β := α) ((f : (a : Associates α) → α) (Associates.mk a) : α)
      ((f : (a : Associates α) → α) (Associates.mk b) : α)
rw₃ :
  Eq (α := α) ((f : (a : Associates α) → α) (Associates.mk (a * b)) : α)
    ((f : (a : Associates α) → α) (HMul.hMul (α := Associates α) (Associates.mk a) (Associates.mk b)) : α)
rw₄ rw₅ :
  Eq (α := α) ((f : (a : Associates α) → α) (Associates.mk (a * b)) : α)
    ((f : (a : Associates α) → α) (Associates.mk (a * b)) : α)
⊢ a * b *
      (↑(Classical.choose (p := fun (x : αˣ) ↦ a * b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (a * b)))
            ⋯) :
        α) =
    a *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ a * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk a)) ⋯) :
          α) *
      (b *
        (↑(Classical.choose (p := fun (x : αˣ) ↦ b * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk b)) ⋯) : α))

Tactic:
rw [map_mk_unit_aux hinv a, map_mk_unit_aux hinv (a * b), map_mk_unit_aux hinv b, ←
      map_mul, Associates.mk_mul_mk]

Premises used: HMul.hMul, _private.0.map_mk_unit_aux, map_mul, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
u : αˣ
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
u : αˣ
h : Nontrivial α
simp_rw :
  (↑(Classical.choose (p := fun (x : αˣ) ↦ (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α)))
          ⋯) :
      α) =
    (↑u⁻¹ : α)
⊢ (if (↑u : α) = 0 then 1
    else
      Classical.choose (p := fun (x : αˣ) ↦ (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α)))
        ⋯) =
    u⁻¹

Tactic:
simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]

Premises used: Units.ext_iff, Units.ne_zero, if_neg
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
u : αˣ
h : Nontrivial α
apply :
  (↑u : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦
            (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α))) ⋯) :
        α) =
    (↑u : α) * (↑u⁻¹ : α)
⊢ (↑(Classical.choose (p := fun (x : αˣ) ↦ (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α)))
          ⋯) :
      α) =
    (↑u⁻¹ : α)

Tactic:
apply mul_left_cancel₀ (Units.ne_zero u)

Premises used: Units.ne_zero, mul_left_cancel₀
-- Module: Mathlib.Algebra.GCDMonoid.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
inst_2 : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (α := α) (β := Associates α) (⇑f : (a : Associates α) → α) Associates.mk
u : αˣ
h : Nontrivial α
rw :
  (↑u : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦
            (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α))) ⋯) :
        α) =
    1
rw₁ : Eq (α := α) ((f : (a : Associates α) → α) (Associates.mk (↑u : α)) : α) (1 : α)
rw₂ : Eq (α := α) ((f : (a : Associates α) → α) (Associates.mk 1) : α) (1 : α)
rw₃ : Eq (α := α) ((f : (a : Associates α) → α) 1 : α) (1 : α)
rw₄ rw₅ : Eq.{u_1 + 1} (α := α) 1 1
⊢ (↑u : α) *
      (↑(Classical.choose (p := fun (x : αˣ) ↦
            (↑u : α) * (↑x : α) = (f : (a : Associates α) → α) (Associates.mk (↑u : α))) ⋯) :
        α) =
    (↑u : α) * (↑u⁻¹ : α)

Tactic:
rw [Units.mul_inv, map_mk_unit_aux hinv u,
      Associates.mk_eq_mk_iff_associated.2 (associated_one_iff_isUnit.2 ⟨u, rfl⟩),
      Associates.mk_one, map_one]

Premises used: Iff.mpr, Units.val, Associates.mk_eq_mk_iff_associated, associated_one_iff_isUnit, _private.0.map_mk_unit_aux, Associates.mk_one, Units.mul_inv, map_one, Exists.intro, rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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 : α
pos : ∀ (a0 : a = 0), Associated (gcd a b * 0) (a * b)
neg : ∀ (a0 : ¬a = 0), Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ a * b = gcd a b * x) ⋯) (a * b)
⊢ Associated (gcd a b * if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ 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 : 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)
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 : 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
neg neg₁ : Associated (a * b) (a * b)
⊢ Associated (gcd a b * Classical.choose (p := fun (x : α) ↦ a * b = gcd a b * x) ⋯) (a * b)

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

Premises used: Dvd.intro, Classical.choose_spec, rfl, Dvd.dvd.trans
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
neg : ∀ (a0 : ¬a = 0), Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
⊢ (if a = 0 then 0 else Classical.choose (p := fun (x : α) ↦ 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 : 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
⊢ Eq.{u_1 + 1} (α := α) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = a * 0

Tactic:
have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
contrapose : ∀ (a0 : gcd a 0 = 0), a = 0
⊢ gcd a 0 ≠ 0

Tactic:
contrapose a0
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
rw : Associated a (gcd a 0)
⊢ a = 0

Tactic:
rw [← associated_zero_iff_eq_zero, ← a0]

Premises used: associated_zero_iff_eq_zero
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
⊢ Associated a (gcd a 0)

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

Premises used: dvd_zero, associated_of_dvd_dvd, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
⊢ Associated a (gcd a 0)

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

Premises used: dvd_zero, associated_of_dvd_dvd, dvd_refl
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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

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 _ _)
-- Module: Mathlib.Algebra.GCDMonoid.Basic
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
apply : gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0
⊢ Classical.choose (p := fun (x : α) ↦ 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 : 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
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) 0 0
⊢ gcd a 0 * Classical.choose (p := fun (x : α) ↦ a * 0 = gcd a 0 * x) ⋯ = 0

Tactic:
rw [h, mul_zero]

Premises used: MulZeroClass.mul_zero