rw [← ha]
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'
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'