case h.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
a✝ : { x // x ∈ S }
⊢ ↑(↑(equivOfEq (_ : S = S)) a✝) = ↑(↑AlgEquiv.refl a✝)
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
⊢ equivOfEq (_ : S = S) = AlgEquiv.refl
ext
no goals
case h.a
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
a✝ : { x // x ∈ S }
⊢ ↑(↑(equivOfEq (_ : S = S)) a✝) = ↑(↑AlgEquiv.refl a✝)
rfl