-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) :
    #{ s : Set α // #s < cof (#α).ord } = #α

Proof state:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α = 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
simp [ha]

Result:
no goals

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

Tactic:
apply mk_le_mk_of_subset

Result:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ (fun x =>
      Quotient.liftOn₂ (#↑x) (#α).ord.cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
        ¬Quotient.liftOn₂ (#α).ord.cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1) ⊆
    fun x => ∃ a, ∀ b ∈ x, r b a

Proof state:
case inr.intro.intro.a.refine_2
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
a b : α
hab : (fun x => ⟨{x}, ⋯⟩) a = (fun x => ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

Result:
no goals

Proof state:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (#α).ord.cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
      ¬Quotient.liftOn₂ (#α).ord.cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1
⊢ s ∈ fun x => ∃ a, ∀ b ∈ x, r b a

Tactic:
rw [hr] at hs

Result:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (type r).cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
      ¬Quotient.liftOn₂ (type r).cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1
⊢ s ∈ fun x => ∃ a, ∀ b ∈ x, r b a

Proof state:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (type r).cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
      ¬Quotient.liftOn₂ (type r).cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1
⊢ s ∈ fun x => ∃ a, ∀ b ∈ x, r b a

Tactic:
exact lt_cof_type hs

Result:
no goals

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

Tactic:
haveI := wo

Result:
case inr.intro.intro
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Proof state:
case inr.intro.intro.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
x : α
⊢ 1 < (#α).ord.cof

Tactic:
exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (isLimit_ord h'.aleph0_le))

Result:
no goals

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

Tactic:
intro a b hab

Result:
case inr.intro.intro.a.refine_2
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
a b : α
hab : (fun x => ⟨{x}, ⋯⟩) a = (fun x => ⟨{x}, ⋯⟩) b
⊢ a = b

Proof state:
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
⊢ #{ s // #↑s < (#α).ord.cof } = #α

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

Result:
case inl
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α = 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

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

Tactic:
apply le_antisymm

Result:
case inr.intro.intro.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ #{ s // #↑s < (#α).ord.cof } ≤ #α

case inr.intro.intro.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }

Proof state:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ (fun x =>
      Quotient.liftOn₂ (#↑x) (#α).ord.cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
        ¬Quotient.liftOn₂ (#α).ord.cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1) ⊆
    fun x => ∃ a, ∀ b ∈ x, r b a

Tactic:
intro s hs

Result:
case inr.intro.intro.a.h
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
s : Set α
hs :
  s ∈ fun x =>
    Quotient.liftOn₂ (#↑x) (#α).ord.cof (fun α β => Nonempty (α ↪ β)) instLE.proof_1 ∧
      ¬Quotient.liftOn₂ (#α).ord.cof (#↑x) (fun α β => Nonempty (α ↪ β)) instLE.proof_1
⊢ s ∈ fun x => ∃ a, ∀ b ∈ x, r b a

Proof state:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

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

Result:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Proof state:
case inr.intro.intro.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ #{ s // #↑s < (#α).ord.cof } ≤ #α

Tactic:
conv_rhs => rw [← mk_bounded_subset h hr]

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

Proof state:
case inr
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
rcases ord_eq α with ⟨r, wo, hr⟩

Result:
case inr.intro.intro
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Proof state:
case inr.intro.intro.a
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }

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

Result:
case inr.intro.intro.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
x : α
⊢ #↑{x} < (#α).ord.cof

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