funext x
case h.e'_3.e_f
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (fun x => ↑(f x)) = fun x => f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
case h.e'_3.e_f.h
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
t : ℕ
l : 𝓞 K
f : Fin t → ℤ
μ : K
hμ : IsPrimitiveRoot μ ↑p
h :
  ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
x : Fin t
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)