α : Type u
s : Set α
c : Cardinal
⊢ (#{ t // t ⊆ s ∧ (#↑t) ≤ c }) ≤ (#{ t // (#↑t) ≤ c })
α : Type u
s : Set α
c : Cardinal
⊢ (#{ t // t ⊆ s ∧ (#↑t) ≤ c }) ≤ max (#↑s) ℵ₀ ^ c
refine' le_trans _ (mk_bounded_set_le s c)
case refine'_1
α : Type u
s : Set α
c : Cardinal
⊢ { t // t ⊆ s ∧ (#↑t) ≤ c } ↪ Set ↑s

case refine'_2
α : Type u
s : Set α
c : Cardinal
⊢ ∀ (a : { t // t ⊆ s ∧ (#↑t) ≤ c }),
    ↑?refine'_1 a ∈ fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
α : Type u
s : Set α
c : Cardinal
⊢ (#{ t // t ⊆ s ∧ (#↑t) ≤ c }) ≤ (#{ t // (#↑t) ≤ c })
refine' ⟨Embedding.codRestrict _ _ _⟩
case refine'_1
α : Type u
s : Set α
c : Cardinal
⊢ Injective fun t => Subtype.val ⁻¹' ↑t

case refine'_2
α : Type u
s : Set α
c : Cardinal
⊢ ∀ (a : { t // t ⊆ s ∧ (#↑t) ≤ c }),
    ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t, inj' := ?refine'_1 } a ∈ fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
case refine'_1
α : Type u
s : Set α
c : Cardinal
⊢ { t // t ⊆ s ∧ (#↑t) ≤ c } ↪ Set ↑s

case refine'_2
α : Type u
s : Set α
c : Cardinal
⊢ ∀ (a : { t // t ⊆ s ∧ (#↑t) ≤ c }),
    ↑?refine'_1 a ∈ fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
use fun t => (↑) ⁻¹' t.1
case refine'_2.mk.intro
α : Type u
s : Set α
c : Cardinal
t : Set α
left✝ : t ⊆ s
h2t : (#↑t) ≤ c
⊢ ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : { t // t ⊆ s ∧ (#↑t) ≤ c }⦄,
                (fun t => Subtype.val ⁻¹' ↑t) a₁ = (fun t => Subtype.val ⁻¹' ↑t) a₂ → a₁ = a₂) }
      { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } ∈
    fun t =>
    Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b)) c
case refine'_2
α : Type u
s : Set α
c : Cardinal
⊢ ∀ (a : { t // t ⊆ s ∧ (#↑t) ≤ c }),
    ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t,
            inj' :=
              (_ :
                ∀ ⦃a₁ a₂ : { t // t ⊆ s ∧ (#↑t) ≤ c }⦄,
                  (fun t => Subtype.val ⁻¹' ↑t) a₁ = (fun t => Subtype.val ⁻¹' ↑t) a₂ → a₁ = a₂) }
        a ∈
      fun t =>
      Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b))
        c
rintro ⟨t, _, h2t⟩
no goals
case refine'_2.mk.intro
α : Type u
s : Set α
c : Cardinal
t : Set α
left✝ : t ⊆ s
h2t : (#↑t) ≤ c
⊢ ↑{ toFun := fun t => Subtype.val ⁻¹' ↑t,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : { t // t ⊆ s ∧ (#↑t) ≤ c }⦄,
                (fun t => Subtype.val ⁻¹' ↑t) a₁ = (fun t => Subtype.val ⁻¹' ↑t) a₂ → a₁ = a₂) }
      { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } ∈
    fun t =>
    Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) (_ : ∀ (a b : Type u), a ≈ b → Nonempty (↑t ↪ a) = Nonempty (↑t ↪ b)) c
exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t
case refine'_1.mk.intro.mk.intro
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
⊢ { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } = { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
case refine'_1
α : Type u
s : Set α
c : Cardinal
⊢ Injective fun t => Subtype.val ⁻¹' ↑t
rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h
case refine'_1.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
⊢ ↑{ val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } = ↑{ val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
case refine'_1.mk.intro.mk.intro
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
⊢ { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } = { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
apply Subtype.eq
case refine'_1.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t = t'
case refine'_1.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h :
  (fun t => Subtype.val ⁻¹' ↑t) { val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } =
    (fun t => Subtype.val ⁻¹' ↑t) { val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
⊢ ↑{ val := t, property := (_ : t ⊆ s ∧ (#↑t) ≤ c) } = ↑{ val := t', property := (_ : t' ⊆ s ∧ (#↑t') ≤ c) }
dsimp only at h⊢
no goals
case refine'_1.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal
t : Set α
ht1 : t ⊆ s
ht2 : (#↑t) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : (#↑t') ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t = t'
refine' (preimage_eq_preimage' _ _).1 h <;> rw [Subtype.range_coe] <;> assumption