-- 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:
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:
apply ciSup_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:
case inl.false.mk
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
s : Set α
hs : Bounded r s
⊢ False

Tactic:
exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)

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 : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫{j | r j i}
⊢ #α ⊔ ⨆ i, #↑(𝒫{j | r j i}) ≤ #α

Tactic:
rw [max_eq_left]

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 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

Tactic:
rintro ⟨s, hs⟩

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

Proof state:
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

Tactic:
rw [mk_eq_zero_iff]

Result:
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 }

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:
have : { s : Set α | Bounded r s } = ⋃ i, 𝒫{ j | r j i } := setOf_exists _

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}
⊢ #{ 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 : α
⊢ (typein r).toRelEmbedding i < type r

Tactic:
apply typein_lt_type

Result:
no goals

Proof state:
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}, ⋯⟩

Tactic:
intro a b hab

Result:
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 : ℵ₀ ≤ #α
a b : α
hab : (fun x => ⟨{x}, ⋯⟩) a = (fun x => ⟨{x}, ⋯⟩) b
⊢ a = b

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

Tactic:
have h' : IsStrongLimit #α := ⟨ha, h⟩

Result:
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 } = #α

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 } = #α

Tactic:
rw [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 } = 0

Proof state:
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 : ℵ₀ ≤ #α
a b : α
hab : (fun x => ⟨{x}, ⋯⟩) a = (fun x => ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

Result:
no goals