## Stream: new members

### Topic: extract part of goal into separate variable

#### Eric Rodriguez (Apr 06 2022 at 01:02):

I can only find this being used in mathlib in docs#polynomial.gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, it definitely should be in the tips and tricks page

#### Adam Topaz (Apr 06 2022 at 01:05):

We use it quite frequently in LTE.

#### Matt Diamond (Apr 06 2022 at 02:27):

I'm running into one other roadblock with the above code... trying to prove this:

example : ∀ (o : ordinal), beth o ≥ aleph o := begin

end


and Lean isn't happy about universes:

type mismatch at application
aleph o
term
o
has type
ordinal.{?l_1} : Type (?l_1+1)
but is expected to have type
ordinal.{(max (?l_1+1) ?l_2)} : Type ((max (?l_1+1) ?l_2)+1)


I tried changing ordinal to ordinal.{max (u+1) v} but that just led to this new error:

type mismatch at application
aleph o
term
o
has type
ordinal.{(max (u+1) v)} : Type ((max (u+1) v)+1)
but is expected to have type
ordinal.{(max ((max (u+1) v)+1) ?l_1)} : Type ((max ((max (u+1) v)+1) ?l_1)+1)


Is there any way I can get past this? Do I need to modify my definition of beth to explicitly declare universe variables?

#### Notification Bot (Apr 06 2022 at 02:27):

Matt Diamond has marked this topic as unresolved.

#### Junyan Xu (Apr 06 2022 at 05:43):

I think you won't get the universe issue with the definition beth':

noncomputable
def beth' (o: ordinal) : cardinal :=
ordinal.limit_rec_on o
(cardinal.aleph 0)
(λ _ b, 2 ^ b)
(λ lim _ IH, Sup (lim.brange IH))

set_option pp.universes true
#check beth
#check beth'

beth.{u_1 u_2} : ordinal.{u_1} → cardinal.{(max (u_1+1) u_2)}
beth'.{u_1 u_2} : ordinal.{u_1} → cardinal.{u_2}


(Notice that you need bdd_above(using the disjoint union / Sigma type) for Sup to be well behaved: docs#le_cSup )

I think it's good in this case to specify explicit universes like

universe u
def beth' (o: ordinal.{u}) : cardinal.{u} :=


#### Junyan Xu (Apr 06 2022 at 05:53):

The universe issue with your approach is that the indexing type ι in

noncomputable def cardinal.sup {ι : Type u} (f : ι → cardinal.{max u v}) : cardinal :=


is { o // o < lim } : Type (u_1+1).

Last updated: Dec 20 2023 at 11:08 UTC