English
Let C be a property of nonnegative rationals. If for every pair of natural numbers n, d with d ≠ 0 and gcd(n, d) = 1 the value C(n/d) holds, then C(q) holds for every q ≥ 0.
Русский
Пусть C — свойство неотрицательных рациональных чисел. Если для каждой пары натуральных чисел n, d с d ≠ 0 и gcd(n,d) = 1 выполняется C(n/d), то C(q) выполняется для любого q ≥ 0.
LaTeX
$$$\forall C:\mathbb{Q}_{\ge 0}\to \text{Prop},\; \forall q\in\mathbb{Q}_{\ge 0},\; \Big(\forall n,d\in\mathbb{N},\; d\neq 0 \land \gcd(n,d)=1 \Rightarrow C\left(\frac{n}{d}\right)\Big) \Rightarrow C(q).$$$
Lean4
/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with nonnegative rational
numbers of the form `n / d` with `d ≠ 0` and `n`, `d` coprime. -/
@[elab_as_elim]
def numDenCasesOn.{u} {C : ℚ≥0 → Sort u} (q) (H : ∀ n d, d ≠ 0 → n.Coprime d → C (divNat n d)) : C q := by
rw [← q.num_divNat_den]; exact H _ _ q.den_ne_zero q.coprime_num_den
