Theorem: systemOfUnits.IsFundamental.existence (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✝ : Module A G
⊢ ∃ S, IsFundamental p G r S
Tactic:
obtain ⟨S⟩ := systemOfUnits.existence p hp G r hf
State after:
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✝ : Module A G
S : systemOfUnits p G r
⊢ ∃ S, IsFundamental p G r S

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✝ : Module A G
S : systemOfUnits p G r
⊢ ∃ S, IsFundamental p G r S
Tactic:
letI := S.isMaximal hp hf
State after:
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✝ : Module A G
S : systemOfUnits p G r
this : S.IsMaximal := isMaximal p hp G hf S
⊢ ∃ S, IsFundamental p G r S

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✝ : Module A G
S : systemOfUnits p G r
this : S.IsMaximal := isMaximal p hp G hf S
⊢ ∃ S, IsFundamental p G r S
Tactic:
have : { a | ∃ (S : systemOfUnits p G r) (_ : S.IsMaximal), a = S.index p G r }.Nonempty :=
  ⟨S.index, S, S.isMaximal hp hf, rfl⟩
State after:
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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
⊢ ∃ S, IsFundamental p G r S

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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
⊢ ∃ S, IsFundamental p G r S
Tactic:
obtain ⟨S', hS', ha⟩ := Nat.sInf_mem this
State after:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∃ S, IsFundamental p G r S

State before:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∃ S, IsFundamental p G r S
Tactic:
use S', hS'
State after:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∀ (s : systemOfUnits p G r) (x : s.IsMaximal), index p G r S' ≤ index p G r s

State before:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∀ (s : systemOfUnits p G r) (x : s.IsMaximal), index p G r S' ≤ index p G r s
Tactic:
intro a' ha'
State after:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ index p G r S' ≤ index p G r a'

State before:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ index p G r S' ≤ index p G r a'
Tactic:
rw [← ha]
State after:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ sInf {a | ∃ S x, a = index p G r S} ≤ index p G r a'

State before:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ sInf {a | ∃ S x, a = index p G r S} ≤ index p G r a'
Tactic:
apply csInf_le (OrderBot.bddBelow _)
State after:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ index p G r a' ∈ {a | ∃ S x, a = index p G r S}

State before:
case 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✝ : Module A G
S : systemOfUnits p G r
this✝ : S.IsMaximal := isMaximal p hp G hf S
this : {a | ∃ S x, a = index p G r S}.Nonempty
S' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
a' : systemOfUnits p G r
ha' : a'.IsMaximal
⊢ index p G r a' ∈ {a | ∃ S x, a = index p G r S}
Tactic:
use a', ha'
State after:
no goals