case refine'_1
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
⊢ ∀ (b : Cardinal), b ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a} → cof o ≤ b

case refine'_2
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
⊢ cof o ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
⊢ cof o = sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
refine' le_antisymm (le_csInf (cof_lsub_def_nonempty o) _) (csInf_le' _)
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
⊢ cof o ≤ (#ι)
case refine'_1
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
⊢ ∀ (b : Cardinal), b ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a} → cof o ≤ b
rintro a ⟨ι, f, hf, rfl⟩
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
⊢ cof (type fun x x_1 => x < x_1) ≤ (#ι)
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
⊢ cof o ≤ (#ι)
rw [← type_lt o]
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
this : typein (fun x x_1 => x < x_1) a < o
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
have := typein_lt_self a
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
this : ∃ i, typein (fun x x_1 => x < x_1) a ≤ f i
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
this : typein (fun x x_1 => x < x_1) a < o
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
simp_rw [← hf, lt_lsub_iff] at this
case refine'_1.intro.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
case refine'_1.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
this : ∃ i, typein (fun x x_1 => x < x_1) a ≤ f i
⊢ ∃ b, b ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f ∧ ¬b < a
cases' this with i hi
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
s t : ↑((typein fun x x_1 => x < x_1) ⁻¹' range f)
hst :
  (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) s =
    (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) t
H : f ((fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) s) =
  f ((fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) t) :=
  congr_arg f hst
⊢ s = t
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
s t : ↑((typein fun x x_1 => x < x_1) ⁻¹' range f)
hst :
  (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) s =
    (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) t
⊢ s = t
let H := congr_arg f hst
no goals
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
s t : ↑((typein fun x x_1 => x < x_1) ⁻¹' range f)
hst :
  (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) s =
    (fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) t
H : f ((fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) s) =
  f ((fun s => choose (_ : ↑s ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f)) t) :=
  congr_arg f hst
⊢ s = t
rwa [Classical.choose_spec s.prop, Classical.choose_spec t.prop, typein_inj,
  Subtype.coe_inj] at H
case refine'_1.intro.intro.intro.intro.refine'_1
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ f i < lsub f
case refine'_1.intro.intro.intro.intro.refine'_1
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ f i < type fun x x_1 => x < x_1
rw [type_lt, ← hf]
no goals
case refine'_1.intro.intro.intro.intro.refine'_1
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ f i < lsub f
apply lt_lsub
case refine'_1.intro.intro.intro.intro.refine'_2
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ f i ∈ range f
case refine'_1.intro.intro.intro.intro.refine'_2
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ enum (fun x x_1 => x < x_1) (f i) (_ : f i < type fun x x_1 => x < x_1) ∈ (typein fun x x_1 => x < x_1) ⁻¹' range f
rw [mem_preimage, typein_enum]
no goals
case refine'_1.intro.intro.intro.intro.refine'_2
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ f i ∈ range f
exact mem_range_self i
no goals
case refine'_1.intro.intro.intro.intro.refine'_3
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
a : (Quotient.out o).α
i : ι
hi : typein (fun x x_1 => x < x_1) a ≤ f i
⊢ ¬enum (fun x x_1 => x < x_1) (f i) (_ : f i < type fun x x_1 => x < x_1) < a
rwa [← typein_le_typein, typein_enum]
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
⊢ cof o ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
⊢ cof o ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
let f : S → Ordinal := fun s => typein LT.lt s.val
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < o
⊢ a < lsub f
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
⊢ cof o ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
refine'
  ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self i) (le_of_forall_lt fun a ha => _), by
    rwa [type_lt o] at hS'⟩
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < type fun x x_1 => x < x_1
⊢ a < lsub f
case refine'_2.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < o
⊢ a < lsub f
rw [← type_lt o] at ha
case refine'_2.intro.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < type fun x x_1 => x < x_1
b : (Quotient.out o).α
hb : b ∈ S
hb' : a ≤ typein LT.lt b
⊢ a < lsub f
case refine'_2.intro.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < type fun x x_1 => x < x_1
b : (Quotient.out o).α
hb : b ∈ S
hb' : ¬(fun x x_1 => x < x_1) b (enum (fun x x_1 => x < x_1) a ha)
⊢ a < lsub f
rw [← typein_le_typein, typein_enum] at hb'
no goals
case refine'_2.intro.intro.intro.intro
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
a : Ordinal
ha : a < type fun x x_1 => x < x_1
b : (Quotient.out o).α
hb : b ∈ S
hb' : a ≤ typein LT.lt b
⊢ a < lsub f
exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)
no goals
α : Type ?u.13677
r : α → α → Prop
o : Ordinal
S : Set (Quotient.out o).α
hS : Unbounded (fun x x_1 => x < x_1) S
hS' : (#↑S) = cof (type fun x x_1 => x < x_1)
f : ↑S → Ordinal := fun s => typein LT.lt ↑s
⊢ (#↑S) = cof o
rwa [type_lt o] at hS'