Theorem: systemOfUnits.IsFundamental.maximal' (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 : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index
Tactic:
letI := hs.choose
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✝¹ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
this : S.IsMaximal := Exists.choose hs
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index

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 : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
this : S.IsMaximal := Exists.choose hs
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index
Tactic:
convert hs.choose_spec a ‹_› <;> symm <;> exact Nat.card_eq_fintype_card.symm
State after:
no goals