Theorem: h_exists' (FltRegular/NumberTheory/Hilbert92.lean)

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 σ
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
let H := Subgroup.toAddSubgroup.symm
  (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) (Submonoid.powers (p : ℕ))).toAddSubgroup
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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε

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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
have : H ≤ NumberField.Units.torsion k
State after:
case this
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 : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ H ≤ Units.torsion k

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 : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε

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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
obtain ⟨ζ, hζ⟩ := Subgroup.isCyclic_of_le this
State after:
case mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε

State before:
case mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
obtain ⟨⟨_, i, rfl⟩, hiζ : (ζ : (𝓞 k)ˣ) ^ (p ^ i : ℕ) = 1⟩ := ζ.prop
State after:
case mk.intro.intro.mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε

State before:
case mk.intro.intro.mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
obtain ⟨j, _, hj'⟩ := (Nat.dvd_prime_pow hp).mp (orderOf_dvd_of_pow_eq_one hiζ)
State after:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε

State before:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
⊢ ∃ h ζ, IsPrimitiveRoot ((algebraMap (𝓞 k) k) ↑ζ) (↑p ^ h) ∧ ∀ (ε : (𝓞 k)ˣ) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
Tactic:
refine ⟨j, ζ, IsPrimitiveRoot.coe_coe_iff.mpr (hj' ▸ IsPrimitiveRoot.orderOf ζ.1),
  fun ε n hn ↦ ?_⟩
State after:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
⊢ ∃ i, ↑ζ ^ i = ε

State before:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
⊢ ∃ i, ↑ζ ^ i = ε
Tactic:
have : Fintype H := Set.fintypeSubset (NumberField.Units.torsion k) (by exact this)
State after:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this : Fintype ↥H
⊢ ∃ i, ↑ζ ^ i = ε

State before:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this : Fintype ↥H
⊢ ∃ i, ↑ζ ^ i = ε
Tactic:
have := Finite.of_fintype H
State after:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝¹ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this✝ : Fintype ↥H
this : Finite ↥H
⊢ ∃ i, ↑ζ ^ i = ε

State before:
case mk.intro.intro.mk.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝¹ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this✝ : Fintype ↥H
this : Finite ↥H
⊢ ∃ i, ↑ζ ^ i = ε
Tactic:
obtain ⟨i, hi⟩ := mem_powers_iff_mem_zpowers.mpr (hζ ⟨ε, ⟨_, n, rfl⟩, hn⟩)
State after:
case mk.intro.intro.mk.intro.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝¹ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i✝ : ℕ
hiζ : ↑ζ ^ ↑p ^ i✝ = 1
j : ℕ
left✝ : j ≤ i✝
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this✝ : Fintype ↥H
this : Finite ↥H
i : ℕ
hi : (fun x => ζ ^ x) i = ⟨ε, ⋯⟩
⊢ ∃ i, ↑ζ ^ i = ε

State before:
case mk.intro.intro.mk.intro.intro.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this✝¹ : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i✝ : ℕ
hiζ : ↑ζ ^ ↑p ^ i✝ = 1
j : ℕ
left✝ : j ≤ i✝
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
this✝ : Fintype ↥H
this : Finite ↥H
i : ℕ
hi : (fun x => ζ ^ x) i = ⟨ε, ⋯⟩
⊢ ∃ i, ↑ζ ^ i = ε
Tactic:
exact ⟨i, congr_arg Subtype.val hi⟩
State after:
no goals

State before:
case this
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 : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
⊢ H ≤ Units.torsion k
Tactic:
rintro x ⟨⟨_, i, rfl⟩, hnx : x ^ (p ^ i : ℕ) = 1⟩
State after:
case this.intro.mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
x : (𝓞 k)ˣ
i : ℕ
hnx : x ^ ↑p ^ i = 1
⊢ x ∈ Units.torsion k

State before:
case this.intro.mk.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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
x : (𝓞 k)ˣ
i : ℕ
hnx : x ^ ↑p ^ i = 1
⊢ x ∈ Units.torsion k
Tactic:
exact isOfFinOrder_iff_pow_eq_one.mpr ⟨p ^ i, Fin.size_pos', hnx⟩
State after:
no goals

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 σ
H : Subgroup (𝓞 k)ˣ :=
  Subgroup.toAddSubgroup.symm (Submodule.torsion' ℤ (Additive (𝓞 k)ˣ) ↥(Submonoid.powers ↑p)).toAddSubgroup
this : H ≤ Units.torsion k
ζ : ↥H
hζ : ∀ (x : ↥H), x ∈ Subgroup.zpowers ζ
i : ℕ
hiζ : ↑ζ ^ ↑p ^ i = 1
j : ℕ
left✝ : j ≤ i
hj' : orderOf ↑ζ = ↑p ^ j
ε : (𝓞 k)ˣ
n : ℕ
hn : ε ^ ↑p ^ n = 1
⊢ ↑H ⊆ ↑(Units.torsion k)
Tactic:
exact this
State after:
no goals