have := fintypeOfIndexNeZero hn
case inr.a
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σ : zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G✝
inst✝² : Module.Free ℤ G✝
inst✝¹ : Module.Finite ℤ G✝
hf : finrank ℤ G✝ = r * (↑p - 1)
G : Type u_5
inst✝ : Group G
H₁ H₂ : Subgroup G
h : H₁ < H₂
h₁ : Fintype (G ⧸ H₁)
hn : H₂.index ≠ 0
⊢ H₂.index ≠ H₁.index
case inr.a
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σ : zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G✝
inst✝² : Module.Free ℤ G✝
inst✝¹ : Module.Finite ℤ G✝
hf : finrank ℤ G✝ = r * (↑p - 1)
G : Type u_5
inst✝ : Group G
H₁ H₂ : Subgroup G
h : H₁ < H₂
h₁ : Fintype (G ⧸ H₁)
hn : H₂.index ≠ 0
this : Fintype (G ⧸ H₂)
⊢ H₂.index ≠ H₁.index