-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) :
    #{ t : Set α // t ⊆ s ∧ #t ≤ c } ≤ max #s ℵ₀ ^ c

Proof state:
case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

Tactic:
use fun t => (↑) ⁻¹' t.1

Result:
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
⊢ Injective fun t => Subtype.val ⁻¹' ↑t

Proof state:
case inj'
α : Type u
s : Set α
c : Cardinal.{u}
⊢ Injective fun t => Subtype.val ⁻¹' ↑t

Tactic:
rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h

Result:
case inj'.mk.intro.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t => Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t => Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ⟨t, ⋯⟩ = ⟨t', ⋯⟩

Proof state:
case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }),
    { toFun := fun t => Subtype.val ⁻¹' ↑t, inj' := ⋯ } a ∈ fun t => Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
rintro ⟨t, _, h2t⟩

Result:
case refine_2.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left✝ : t ⊆ s
h2t : #↑t ≤ c
⊢ { toFun := fun t => Subtype.val ⁻¹' ↑t, inj' := ⋯ } ⟨t, ⋯⟩ ∈ fun t => Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) ⋯ c

Proof state:
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t => Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t => Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ↑⟨t, ⋯⟩ = ↑⟨t', ⋯⟩

Tactic:
dsimp only at h ⊢

Result:
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
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'

Proof state:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }

Tactic:
refine ⟨Embedding.codRestrict _ ?_ ?_⟩

Result:
case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }), ?refine_1 a ∈ fun t => Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) ⋯ c

Proof state:
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
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'

Tactic:
refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption

Result:
no goals

Proof state:
case refine_2.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left✝ : t ⊆ s
h2t : #↑t ≤ c
⊢ { toFun := fun t => Subtype.val ⁻¹' ↑t, inj' := ⋯ } ⟨t, ⋯⟩ ∈ fun t => Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t

Result:
no goals

Proof state:
case inj'.mk.intro.mk.intro
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t => Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t => Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ⟨t, ⋯⟩ = ⟨t', ⋯⟩

Tactic:
apply Subtype.eq

Result:
case inj'.mk.intro.mk.intro.a
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : (fun t => Subtype.val ⁻¹' ↑t) ⟨t, ⋯⟩ = (fun t => Subtype.val ⁻¹' ↑t) ⟨t', ⋯⟩
⊢ ↑⟨t, ⋯⟩ = ↑⟨t', ⋯⟩

Proof state:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ (#↑s ⊔ ℵ₀) ^ c

Tactic:
refine le_trans ?_ (mk_bounded_set_le s c)

Result:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }