extract part of goal into separate variable

Stream: new members

[Eric Rodriguez]

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]

We use it quite frequently in LTE.

[Matt Diamond]

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]

Matt Diamond has marked this topic as unresolved.

[Junyan Xu]

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]

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