-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_eq_of_dvd_sub_right {a b c : α} (h : a ∣ b - c) : gcd a b = gcd a c

Proof state:
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

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

Result:
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

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

Tactic:
rcases h with ⟨d, hd⟩

Result:
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

Proof state:
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

Tactic:
use e + f * d

Result:
case h
α : 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)

Proof state:
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

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

Result:
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

Proof state:
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b = gcd a c

Tactic:
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
  rw [dvd_gcd_iff] <;>
  refine ⟨gcd_dvd_left _ _, ?_⟩

Result:
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

Proof state:
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

Tactic:
use e - f * d

Result:
case h
α : 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)

Proof state:
case h
α : 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)

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

Result:
no goals

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

Tactic:
rcases h with ⟨d, hd⟩

Result:
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

Proof state:
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

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

Result:
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

Proof state:
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

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

Result:
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

Proof state:
case h
α : 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)

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

Result:
no goals