Subalgebras over different base fields

Stream: Is there code for X?

[Patrick Lutz]

Say that I have some subalgebras of an algebra which are over different base fields and I know some equalities between them which I want to use for a series of rewrites. Is there a really easy way to do this? Lean often seems to get confused because the types are different (even though the equalities are all really equalities on the underlying subsets of the algebra). As a mwe:

import ring_theory.algebra

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : ⊤ = B :=
begin
  ext,
  apply iff_of_true algebra.mem_top,
  change x ∈ (B : set E),
  rw [← h₂, h₃, h₁],
  exact algebra.mem_top,
end

I feel like I should be able to prove the example above in a single line, but I don't see how to do so.

[Kevin Buzzard]

import field_theory.tower

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : ⊤ = B :=
by simp [subalgebra.ext_iff, set.ext_iff, algebra.mem_top, *] at *

[Kyle Miller]

A very slightly different one:

import field_theory.tower

variables (F E L : Type*) [field F] [field E] [field L] [algebra F E] [algebra L E]
variables (A B : subalgebra F E) (C : subalgebra L E)

example (h₁ : C = ⊤) (h₂ : A = B) (h₃ : (A : set E) = C) : B = ⊤ :=
by { ext, rw [←h₂, ←subalgebra.mem_coe, h₃, h₁], simp [algebra.mem_top] }

[Patrick Lutz]

Okay, nice. I had tried simp before, but not with the right lemmas I guess.