Working with nested intermediate fields

Stream: new members

[Michał Staromiejski]

I'm trying to prove things in field theory and arrived at something that I don't yet understand regarding (nested) subtyping.
Here's my mwe:

import Mathlib.FieldTheory.Adjoin
import Mathlib.LinearAlgebra.Dimension.Finrank

open scoped IntermediateField /- `F⟮a⟯` notation -/

def test (F K : Type u) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K]
    (E : IntermediateField F K) (a : E) : ℕ :=
  FiniteDimensional.finrank F⟮a⟯ E

The error is in the last line saying: failed to synthesize Module ↥(IntermediateField.lift F⟮a⟯) ↥E.
As far as I understand, Lean tries to reinterpret F⟮a⟯ as IntermediateField F K (IntermediateField.lift F⟮a⟯) and then it cannot find instances existing in Mathlib for towers of extensions.
How to properly handle such cases?

[Michał Staromiejski]

Ok, I was able to workaround by

import Mathlib.FieldTheory.Adjoin
import Mathlib.LinearAlgebra.Dimension.Finrank

open scoped IntermediateField -- `F⟮a⟯` notation

variable (F K : Type u) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K]

noncomputable def codeg (a : K) : ℕ := FiniteDimensional.finrank F⟮a⟯ K

variable (E : IntermediateField F K) (a : E)

noncomputable def test : ℕ := codeg F E a

But I'm still wondering if there is another way to work with such towers...
The following approaches also failed unless I explicitely add typeclass parameter:

import Mathlib.FieldTheory.Adjoin
import Mathlib.LinearAlgebra.Dimension.Finrank

open scoped IntermediateField -- `F⟮a⟯` notation

variable (F K : Type u) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K]
variable (E : IntermediateField F K) (a : E)

-- does not work
noncomputable def test2 (E₁ : IntermediateField F E) : ℕ := FiniteDimensional.finrank E₁ E
noncomputable def test3 (E₁ : IntermediateField F K) (h : E₁ ≤ E) : ℕ := FiniteDimensional.finrank E₁ E

-- works but does not work "inline" with `haveI : ... := inferInstance`
noncomputable def test' [Algebra F⟮a⟯ E] : ℕ := FiniteDimensional.finrank F⟮a⟯ E
noncomputable def test2' (E₁ : IntermediateField F E) [Algebra E₁ E] : ℕ := FiniteDimensional.finrank E₁ E
noncomputable def test3' (E₁ : IntermediateField F K) (h : E₁ ≤ E) [Algebra E₁ E] : ℕ := FiniteDimensional.finrank E₁ E