internlm/Lean-Github huggingface dataset:
Theorem: Hilbert92ish_aux0
Proof state before:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (Algebra.norm k) ((algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ)) ^ ↑p ^ (h - 1) = 1
Tactic:
rw [Algebra.norm_algebraMap, hKL, ← pow_mul]
Proof state after:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ (↑p * ↑p ^ (h - 1)) = 1
Theorem: Hilbert92ish_aux0
Proof state before:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ (↑p * ↑p ^ (h - 1)) = 1
Tactic:
nth_rewrite 1 [← pow_one (p : ℕ)]
Proof state after:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ (↑p ^ 1 * ↑p ^ (h - 1)) = 1
Theorem: Hilbert92ish_aux0
Proof state before:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ (↑p ^ 1 * ↑p ^ (h - 1)) = 1
Tactic:
rw [← pow_add]
Proof state after:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ (1 + (h - 1)) = 1
Theorem: Hilbert92ish_aux0
Proof state before:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ (algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ (1 + (h - 1)) = 1
Tactic:
apply (hζ.pow_eq_one_iff_dvd _).2
Proof state after:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ ↑p ^ h ∣ ↑p ^ (1 + (h - 1))
Theorem: Hilbert92ish_aux0
Proof state before:
case h.left
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ ↑p ^ h ∣ ↑p ^ (1 + (h - 1))
Tactic:
cases h <;> simp [add_comm]
Proof state after:
no goals
Theorem: Hilbert92ish_aux0
Proof state before:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
⊢ ∀ (ε : (𝓞 K)ˣ), (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
Tactic:
intro ε hε
Proof state after:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ False
Theorem: Hilbert92ish_aux0
Proof state before:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ False
Tactic:
apply H ε
Proof state after:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
Theorem: Hilbert92ish_aux0
Proof state before:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
Tactic:
rw [← hε]
Proof state after:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1))
Theorem: Hilbert92ish_aux0
Proof state before:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1))
Tactic:
simp only [ge_iff_le, Units.val_pow_eq_pow_val, Units.coe_map, MonoidHom.coe_coe,
  SubmonoidClass.coe_pow]
Proof state after:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) (↑η ^ ↑p ^ (h - 1))
Theorem: Hilbert92ish_aux0
Proof state before:
case h.right
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
H :
  ∀ (ε : (𝓞 K)ˣ),
    (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) ≠ (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
η : (𝓞 K)ˣ := (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑(η ^ ↑p ^ (h - 1)) = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
⊢ (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) (↑η ^ ↑p ^ (h - 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Hilbert92ish_aux1
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
n : ℕ
H : Fin n → Additive (𝓞 K)ˣ
ζ : (𝓞 k)ˣ
a : ℤ
ι : Fin n → ℤ
η : Fin n → Additive (𝓞 k)ˣ
ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
hη :
  ∀ (i : Fin n),
    (algebraMap (𝓞 k) k) ↑(Additive.toMul (η i)) = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H i)))
⊢ (Algebra.norm k)
      ((algebraMap (𝓞 K) K)
        ↑(Additive.toMul (∑ i : Fin n, ι i • H i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a))) =
    1
Tactic:
have hcoe : ((algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ((ζ ^ a)⁻¹).1)) =
  algebraMap (𝓞 k) (𝓞 K) ((ζ ^ a)⁻¹).1 := rfl
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
n : ℕ
H : Fin n → Additive (𝓞 K)ˣ
ζ : (𝓞 k)ˣ
a : ℤ
ι : Fin n → ℤ
η : Fin n → Additive (𝓞 k)ˣ
ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
hη :
  ∀ (i : Fin n),
    (algebraMap (𝓞 k) k) ↑(Additive.toMul (η i)) = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H i)))
hcoe : (algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹) = ↑((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)
⊢ (Algebra.norm k)
      ((algebraMap (𝓞 K) K)
        ↑(Additive.toMul (∑ i : Fin n, ι i • H i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a))) =
    1
Theorem: Hilbert92ish_aux1
Proof state before:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
n : ℕ
H : Fin n → Additive (𝓞 K)ˣ
ζ : (𝓞 k)ˣ
a : ℤ
ι : Fin n → ℤ
η : Fin n → Additive (𝓞 k)ˣ
ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
hη :
  ∀ (i : Fin n),
    (algebraMap (𝓞 k) k) ↑(Additive.toMul (η i)) = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H i)))
hcoe : (algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹) = ↑((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)
⊢ (Algebra.norm k)
      ((algebraMap (𝓞 K) K)
        ↑(Additive.toMul (∑ i : Fin n, ι i • H i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a))) =
    1
Tactic:
simp only [toMul_sum, toMul_zsmul, zpow_neg, Units.val_mul, Units.coe_prod, map_mul, map_prod,
  Units.coe_zpow, map_mul, map_prod, ← Units.coe_val_inv, norm_map_inv, norm_map_zpow,
  Units.coe_map]
Proof state after:
p : ℕ+
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : NumberField K
k : Type u_2
inst✝¹¹ : Field k
inst✝¹⁰ : NumberField k
hp : (↑p).Prime
G : Type u_3
H✝ : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : CommGroup H✝
inst✝⁷ : Fintype H✝
hCard : Fintype.card H✝ = ↑p
σ✝ : H✝
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁶ : DistribMulAction H✝ G
inst✝⁵ : Module.Free ℤ G
inst✝⁴ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝³ : Algebra k K
inst✝² : IsGalois k K
inst✝¹ : FiniteDimensional k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
n : ℕ
H : Fin n → Additive (𝓞 K)ˣ
ζ : (𝓞 k)ˣ
a : ℤ
ι : Fin n → ℤ
η : Fin n → Additive (𝓞 k)ˣ
ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
hη :
  ∀ (i : Fin n),
    (algebraMap (𝓞 k) k) ↑(Additive.toMul (η i)) = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H i)))
hcoe : (algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹) = ↑((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) *
      (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑((Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ a)⁻¹) =
    1