a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ a = gcd (a * b) m
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
rw [gcd_eq_left_iff_dvd] at am
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd a m = gcd (a * b) m
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ a = gcd (a * b) m
conv_lhs => rw [← am]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd (a * b) m = gcd a m
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd a m = gcd (a * b) m
rw [eq_comm]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ Coprime b m
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd (a * b) m = gcd a m
apply Coprime.gcd_mul_right_cancel a
no goals
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ Coprime b m
apply Coprime.coprime_dvd_left bn cop.symm