theorem MathlibNt.SieveTheory.sum_card_le_of_relation {α : Type u_1} {β : Type u_2} (S : Finset α) (T : Finset β) (F : α → Finset β) (r : α → β → Prop) [DecidableRel r] (C : ℕ) (hmap : ∀ a ∈ S, ∀ b ∈ F a, b ∈ T ∧ r a b) (hcap : ∀ b ∈ T, {a ∈ S | r a b}.card ≤ C) : ∑ a ∈ S, (F a).card ≤ C * T.card

Bound labelled incidences by a relation whose reverse fibres have bounded size. The labels remain in S, even when their associated values coincide.

theorem MathlibNt.SieveTheory.sigma_snd_injOn_sub_mul_fiber (A : Finset ((_ : ℕ) × ℕ)) (N p : ℕ) (hpos : ∀ x ∈ A, 0 < x.snd) (hle : ∀ x ∈ A, x.snd * x.fst ≤ N) : Set.InjOn (fun (x : (_ : ℕ) × ℕ) => x.snd) ↑({x ∈ A | N - x.snd * x.fst = p})

On a fixed output fibre, a positive retained factor determines its cofactor. The product bounds are essential because subtraction is in the naturals.