α : Type u
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ (#{ t // (#↑t) ≤ c })

α : Type u
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ max (#α) ℵ₀ ^ c
α : Type u
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ max (#α) ℵ₀ ^ c
trans #{ t : Set (Sum (ULift.{u} ℕ) α) // (#t) ≤ c }
α : Type u
c : Cardinal
⊢ (#ULift ℕ ⊕ α) ^ c ≤ max (#α) ℵ₀ ^ c
α : Type u
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ max (#α) ℵ₀ ^ c
apply (mk_bounded_set_le_of_infinite (Sum (ULift.{u} ℕ) α) c).trans
no goals
α : Type u
c : Cardinal
⊢ (#ULift ℕ ⊕ α) ^ c ≤ max (#α) ℵ₀ ^ c
rw [max_comm, ← add_eq_max] <;> rfl
case refine'_1
α : Type u
c : Cardinal
⊢ Set α ↪ Set (ULift ℕ ⊕ α)

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑?refine'_1 x)) ≤ c
α : Type u
c : Cardinal
⊢ (#{ t // (#↑t) ≤ c }) ≤ (#{ t // (#↑t) ≤ c })
refine' ⟨Embedding.subtypeMap _ _⟩
case refine'_1.f
α : Type u
c : Cardinal
⊢ α ↪ ULift ℕ ⊕ α

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑(Embedding.image ?refine'_1.f) x)) ≤ c
case refine'_1
α : Type u
c : Cardinal
⊢ Set α ↪ Set (ULift ℕ ⊕ α)

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑?refine'_1 x)) ≤ c
apply Embedding.image
case refine'_1.f
α : Type u
c : Cardinal
⊢ Injective Sum.inr

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑(Embedding.image { toFun := Sum.inr, inj' := ?refine'_1.f }) x)) ≤ c
case refine'_1.f
α : Type u
c : Cardinal
⊢ α ↪ ULift ℕ ⊕ α

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑(Embedding.image ?refine'_1.f) x)) ≤ c
use Sum.inr
case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄,
    (#↑x) ≤ c →
      (#↑(↑(Embedding.image
                  { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
              x)) ≤
        c
case refine'_1.f
α : Type u
c : Cardinal
⊢ Injective Sum.inr

case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄, (#↑x) ≤ c → (#↑(↑(Embedding.image { toFun := Sum.inr, inj' := ?refine'_1.f }) x)) ≤ c
apply Sum.inr.inj
case refine'_2
α : Type u
c : Cardinal
s : Set α
hs : (#↑s) ≤ c
⊢ (#↑(↑(Embedding.image
              { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
          s)) ≤
    c
case refine'_2
α : Type u
c : Cardinal
⊢ ∀ ⦃x : Set α⦄,
    (#↑x) ≤ c →
      (#↑(↑(Embedding.image
                  { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
              x)) ≤
        c
intro s hs
no goals
case refine'_2
α : Type u
c : Cardinal
s : Set α
hs : (#↑s) ≤ c
⊢ (#↑(↑(Embedding.image
              { toFun := Sum.inr, inj' := (_ : ∀ {val val_1 : α}, Sum.inr val = Sum.inr val_1 → val = val_1) })
          s)) ≤
    c
exact mk_image_le.trans hs