internlm/Lean-Github huggingface dataset:
Theorem: Hilbert92ish
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.right.refine_1.succ.intro.intro
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι (Fin.last (r + 1))
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε'✝ : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
this : i = Fin.last (r + 1)
h : ℕ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ (h + 1))
ε' : (𝓞 k)ˣ
hε' : ε' ^ ↑p = NE
hζ'' : ↑p = 1
ε'' : (𝓞 k)ˣ
hε'' : E = (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ε''
hE : (algebraMap k K) (↑↑ζ ^ ↑p ^ h) = 1
⊢ False
Tactic:
exact hp.one_lt.ne.symm hζ''
Proof state after:
no goals
Theorem: Hilbert92ish
Proof state before:
case intro
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 σ
hpodd : ↑p ≠ 2
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
hE : (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε' : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
i : Fin (r + 1)
ha' : ¬↑↑p ∣ ι i.castSucc
ha'' : ζ = 1 → i.castSucc ≠ Fin.last (r + 1)
⊢ False
Tactic:
exact ha' (hε' i)
Proof state after:
no goals
Theorem: Hilbert92ish
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.right.refine_1.zero.a.h
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι (Fin.last (r + 1))
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε' : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
this : i = Fin.last (r + 1)
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ 0)
hE : (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (0 - 1) = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
⊢ ↑↑ζ = ↑↑1
Tactic:
simpa using hζ
Proof state after:
no goals
Theorem: Hilbert92ish
Proof state before:
case intro.intro
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
this : i = Fin.last (r + 1)
h : ℕ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ (h + 1))
hE :
  (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h + 1 - 1) = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
α β : ℤ
hαβ : α * ↑↑p + β * ι (Fin.last (r + 1)) = 1
ι' : Fin (r + 1) → ℤ
hι' : ∀ (x : Fin (r + 1)), ι x.castSucc = ↑↑p * ι' x
ha : Additive.ofMul NE = ↑↑p • (α • Additive.ofMul NE + β • (a • Additive.ofMul ζ - ∑ x : Fin (r + 1), ι' x • N x))
⊢ ∃ ε', ε' ^ ↑p = NE
Tactic:
exact ⟨_, ha.symm⟩
Proof state after:
no goals
Theorem: Hilbert92ish
Proof state before:
case h.a.h
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i✝ : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι (Fin.last (r + 1))
ha'' : ζ = 1 → i✝ ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε'✝ : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
this : i✝ = Fin.last (r + 1)
h : ℕ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ (h + 1))
hE :
  (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h + 1 - 1) = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
ε' : (𝓞 k)ˣ
hε' : ε' ^ ↑p = NE
hζ'' : IsPrimitiveRoot ((algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ h)) ↑p
NE_p_pow : (algebraMap (𝓞 K) K) ((↑E * (algebraMap (𝓞 k) (𝓞 K)) ↑ε'⁻¹) ^ ↑p) = (algebraMap (𝓞 K) K) 1
i : ℕ
e : (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ h) ^ i = ↑(↑E * (algebraMap (𝓞 k) (𝓞 K)) ↑ε'⁻¹)
⊢ ↑↑(E * ((Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ε')⁻¹) = ↑↑((Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ((ζ ^ ↑p ^ h) ^ i))
Tactic:
simpa using e.symm
Proof state after:
no goals
Theorem: Hilbert92ish
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι (Fin.last (r + 1))
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε'✝ : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
this : i = Fin.last (r + 1)
h : ℕ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ (h + 1))
ε' : (𝓞 k)ˣ
hε' : ε' ^ ↑p = NE
hζ'' : IsPrimitiveRoot ((algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ h)) ↑p
ε'' : (𝓞 k)ˣ
hε'' : E = (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ε''
hE : (algebraMap k K) ((algebraMap (𝓞 k) k) (↑ζ ^ ↑p ^ h)) = (algebraMap k K) ↑↑ε'' / (algebraMap k K) ↑↑ε''
⊢ (algebraMap k K) (↑↑ζ ^ ↑p ^ h) = 1
Tactic:
rwa [div_self (by simp)] at hE
Proof state after:
no goals
Theorem: Hilbert92ish
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 σ
hpodd : ↑p ≠ 2
ζ : (𝓞 k)ˣ
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
NE_p_pow : (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) NE = E ^ ↑p
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι (Fin.last (r + 1))
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
hε'✝ : ∀ (x : Fin (r + 1)), ↑↑p ∣ ι x.castSucc
this : i = Fin.last (r + 1)
h : ℕ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ (h + 1))
ε' : (𝓞 k)ˣ
hε' : ε' ^ ↑p = NE
hζ'' : IsPrimitiveRoot ((algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ ^ ↑p ^ h)) ↑p
ε'' : (𝓞 k)ˣ
hε'' : E = (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ε''
hE : (algebraMap k K) ((algebraMap (𝓞 k) k) (↑ζ ^ ↑p ^ h)) = (algebraMap k K) ↑↑ε'' / (algebraMap k K) ↑↑ε''
⊢ (algebraMap k K) ↑↑ε'' ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Hilbert92ish
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.intro.right.refine_2
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 σ
hpodd : ↑p ≠ 2
h : ℕ
ζ : (𝓞 k)ˣ
hζ : IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h)
hζ' : ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
E : (𝓞 K)ˣ
hE : (algebraMap k K) ((algebraMap (𝓞 k) k) ↑ζ) ^ ↑p ^ (h - 1) = (algebraMap (𝓞 K) K) ↑E / σ ((algebraMap (𝓞 K) K) ↑E)
NE : (𝓞 k)ˣ := (Units.map (RingOfIntegers.norm k)) E
hNE : (algebraMap (𝓞 k) k) ↑NE = (Algebra.norm k) ((algebraMap (𝓞 K) K) ↑E)
S :
  systemOfUnits p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1)
hS :
  systemOfUnits.IsFundamental p
    (Additive (relativeUnitsWithGenerator p hp hKL σ hσ) ⧸
      AddCommGroup.torsion (Additive (relativeUnitsWithGenerator p hp hKL σ hσ)))
    (r + 1) S
H : Fin (r + 1) → Additive (𝓞 K)ˣ := unitlifts p hp hKL σ hσ S
N : Fin (r + 1) → Additive (𝓞 k)ˣ :=
  fun e => Additive.ofMul ((Units.map (RingOfIntegers.norm k)) (Additive.toMul (H e)))
η : Fin (r + 2) → Additive (𝓞 k)ˣ := Fin.snoc N (Additive.ofMul NE)
a : ℤ
ι : Fin (r + 2) → ℤ
i : Fin (r + 2)
ha : ∑ i : Fin (r + 2), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ
ha' : ¬↑↑p ∣ ι i
ha'' : ζ = 1 → i ≠ Fin.last (r + 1)
H2 : Fin (r + 2) → Additive (𝓞 K)ˣ := Fin.snoc H (Additive.ofMul E)
J : (𝓞 K)ˣ := Additive.toMul (∑ i : Fin (r + 2), ι i • H2 i) * (Units.map ↑(algebraMap (𝓞 k) (𝓞 K))) ζ ^ (-a)
ε : (𝓞 K)ˣ
hε : (algebraMap (𝓞 K) K) ↑J = (algebraMap (𝓞 K) K) ↑ε / σ ((algebraMap (𝓞 K) K) ↑ε)
NE_p_pow : mkG E = 0
⊢ ι (Fin.last (r + 1)) • mkG E = 0
Tactic:
rw [NE_p_pow, smul_zero]
Proof state after:
no goals
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ ↔ Submodule.span R s = ⊤
Tactic:
have H : (Submodule.span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
    (Submodule.span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS)) := by
  rw [Submodule.map_span, ← Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective]
  rfl
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ ↔ Submodule.span R s = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ ↔ Submodule.span R s = ⊤
Tactic:
constructor
Proof state after:
case mp
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤ → Submodule.span R s = ⊤

case mpr
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
⊢ Submodule.span R s = ⊤ → Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
Theorem: quotient_span_eq_top_iff_span_eq_top_of_localRing
Proof state before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
⊢ Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
Tactic:
rw [Submodule.map_span, ← Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective]
Proof state after:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
s : Set S
⊢ Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    Submodule.restrictScalars R
      (Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' s))