!4#3716 FieldTheory.Tower

Stream: mathlib4

[Jeremy Tan]

In !4#3716, current line 150, this doesn't compile:
letI := divisionRingOfFiniteDimensional F K
I checked in mathlib3 (using Gitpod on Safari – finally) and there is a hidden ↥ in the type of the let declaration, which is
division_ring ↥K := division_ring_of_finite_dimensional F ↥K
The ↥ is apparently a coe_sort of some kind, relating to SetLike, but how do I translate this to mathlib4?

[Jeremy Tan]

letI := divisionRingOfFiniteDimensional F (↥K) fails with the error

failed to synthesize instance
  FiniteDimensional F { x // x ∈ K }

[Jeremy Tan]

Actually it's the same with or without the ↥

[Eric Wieser]

This is a recurring problem with FiniteDimensional; have := some_finiteDimensional fails, you have to use have : FiniteDimensional _ _ := some_finiteDImensional

[Eric Wieser]

I've pushed a fix

[Eric Rodriguez]

should it be haveI and letI? why are we using those instead of have/let?

[Eric Wieser]

I doesn't mean instance any more

[Eric Wieser]

It means inline

[Eric Wieser]

In tactic mode, the translation is {have,haveI} -> haveI, {let, letI} -> let. Lean 3's term-mode have is lean 4's tactic have

[Eric Wieser]

Mathport doesn't actually do that translation, but it could

[Eric Rodriguez]

I know this, but they seem to be being used like the lean3 ones here and I was wondering if that was maybe some of the issue

[Eric Wieser]

I think the issue is just that the instance cache gets confused by FiniteDimensional which is an abbreviation