suffices finrank K L = 1 by
  obtain ⟨a, ha⟩ := mem_span_singleton.1 <| (eq_top_iff'.1 <|
    (finrank_eq_one_iff_of_nonzero _ one_ne_zero).1 this) η
  rw [← Algebra.algebraMap_eq_smul_one] at ha
  rw [← ha, Algebra.norm_algebraMap, this, pow_one] at hη
  exact ⟨1, by simp [← ha, hη]⟩
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ ∃ ε, η = ε / σ ε
case pos
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : NumberField K
inst✝² : Algebra K L
inst✝¹ : IsGalois K L
inst✝ : FiniteDimensional K L
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : L
hη : (Algebra.norm K) η = 1
hone : orderOf σ = 1
⊢ finrank K L = 1