# Zulip Chat Archive

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