Bottom subalgebra over fields is finite-dimensional

Stream: new members

[Sebastian Monnet]

Let $L/K$ be a field extension. I'm trying to show that ⊥ is finite-dimensional over $K$. Here's my attempt:

import field_theory.galois

lemma fin_dim_bot (K L : Type*) [field K] [field L] [algebra K L] : finite_dimensional K (⊥ : intermediate_field K L) :=
begin
  exact finite_dimensional_of_dim_eq_one (subalgebra.dim_bot),
end

The problem is that the subalgebra.dim_bot has type module.rank ?m_1 ↥⊥ = 1, and I need it to have type module.rank K ↥⊥ = 1. I've seen this ?m_1 notation before, and I think it means that the result is true for any type, but I don't know how to insert the type I want (namely K). I've tried things like subalgebra.dim_bot K and subalgebra.dim_bot K L, but none of it has worked.

I'd appreciate any guidance or explanation of what I need to do.

[Eric Wieser]

set_option pp.implicit true will give a clearer message

[Eric Wieser]

begin
  refine finite_dimensional_of_dim_eq_one _,
  convert subalgebra.dim_bot,
  sorry
end

Might help you understand what's going wrong

[Eric Wieser]

(untested)

[Sebastian Monnet]

Hmm, well I solved the problem by using your refine tactic and then just whacking it with simp. I still have no idea what the original problem was, or what simp actually did in this instance.

Using convert subalgebra.dim_bot creates six goals, some of which are really weird. The first one is module.rank K ↥⊥ = module.rank ?m_1 ↥⊥, which seems to be exactly the same as the original problem, since I don't know what this ?m_1 is or how to interact with it.

[Eric Wieser]

?m_1 means " I can't work out what to put here"

[Eric Wieser]

Probably because the bits you can't see without pp.implicit true don't match at all

[Eric Wieser]

simp? will tell you what simp did

[Stuart Presnell]

This might be a way to see more clearly what's going on:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tips.20and.20tricks/near/265410441