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

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
Tactic:
have := Units.coe_map_inv' (N := 𝓞 K ⧸ I) (algebraMap (𝓞 K) (𝓞 K ⧸ I)) (unitGalConj K p u)
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
Tactic:
rw [Units.val_mul, map_mul, ← this, Units.mul_inv_eq_one, Units.coe_map , MonoidHom.coe_coe]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
haveI := Fact.mk hp
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
have hu := hζ.integralPowerBasis'.basis.sum_repr u
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
let a := hζ.integralPowerBasis'.basis.repr
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
let φn := hζ.integralPowerBasis'.dim
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
hu :
  ∑ i : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) i • hζ.integralPowerBasis'.basis i = ↑u
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
simp_rw [PowerBasis.basis_eq_pow, IsPrimitiveRoot.integralPowerBasis'_gen] at hu
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
have hu' := congr_arg (intGal ↑(galConj K p)) hu
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
replace hu' :
    ∑ x : Fin φn, (a u) x • (intGal ↑(galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) =
    unitGalConj K p u := by
  refine' Eq.trans _ hu'
  rw [map_sum]
  congr 1
  ext x
  congr 1
  rw [map_zsmul]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
have : ∀ x : Fin φn, intGal ((galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) =
    ⟨ζ⁻¹, hζ.inv.isIntegral p.pos⟩ ^ (x : ℕ) := by
  intro x
  ext
  simp only [map_pow, intGal_apply_coe, RingOfIntegers.map_mk, AlgHom.coe_coe, inv_pow]
  rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝¹ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this✝ : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
this : ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝¹ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this✝ : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
this : ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
conv_lhs at hu' =>
  congr
  congr
  ext a
  rw [this a]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝¹ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this✝ : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ a_1 : Fin φn, (a ↑u) a_1 • ⟨ζ⁻¹, ⋯⟩ ^ ↑a_1 = ↑((unitGalConj K p) u)
this : ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝¹ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this✝ : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ a_1 : Fin φn, (a ↑u) a_1 • ⟨ζ⁻¹, ⋯⟩ ^ ↑a_1 = ↑((unitGalConj K p) u)
this : ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
Tactic:
exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
Tactic:
refine' Eq.trans _ hu'
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
rw [map_sum]
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    ∑ x : Fin hζ.integralPowerBasis'.dim,
      (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    ∑ x : Fin hζ.integralPowerBasis'.dim,
      (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
congr 1
State after:
case e_f
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (fun x => (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = fun x =>
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)

State before:
case e_f
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
⊢ (fun x => (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = fun x =>
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
ext x
State after:
case e_f.h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ ↑((a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) =
    ↑((intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x))

State before:
case e_f.h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ ↑((a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) =
    ↑((intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x))
Tactic:
congr 1
State after:
case e_f.h.h.e_x
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)

State before:
case e_f.h.h.e_x
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' :
  (intGal ↑(galConj K p))
      (∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x) =
    (intGal ↑(galConj K p)) ↑u
x : Fin φn
⊢ (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) =
    (intGal ↑(galConj K p)) ((hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x)
Tactic:
rw [map_zsmul]
State after:
no goals

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
⊢ ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
Tactic:
intro x
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
Tactic:
ext
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ ↑((intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = ↑(⟨ζ⁻¹, ⋯⟩ ^ ↑x)

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ ↑((intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x)) = ↑(⟨ζ⁻¹, ⋯⟩ ^ ↑x)
Tactic:
simp only [map_pow, intGal_apply_coe, RingOfIntegers.map_mk, AlgHom.coe_coe, inv_pow]
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (galConj K p) ζ ^ ↑x = (ζ ^ ↑x)⁻¹

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (galConj K p) ζ ^ ↑x = (ζ ^ ↑x)⁻¹
Tactic:
rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow]
State after:
no goals