instForall — Mathlib

English

If each G i has UniqueProds, then the function type ∀ i, G i has UniqueProds.

Русский

Если каждый G i имеет UniqueProds, то ∀ i, G i имеет UniqueProds.

LaTeX

$$$ \\forall \\iota\\, (G: \\iota \\to Type^*)\\ [\\forall i, Mul (G i)] [\\forall i, \\mathrm{UniqueProds} (G i)] : \\mathrm{UniqueProds}(\\forall i, G i). $$$

Lean4

@[to_additive]
instance instForall {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, UniqueProds (G i)] : UniqueProds (∀ i, G i) where
  uniqueMul_of_nonempty
    {A} := by
    classical
    let _ :=
      isWellFounded_ssubset (α := ∀ i, G i) -- why need this?

    apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
    apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
    by_cases hc : #A ≤ 1 ∧ #B ≤ 1
    · exact of_card_le_one hA hB hc.1 hc.2
    simp_rw [not_and_or, not_le] at hc
    obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
    obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))
    rw [mem_image, ← filter_nonempty_iff] at hA hB
    let A' := {a ∈ A | a i = ai}; let B' := {b ∈ B | b i = bi}
    obtain ⟨a0, ha0, b0, hb0, hu⟩ : ∃ a0 ∈ A', ∃ b0 ∈ B', UniqueMul A' B' a0 b0 :=
      by
      rcases hc with hc | hc; · exact ihA A' (hc.2 ai) hA hB
      by_cases hA' : A' = A
      · rw [hA']
        exact ihB B' (hc.2 bi) hB
      · exact ihA A' ((A.filter_subset _).ssubset_of_ne hA') hA hB
    rw [mem_filter] at ha0 hb0
    exact ⟨a0, ha0.1, b0, hb0.1, of_image_filter (Pi.evalMulHom G i) ha0.2 hb0.2 hi hu⟩

Похожие утверждения