internlm/Lean-Github huggingface dataset:
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)⁻¹)
⊢ (∏ 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
Tactic:
rw [← map_zpow, Units.coe_map_inv]
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) (↑(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)⁻¹)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) *
      (Algebra.norm k) ((algebraMap (𝓞 K) K) (↑(algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)) =
    1
Tactic:
simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe]
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) ((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)⁻¹)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) *
      (Algebra.norm k) ((algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)) =
    1
Tactic:
have hcoe1 :
    algebraMap (𝓞 k) k (((ζ ^ (p : ℕ)) ^ a)⁻¹).1 = ((((ζ : 𝓞 k) : k) ^ (p : ℕ)) ^ a)⁻¹ := by
  convert (Units.coe_map_inv ((algebraMap (𝓞 k) k) : (𝓞 k) →* k) ((ζ ^ (p : ℕ)) ^ a)).symm
  simp
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) *
      (Algebra.norm k) ((algebraMap (𝓞 K) K) ((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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) *
      (Algebra.norm k) ((algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)) =
    1
Tactic:
rw [hcoe, RingOfInteger.coe_algebraMap_apply, Algebra.norm_algebraMap, hKL, ← map_pow,
  ← Units.val_pow_eq_pow_val, inv_pow, ← zpow_natCast, ← zpow_mul, mul_comm a, zpow_mul,
    zpow_natCast, hcoe1]
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ 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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ a)⁻¹ = 1
Tactic:
apply_fun Additive.toMul at ha
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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha : Additive.toMul (∑ i : Fin n, ι i • η i) = Additive.toMul ((a * ↑↑p) • Additive.ofMul ζ)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ 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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha : Additive.toMul (∑ i : Fin n, ι i • η i) = Additive.toMul ((a * ↑↑p) • Additive.ofMul ζ)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ a)⁻¹ = 1
Tactic:
apply_fun ((↑) : (𝓞 k)ˣ → k) at ha
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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  (algebraMap (𝓞 k) k) ↑(Additive.toMul (∑ i : Fin n, ι i • η i)) =
    (algebraMap (𝓞 k) k) ↑(Additive.toMul ((a * ↑↑p) • Additive.ofMul ζ))
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ 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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  (algebraMap (𝓞 k) k) ↑(Additive.toMul (∑ i : Fin n, ι i • η i)) =
    (algebraMap (𝓞 k) k) ↑(Additive.toMul ((a * ↑↑p) • Additive.ofMul ζ))
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ a)⁻¹ = 1
Tactic:
simp only [toMul_sum, toMul_zsmul, Units.coe_prod, map_prod, hη,
  Units.coe_zpow, toMul_ofMul] at ha
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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  ∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x =
    (algebraMap (𝓞 k) k) ↑ζ ^ (a * ↑↑p)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ 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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  ∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x =
    (algebraMap (𝓞 k) k) ↑ζ ^ (a * ↑↑p)
⊢ (∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x) * ((↑↑ζ ^ ↑p) ^ a)⁻¹ = 1
Tactic:
rwa [← zpow_natCast, ← zpow_mul, mul_comm _ a, mul_inv_eq_one₀]
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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  ∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x =
    (algebraMap (𝓞 k) k) ↑ζ ^ (a * ↑↑p)
⊢ ↑↑ζ ^ (a * ↑↑p) ≠ 0
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)ˣ
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)⁻¹)
hcoe1 : (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
ha :
  ∏ x : Fin n, (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑(Additive.toMul (H x))) ^ ι x =
    (algebraMap (𝓞 k) k) ↑ζ ^ (a * ↑↑p)
⊢ ↑↑ζ ^ (a * ↑↑p) ≠ 0
Tactic:
simp [← Units.coe_zpow]
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)))
hcoe : (algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹) = ↑((algebraMap (𝓞 k) (𝓞 K)) ↑(ζ ^ a)⁻¹)
⊢ (algebraMap (𝓞 k) k) ↑((ζ ^ ↑p) ^ a)⁻¹ = ((↑↑ζ ^ ↑p) ^ a)⁻¹
Tactic:
convert (Units.coe_map_inv ((algebraMap (𝓞 k) k) : (𝓞 k) →* k) ((ζ ^ (p : ℕ)) ^ a)).symm
Proof state after:
case h.e'_3
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)⁻¹)
⊢ ((↑↑ζ ^ ↑p) ^ a)⁻¹ = ↑((Units.map ↑(algebraMap (𝓞 k) k)) ((ζ ^ ↑p) ^ a))⁻¹