Formalizing simple theorem involving division

Stream: new members

[Alex Gu]

I'm trying to formalize the simple theorem and its proof: Prove that if $a, b, c, d$ are natural numbers such that $a/b+c/d=1$, then $ad+bc$ is divisible by $bd$.

The proof (mathematically) is very simple, expand out the fraction, and then $ad+bc=bd$. However, I'm struggling to represent this in Lean. Is this a good formalization to work with? If not, any tips?

import Mathlib

theorem composite_natural_number_iff_exists_a_b_x_y (a b c d : ℤ)

(ha : a ≥ 1) (hb : b ≥ 1) (hc : c ≥ 1) (hd : d ≥ 1) :

(a : ℚ) / (b : ℚ) + (c : ℚ) / (d : ℚ) = 1 → (b*d) ∣ (a*d+b*c) := by sorry

[Kevin Buzzard]

Yeah that looks fine. What does intro h then field_simp at h do? PS the question is weird, surely you should be proving that the two numbers are equal, not that one divides the other?

[Kevin Buzzard]

Then norm_cast at h then use 1 then polyrith?

[Alex Gu]

Thanks, awesome! I didn't know about norm_cast (and yes, agree the question is weird, but just doing some personal exercises :D)