Theorem: Subgroup.index_mono (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σ : 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₁)
⊢ H₂.index < H₁.index
Tactic:
rcases eq_or_ne H₂.index 0 with hn | hn
State after:
case inl
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
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

State before:
case inr
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
Tactic:
apply lt_of_le_of_ne
State after:
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
⊢ H₂.index ≠ H₁.index

State before:
case inl
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
Tactic:
rw [hn, index_eq_card]
State after:
case inl
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
⊢ 0 < Fintype.card (G ⧸ H₁)

State before:
case inl
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
⊢ 0 < Fintype.card (G ⧸ H₁)
Tactic:
exact Fintype.card_pos
State after:
no goals

State before:
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
Tactic:
refine Nat.le_of_dvd (by rw [index_eq_card]; apply Fintype.card_pos) <| Subgroup.index_dvd_of_le h.le
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σ : 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
⊢ 0 < H₁.index
Tactic:
rw [index_eq_card]
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σ : 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
⊢ 0 < Fintype.card (G ⧸ H₁)

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σ : 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
⊢ 0 < Fintype.card (G ⧸ H₁)
Tactic:
apply Fintype.card_pos
State after:
no goals

State before:
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
Tactic:
have := fintypeOfIndexNeZero hn
State after:
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

State before:
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
Tactic:
rw [←mul_one H₂.index, ←relindex_mul_index h.le, mul_comm, Ne, eq_comm]
State after:
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₁.relindex H₂ * H₂.index = 1 * H₂.index

State before:
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₁.relindex H₂ * H₂.index = 1 * H₂.index
Tactic:
simp [-one_mul, -Nat.one_mul, hn, h.not_le]
State after:
no goals