case hab
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ c

case hba
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b = gcd a c
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
  rw [dvd_gcd_iff] <;>
  refine' ⟨gcd_dvd_left _ _, _⟩
case hab.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a b ∣ c
case hab
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ c
rcases h with ⟨d, hd⟩
case hab.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
⊢ gcd a b ∣ c
case hab.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a b ∣ c
rcases gcd_dvd_right a b with ⟨e, he⟩
case hab.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ gcd a b ∣ c
case hab.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
⊢ gcd a b ∣ c
rcases gcd_dvd_left a b with ⟨f, hf⟩
case hab.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = gcd a b * (e - f * d)
case hab.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ gcd a b ∣ c
use e - f * d
no goals
case hab.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = gcd a b * (e - f * d)
rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]
case hba.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a c ∣ b
case hba
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b
rcases h with ⟨d, hd⟩
case hba.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
⊢ gcd a c ∣ b
case hba.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
⊢ gcd a c ∣ b
rcases gcd_dvd_right a c with ⟨e, he⟩
case hba.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ gcd a c ∣ b
case hba.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
⊢ gcd a c ∣ b
rcases gcd_dvd_left a c with ⟨f, hf⟩
case hba.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = gcd a c * (e + f * d)
case hba.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ gcd a c ∣ b
use e + f * d
no goals
case hba.intro.intro.intro
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = gcd a c * (e + f * d)
rw [mul_add, ← he, ← mul_assoc, ← hf, ← hd, ← add_sub_assoc, add_comm c b, add_sub_cancel]