-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) {r : α → α → Prop}
    [IsWellOrder α r] (hr : (#α).ord = type r) : #{ s : Set α // Bounded r s } = #α

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ 2 ^ #↑{j | r j i} ≤ #α

Tactic:
apply (h'.two_power_lt _).le

Result:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ #↑{j | r j i} < #α

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ #↑{j | r j i} < #α

Tactic:
rw [coe_setOf, card_typein, ← lt_ord, hr]

Result:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ (typein r).toRelEmbedding i < type r

Proof state:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = 0

Tactic:
haveI := mk_eq_zero_iff.1 ha

Result:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ #{ s // Bounded r s } = 0

Proof state:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ #{ s // Bounded r s } ≤ #α

Tactic:
rw [← coe_setOf, this]

Result:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ #↑(⋃ i, 𝒫{j | r j i}) ≤ #α

Proof state:
case inr.a.refine_1.hr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ (#α).ord.IsLimit

Tactic:
apply isLimit_ord ha

Result:
no goals

Proof state:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s // Bounded r s }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Result:
case inr.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ Bounded r {x}

case inr.a.refine_2
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ Injective fun x => ⟨{x}, ⋯⟩

Proof state:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } = #α

Tactic:
apply le_antisymm

Result:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } ≤ #α

case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s // Bounded r s }

Proof state:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty { s // Bounded r s }

Tactic:
constructor

Result:
case inl.false
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ { s // Bounded r s } → False

Proof state:
case inr.a.refine_1.hr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ (type r).IsLimit

Tactic:
rw [← hr]

Result:
case inr.a.refine_1.hr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ (#α).ord.IsLimit

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ #↑(𝒫{j | r j i}) ≤ #α

Tactic:
rw [mk_powerset]

Result:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ 2 ^ #↑{j | r j i} ≤ #α

Proof state:
case inr.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ Bounded r {x}

Tactic:
apply bounded_singleton

Result:
case inr.a.refine_1.hr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ (type r).IsLimit

Proof state:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ #↑(⋃ i, 𝒫{j | r j i}) ≤ #α

Tactic:
refine mk_iUnion_le_sum_mk.trans ((sum_le_iSup (fun i => #(𝒫{ j | r j i }))).trans
  ((mul_le_max_of_aleph0_le_left ha).trans ?_))

Result:
case inr.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ #α ⊔ ⨆ i, #↑(𝒫{j | r j i}) ≤ #α

Proof state:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // Bounded r s } = #α

Tactic:
have ha := h'.aleph0_le

Result:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #{ s // Bounded r s } = #α

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // Bounded r s } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)

Result:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = #α

case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s // Bounded r s } = #α

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ ∀ (i : α), #↑(𝒫{j | r j i}) ≤ #α

Tactic:
intro i

Result:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
i : α
⊢ #↑(𝒫{j | r j i}) ≤ #α