English
If a | b·c and gcd(a,b) = 1, then a | c.
Русский
Если a делит b·c и gcd(a,b) = 1, тогда a делит c.
LaTeX
$$$$a \\mid bc \\wedge \\gcd(a,b) = 1 \\Rightarrow a \\mid c.$$$$
Lean4
/-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
Compare with `IsCoprime.dvd_of_dvd_mul_left` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors` -/
theorem dvd_of_dvd_mul_left_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a c = 1) : a ∣ b :=
by
have := gcd_eq_gcd_ab a c
simp only [hab, Int.ofNat_zero, Int.natCast_succ, zero_add] at this
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← Int.mul_add, ← this]
rw [← this]
exact Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b) _) (dvd_mul_of_dvd_left habc _)
