English
As in 22537, with additional structural details about the distribution of prime divisors across the coordinates of f ∈ finMulAntidiag n.
Русский
Как в 22537, добавлены дополнительные структурные детали о распределении простых делителей по координатам f в finMulAntidiag n.
LaTeX
$$$\text{(detailed prime-divisibility structure for } f\in\text{finMulAntidiag}(d,n)\text{)}$$$
Lean4
/-- `finAntidiagonal d n` is the type of `d`-tuples with sum `n`.
TODO: deduplicate with the less general `Finset.Nat.antidiagonalTuple`. -/
def finAntidiagonal (d : ℕ) (n : μ) : Finset (Fin d → μ) :=
aux d n
where/-- Auxiliary construction for `finAntidiagonal` that bundles a proof of lawfulness
(`mem_finAntidiagonal`), as this is needed to invoke `disjiUnion`. Using `Finset.disjiUnion` makes
this computationally much more efficient than using `Finset.biUnion`. -/
aux (d : ℕ) (n : μ) : { s : Finset (Fin d → μ) // ∀ f, f ∈ s ↔ ∑ i, f i = n } :=
match d with
| 0 => if h : n = 0 then ⟨{0}, by simp [h, Subsingleton.elim _ ![]]⟩ else ⟨∅, by simp [Ne.symm h]⟩
| d + 1 =>
{ val :=
(antidiagonal n).disjiUnion
(fun ab =>
(aux d ab.2).1.map
{ toFun := Fin.cons (ab.1)
inj' := Fin.cons_right_injective _ })
(fun i _hi j _hj hij =>
Finset.disjoint_left.2 fun t hti htj =>
hij <| by
simp_rw [Finset.mem_map, Embedding.coeFn_mk] at hti htj
obtain ⟨ai, hai, hij'⟩ := hti
obtain ⟨aj, haj, rfl⟩ := htj
rw [Fin.cons_inj] at hij'
ext
· exact hij'.1
· obtain ⟨-, rfl⟩ := hij'
rw [← (aux d i.2).prop ai |>.mp hai, ← (aux d j.2).prop ai |>.mp haj])
property := fun f =>
by
simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists, (aux d _).prop,
Fin.sum_univ_succ]
constructor
· rintro ⟨a, b, rfl, g, rfl, rfl⟩
simp only [Fin.cons_zero, Fin.cons_succ]
· intro hf
exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩ }
