internlm/Lean-Github huggingface dataset:
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), (σ * l' j - if i = j then σ * l' i else 0) + l' i * l j = 0
⊢ l' = 0
Tactic:
have : l' i = 0 := hl _ (by simpa using hl' i)
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), (σ * l' j - if i = j then σ * l' i else 0) + l' i * l j = 0
this : l' i = 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), (σ * l' j - if i = j then σ * l' i else 0) + l' i * l j = 0
this : l' i = 0
⊢ l' = 0
Tactic:
simp only [this, zero_mul, add_zero, mul_zero, ite_self, sub_zero] at hl'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
this : l' i = 0
hl' : ∀ (j : ι), σ * l' j = 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
this : l' i = 0
hl' : ∀ (j : ι), σ * l' j = 0
⊢ l' = 0
Tactic:
ext j
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
this : l' i = 0
hl' : ∀ (j : ι), σ * l' j = 0
j : ι
⊢ l' j = 0 j
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
this : l' i = 0
hl' : ∀ (j : ι), σ * l' j = 0
j : ι
⊢ l' j = 0 j
Tactic:
exact hσ _ ((mul_comm _ _).trans (hl' j))
Proof state after:
no goals
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : (Finsupp.total ι G R f) ((σ • l' - fun₀ | i => σ * l' i) + l' i • l) = 0
⊢ ∀ (j : ι), σ * l' j - (fun₀ | i => σ * l' i) j + l' i * l j = 0
Tactic:
intro j
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : (Finsupp.total ι G R f) ((σ • l' - fun₀ | i => σ * l' i) + l' i • l) = 0
j : ι
⊢ σ * l' j - (fun₀ | i => σ * l' i) j + l' i * l j = 0
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : (Finsupp.total ι G R f) ((σ • l' - fun₀ | i => σ * l' i) + l' i • l) = 0
j : ι
⊢ σ * l' j - (fun₀ | i => σ * l' i) j + l' i * l j = 0
Tactic:
exact DFunLike.congr_fun (hf _ hl') j
Proof state after:
no goals
Theorem: LinearIndependent.update'
Proof 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)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), (σ * l' j - if i = j then σ * l' i else 0) + l' i * l j = 0
⊢ l' i * l i = 0
Tactic:
simpa using hl' i
Proof state after:
no goals
Theorem: Subgroup.index_mono
Proof 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
Proof 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
Theorem: Subgroup.index_mono
Proof 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
Proof 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
Theorem: Subgroup.index_mono
Proof 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]
Proof 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₁)
Theorem: Subgroup.index_mono
Proof 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
Proof state after:
no goals
Theorem: Subgroup.index_mono
Proof 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
Proof state after:
no goals
Theorem: Subgroup.index_mono
Proof 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]
Proof 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₁)
Theorem: Subgroup.index_mono
Proof 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
Proof state after:
no goals
Theorem: Subgroup.index_mono
Proof 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
Proof 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
Theorem: Subgroup.index_mono
Proof 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]
Proof 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
Theorem: Subgroup.index_mono
Proof 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]
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.existence
Proof 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
Proof 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
Theorem: systemOfUnits.IsFundamental.existence
Proof 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
Proof 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
Theorem: systemOfUnits.IsFundamental.existence
Proof 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⟩
Proof 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