case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd (a * b) (d * b) = b
a b c : ℕ
hac : coprime a c
b_dvd_c : b ∣ c
⊢ gcd (a * b) c = b
rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d * b = b
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd (a * b) (d * b) = b
rw [gcd_mul_right]
case h.e'_2.h.e'_5
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d = 1
case intro
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d * b = b
convert one_mul b
no goals
case h.e'_2.h.e'_5
a b d : ℕ
hac : coprime a (d * b)
b_dvd_c : b ∣ d * b
⊢ gcd a d = 1
exact coprime.coprime_mul_right_right hac