F : Type u_1
K : Type u_2
inst✝¹⁹ : Field F
inst✝¹⁸ : Field K
inst✝¹⁷ : Algebra F K
K₁ : Type ?u.303481
K₂ : Type ?u.303484
K₃ : Type ?u.303487
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K₁
inst✝¹⁴ : Field K₂
inst✝¹³ : Field K₃
inst✝¹² : Algebra F K₁
inst✝¹¹ : Algebra F K₂
inst✝¹⁰ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E✝ : Type ?u.303905
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F E✝
inst✝⁷ : Algebra E✝ K₁
inst✝⁶ : Algebra E✝ K₂
inst✝⁵ : Algebra E✝ K₃
inst✝⁴ : IsScalarTower F E✝ K₁
inst✝³ : IsScalarTower F E✝ K₂
inst✝² : IsScalarTower F E✝ K₃
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F { x // x ∈ E }
f : { x // x ∈ E } →ₐ[F] K
this : Algebra { x // x ∈ E } { x // x ∈ E } := Algebra.id { x // x ∈ E }
⊢ fieldRange f = E
F : Type u_1
K : Type u_2
inst✝¹⁹ : Field F
inst✝¹⁸ : Field K
inst✝¹⁷ : Algebra F K
K₁ : Type ?u.303481
K₂ : Type ?u.303484
K₃ : Type ?u.303487
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K₁
inst✝¹⁴ : Field K₂
inst✝¹³ : Field K₃
inst✝¹² : Algebra F K₁
inst✝¹¹ : Algebra F K₂
inst✝¹⁰ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E✝ : Type ?u.303905
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F E✝
inst✝⁷ : Algebra E✝ K₁
inst✝⁶ : Algebra E✝ K₂
inst✝⁵ : Algebra E✝ K₃
inst✝⁴ : IsScalarTower F E✝ K₁
inst✝³ : IsScalarTower F E✝ K₂
inst✝² : IsScalarTower F E✝ K₃
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F { x // x ∈ E }
f : { x // x ∈ E } →ₐ[F] K
⊢ fieldRange f = E
letI : Algebra E E := Algebra.id E
F : Type u_1
K : Type u_2
inst✝¹⁹ : Field F
inst✝¹⁸ : Field K
inst✝¹⁷ : Algebra F K
K₁ : Type ?u.303481
K₂ : Type ?u.303484
K₃ : Type ?u.303487
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K₁
inst✝¹⁴ : Field K₂
inst✝¹³ : Field K₃
inst✝¹² : Algebra F K₁
inst✝¹¹ : Algebra F K₂
inst✝¹⁰ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E✝ : Type ?u.303905
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F E✝
inst✝⁷ : Algebra E✝ K₁
inst✝⁶ : Algebra E✝ K₂
inst✝⁵ : Algebra E✝ K₃
inst✝⁴ : IsScalarTower F E✝ K₁
inst✝³ : IsScalarTower F E✝ K₂
inst✝² : IsScalarTower F E✝ K₃
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F { x // x ∈ E }
f : { x // x ∈ E } →ₐ[F] K
this : Algebra { x // x ∈ E } { x // x ∈ E } := Algebra.id { x // x ∈ E }
g : { x // x ∈ E } ≃ₐ[F] { x // x ∈ E } := restrictNormal' f { x // x ∈ E }
⊢ fieldRange f = E
F : Type u_1
K : Type u_2
inst✝¹⁹ : Field F
inst✝¹⁸ : Field K
inst✝¹⁷ : Algebra F K
K₁ : Type ?u.303481
K₂ : Type ?u.303484
K₃ : Type ?u.303487
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K₁
inst✝¹⁴ : Field K₂
inst✝¹³ : Field K₃
inst✝¹² : Algebra F K₁
inst✝¹¹ : Algebra F K₂
inst✝¹⁰ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E✝ : Type ?u.303905
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F E✝
inst✝⁷ : Algebra E✝ K₁
inst✝⁶ : Algebra E✝ K₂
inst✝⁵ : Algebra E✝ K₃
inst✝⁴ : IsScalarTower F E✝ K₁
inst✝³ : IsScalarTower F E✝ K₂
inst✝² : IsScalarTower F E✝ K₃
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F { x // x ∈ E }
f : { x // x ∈ E } →ₐ[F] K
this : Algebra { x // x ∈ E } { x // x ∈ E } := Algebra.id { x // x ∈ E }
⊢ fieldRange f = E
let g := f.restrictNormal' E
no goals
F : Type u_1
K : Type u_2
inst✝¹⁹ : Field F
inst✝¹⁸ : Field K
inst✝¹⁷ : Algebra F K
K₁ : Type ?u.303481
K₂ : Type ?u.303484
K₃ : Type ?u.303487
inst✝¹⁶ : Field F
inst✝¹⁵ : Field K₁
inst✝¹⁴ : Field K₂
inst✝¹³ : Field K₃
inst✝¹² : Algebra F K₁
inst✝¹¹ : Algebra F K₂
inst✝¹⁰ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E✝ : Type ?u.303905
inst✝⁹ : Field E✝
inst✝⁸ : Algebra F E✝
inst✝⁷ : Algebra E✝ K₁
inst✝⁶ : Algebra E✝ K₂
inst✝⁵ : Algebra E✝ K₃
inst✝⁴ : IsScalarTower F E✝ K₁
inst✝³ : IsScalarTower F E✝ K₂
inst✝² : IsScalarTower F E✝ K₃
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F { x // x ∈ E }
f : { x // x ∈ E } →ₐ[F] K
this : Algebra { x // x ∈ E } { x // x ∈ E } := Algebra.id { x // x ∈ E }
g : { x // x ∈ E } ≃ₐ[F] { x // x ∈ E } := restrictNormal' f { x // x ∈ E }
⊢ fieldRange f = E
rw [← show E.val.comp ↑g = f from FunLike.ext_iff.mpr (f.restrictNormal_commutes E), ←
  IntermediateField.AlgHom.map_fieldRange, IntermediateField.AlgEquiv.fieldRange_eq_top g,
    ← IntermediateField.AlgHom.fieldRange_eq_map, IntermediateField.fieldRange_val]