internlm/Lean-Github huggingface dataset:
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
⊢ 2 ∉ Ideal.span {↑hζ.unit' - 1}
Tactic:
intro h2m
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
have := Ideal.sub_mem I hpm (Ideal.mul_mem_right (↑k) I h2m)
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : ↑↑p - 2 * ↑k ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : ↑↑p - 2 * ↑k ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
rw [sub_eq_of_eq_add hk] at this
Proof state after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : 1 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Theorem: IsPrimitiveRoot.two_not_mem_one_sub_zeta
Proof state before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hp : Fact (↑p).Prime
h : p ≠ 2
hpm : ↑↑p ∈ Ideal.span {↑hζ.unit' - 1}
k : ℕ
hk : ↑↑p = 1 + 2 * ↑k
h2m : 2 ∈ Ideal.span {↑hζ.unit' - 1}
this : 1 ∈ Ideal.span {↑hζ.unit' - 1}
⊢ False
Tactic:
exact hζ.isPrime_one_sub_zeta.ne_top (Ideal.eq_top_of_isUnit_mem I this isUnit_one)
Proof state after:
no goals
Theorem: IsUnit.eq_mul_left_iff
Proof state before:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ x = y * x ↔ y = 1
Tactic:
nth_rw 1 [← one_mul x]
Proof state after:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ 1 * x = y * x ↔ y = 1
Theorem: IsUnit.eq_mul_left_iff
Proof state before:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ 1 * x = y * x ↔ y = 1
Tactic:
rw [eq_comm, hx.mul_left_injective.eq_iff]
Proof state after:
no goals
Theorem: map_two
Proof state before:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ f 2 = 2
Tactic:
rw [← one_add_one_eq_two, map_add, map_one]
Proof state after:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ 1 + 1 = 2
Theorem: map_two
Proof state before:
p : ℕ+
K : Type ?u.154058
inst✝⁶ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁵ : NumberField K
inst✝⁴ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
T : Type u_2
F : Type u_3
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring T
inst✝¹ : FunLike F S T
inst✝ : RingHomClass F S T
f : F
⊢ 1 + 1 = 2
Tactic:
exact one_add_one_eq_two
Proof state after:
no goals
Theorem: neg_one_eq_one_iff_two_eq_zero
Proof state before:
p : ℕ+
K : Type ?u.162504
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
M : Type u_1
inst✝ : AddGroupWithOne M
⊢ -1 = 1 ↔ 2 = 0
Tactic:
rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
Proof state after:
no goals
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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)
Proof 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
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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]
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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]
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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]
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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]
Proof 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)
Theorem: unit_inv_conj_not_neg_zeta_runity_aux
Proof 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
Proof state after:
no goals