English
If every G i has TwoUniqueProds, then the function type (i → G i) has TwoUniqueProds.
Русский
Если каждый G i имеет TwoUniqueProds, то функция (i → G i) имеет TwoUniqueProds.
LaTeX
$$$ \\forall ι\\, (G: ι \\to Type^*)\\ [\\forall i, Mul (G i)] [\\forall i, TwoUniqueProds (G i)] : \\mathrm{TwoUniqueProds}(\\lambda i, G i). $$$
Lean4
@[to_additive]
instance instForall {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, TwoUniqueProds (G i)] : TwoUniqueProds (∀ i, G i) where
uniqueMul_of_one_lt_card
{A} := by
classical
let _ :=
isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B
apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hc
obtain ⟨hA, hB, hc⟩ := Nat.one_lt_mul_iff.mp hc
rw [card_pos] at hA hB
obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
obtain ⟨p1, h1, p2, h2, hne, hi1, hi2⟩ :=
uniqueMul_of_one_lt_card
(Nat.one_lt_mul_iff.mpr ⟨card_pos.2 (hA.image _), card_pos.2 (hB.image _), hc.imp And.left And.left⟩)
simp_rw [mem_product, mem_image, ← filter_nonempty_iff] at h1 h2
replace h1 := uniqueMul_of_twoUniqueMul ?_ h1.1 h1.2
on_goal 1 => replace h2 := uniqueMul_of_twoUniqueMul ?_ h2.1 h2.2
· obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1
obtain ⟨a2, ha2, b2, hb2, hu2⟩ := h2
rw [mem_filter] at ha1 hb1 ha2 hb2
simp_rw [mem_product]
refine
⟨(a1, b1), ⟨ha1.1, hb1.1⟩, (a2, b2), ⟨ha2.1, hb2.1⟩, ?_,
UniqueMul.of_image_filter (Pi.evalMulHom G i) ha1.2 hb1.2 hi1 hu1,
UniqueMul.of_image_filter (Pi.evalMulHom G i) ha2.2 hb2.2 hi2 hu2⟩
grind
all_goals rcases hc with hc | hc; · exact ihA _ (hc.2 _)
· by_cases hA : {a ∈ A | a i = p2.1} = A
· rw [hA]
exact ihB _ (hc.2 _)
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
· by_cases hA : {a ∈ A | a i = p1.1} = A
· rw [hA]
exact ihB _ (hc.2 _)
· exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)
