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 : Subsingleton.{u_1 + 1} αˣ
g₂ : GCDMonoid α
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₂
have mk : ∀ [toIsCancelMulZero_1 : IsCancelMulZero α] (gcd_1 lcm_1 : α → α → α) (gcd_dvd_left_1 : ∀ (a b : α), gcd_1 a b ∣ a)
  (gcd_dvd_right_1 : ∀ (a b : α), gcd_1 a b ∣ b) (dvd_gcd_1 : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd_1 c b)
  (gcd_mul_lcm_1 : ∀ (a b : α), Associated (gcd_1 a b * lcm_1 a b) (a * b)) (lcm_zero_left_1 : ∀ (a : α), lcm_1 0 a = 0)
  (lcm_zero_right_1 : ∀ (a : α), lcm_1 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 α } =
    { toIsCancelMulZero := toIsCancelMulZero_1, gcd := gcd_1, lcm := lcm_1, gcd_dvd_left := gcd_dvd_left_1,
      gcd_dvd_right := gcd_dvd_right_1, dvd_gcd := @dvd_gcd_1, gcd_mul_lcm := gcd_mul_lcm_1,
      lcm_zero_left := lcm_zero_left_1, lcm_zero_right := lcm_zero_right_1 }
Tactic: cases g₂
Cleared hypotheses: g₂, hgcd, hlcm
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a b : NormalizedGCDMonoid α
⊢ a = b
have mk : ∀ [toNormalizationMonoid : NormalizationMonoid α] [toGCDMonoid : GCDMonoid α]
  (normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
  (normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
  { toNormalizationMonoid := toNormalizationMonoid, toGCDMonoid := toGCDMonoid, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
b : NormalizedGCDMonoid α
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    b
have mk : ∀ [toNormalizationMonoid : NormalizationMonoid α] [toGCDMonoid : GCDMonoid α]
  (normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
  (normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
  { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := toNormalizationMonoid, toGCDMonoid := toGCDMonoid, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := b_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }
have this : a_gcd = b_gcd
Tactic: have := Subsingleton.elim a_gcd b_gcd
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
this : a_gcd = b_gcd
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := b_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }
have mk : ∀ (normalize_gcd_2 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
  (normalize_lcm_2 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
  { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_2,
      normalize_lcm := normalize_lcm_2 }
Tactic: subst this
Cleared hypotheses: b_gcd, normalize_gcd_1, normalize_lcm_1, this
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }
have this : a_norm = b_norm
Tactic: have := Subsingleton.elim a_norm b_norm
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : Subsingleton.{u_1 + 1} αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
b_norm : NormalizationMonoid α
normalize_gcd_1 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b
normalize_lcm_1 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b
this : a_norm = b_norm
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_1,
      normalize_lcm := normalize_lcm_1 }
have mk : ∀ (normalize_gcd_2 : ∀ (a b : α), (normalize : (a : α) → α) (@gcd _ inst _ a b) = @gcd _ inst _ a b)
  (normalize_lcm_2 : ∀ (a b : α), (normalize : (a : α) → α) (@lcm _ inst _ a b) = @lcm _ inst _ a b),
  { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd,
      normalize_lcm := normalize_lcm : NormalizedGCDMonoid α } =
    { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd_2,
      normalize_lcm := normalize_lcm_2 }
Tactic: subst this
Cleared hypotheses: b_norm, normalize_gcd_1, normalize_lcm_1, this
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c
have hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a c
Tactic: apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c
have hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b
Tactic: apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a c
have hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
Tactic: rw [dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b
have hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
Tactic: rw [dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
have hab : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
Tactic: refine ⟨gcd_dvd_left _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ a ∧ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
have hba : @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
Tactic: refine ⟨gcd_dvd_left _ _, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
have hab : ∀ (d : α) (hd : b - c = a * d), @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
Tactic: rcases h with ⟨d, hd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
have hab : ∀ (e : α) (he : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e),
  @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
Tactic: rcases gcd_dvd_right a b with ⟨e, he⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
have hab : ∀ (f : α) (hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f),
  @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
Tactic: rcases gcd_dvd_left a b with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ c
have h : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
Tactic: use e - f * d
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * e - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (f * d)
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h₁ : c = b - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (f * d)
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h₂ : c = b - @gcd _ CommSemiring.toCommMonoidWithZero _ a b * f * d
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h₃ : c = b - a * d
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h₄ : c = b - (b - c)
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ c = @gcd _ CommSemiring.toCommMonoidWithZero _ a b * (e - f * d)
have h₅ : c = c
Tactic: rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
have hba : ∀ (d : α) (hd : b - c = a * d), @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
Tactic: rcases h with ⟨d, hd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
Goal:
α : Type u_1
inst : CommRing α
inst_1 : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
have hba : ∀ (e : α) (he : c = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e),
  @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
Tactic: rcases gcd_dvd_right a c with ⟨e, he⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
have hba : ∀ (f : α) (hf : a = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f),
  @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
Tactic: rcases gcd_dvd_left a c with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a c ∣ b
have h : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
Tactic: use e + f * d
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h : b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * e + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (f * d)
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₁ : b = c + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (f * d)
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₂ : b = c + @gcd _ CommSemiring.toCommMonoidWithZero _ a c * f * d
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₃ : b = c + a * d
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₄ : b = c + (b - c)
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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)
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₅ : b = c + b - c
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.GCDMonoid.Basic (goal)
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
⊢ b = @gcd _ CommSemiring.toCommMonoidWithZero _ a c * (e + f * d)
have h₆ : b = b + c - c
Tactic: rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel_right]