One more cardinality question

Stream: new members

[Josha Dekker]

Hi, I'm trying to prove the following result, which is what I need to fill in the last sorry in my PR #12542, where I derive some more properties for cocardinal filters. The first version is needed for a result analogous to that for cofinite, the second is a stronger version that I think should apply as well.

import Mathlib.SetTheory.Cardinal.Cofinality

open Set Cardinal

universe u

example {ι : Type u} {c : Cardinal.{u}} {hreg : Cardinal.IsRegular c} {α : ι → Type u}
[inst : Finite ι] {s : Set ((i : ι) → α i)} {h₁ : ∀ (i : ι), #↑((fun a ↦ a i) '' s) < c}
{h₂ : #↑s ≤ #((i : ι) → α i)} : #↑s < c := by sorry

example {ι : Type u} {c : Cardinal.{u}} {hreg : Cardinal.IsRegular c} {α : ι → Type u}
{s : Set ((i : ι) → α i)} {h₁ : ∀ (i : ι), #↑((fun a ↦ a i) '' s) < c} {h₂ : #↑s ≤ #((i : ι) → α i)}
{hι : #ι < c} : #↑s < c := by sorry