Theorem: aux (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
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 • ⟨μ, ⋯⟩ ^ ↑x = l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
apply_fun algebraMap (𝓞 K) (𝓞 K ⧸ I) at h
State after:
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 :
  (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (∑ x : Fin t, f x • ⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)

State before:
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 :
  (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (∑ x : Fin t, f x • ⟨μ, ⋯⟩ ^ ↑x) =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
simp only [map_sum, map_zsmul] at h
State after:
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
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)

State before:
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
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) l = ∑ x : Fin t, ↑(f x)
Tactic:
convert h.symm using 1
State after:
case h.e'_3
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) = ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)

State before:
case h.e'_3
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) = ∑ x : Fin t, f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
congr
State after:
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)

State before:
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)
Tactic:
funext x
State after:
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)

State before:
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)
Tactic:
have : (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (p : ℕ) = 1 := by
  ext
  push_cast
  exact hμ.pow_eq_one
State after:
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
this : ⟨μ, ⋯⟩ ^ ↑p = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)

State before:
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
this : ⟨μ, ⋯⟩ ^ ↑p = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
have := hζ.unit'_coe.eq_one_mod_sub_of_pow this
State after:
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
this✝ : ⟨μ, ⋯⟩ ^ ↑p = 1
this : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ⟨μ, ⋯⟩ = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)

State before:
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
this✝ : ⟨μ, ⋯⟩ ^ ↑p = 1
this : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ⟨μ, ⋯⟩ = 1
⊢ ↑(f x) = f x • (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (⟨μ, ⋯⟩ ^ ↑x)
Tactic:
simp only [map_pow (algebraMap (𝓞 K) (𝓞 K ⧸ I)), this, one_pow, zsmul_one]
State after:
no goals

State before:
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
⊢ ⟨μ, ⋯⟩ ^ ↑p = 1
Tactic:
ext
State after:
case a
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
⊢ ↑(⟨μ, ⋯⟩ ^ ↑p) = ↑1

State before:
case a
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
⊢ ↑(⟨μ, ⋯⟩ ^ ↑p) = ↑1
Tactic:
push_cast
State after:
case a
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
⊢ μ ^ ↑p = 1

State before:
case a
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
⊢ μ ^ ↑p = 1
Tactic:
exact hμ.pow_eq_one
State after:
no goals