internlm/Lean-Github huggingface dataset:
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
this : {a | ∃ S x, a = index p G r S}.Nonempty
⊢ ∃ S, IsFundamental p G r S
Tactic:
obtain ⟨S', hS', ha⟩ := Nat.sInf_mem this
Proof state after:
case intro.intro.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' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∃ S, IsFundamental p G r S
Theorem: systemOfUnits.IsFundamental.existence
Proof state before:
case intro.intro.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' : systemOfUnits p G r
hS' : S'.IsMaximal
ha : sInf {a | ∃ S x, a = index p G r S} = index p G r S'
⊢ ∃ S, IsFundamental p G r S
Tactic:
use S', hS'
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)
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'
⊢ ∀ (s : systemOfUnits p G r) (x : s.IsMaximal), index p G r S' ≤ index p G r s
Theorem: systemOfUnits.IsFundamental.existence
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)
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'
⊢ ∀ (s : systemOfUnits p G r) (x : s.IsMaximal), index p G r S' ≤ index p G r s
Tactic:
intro a' ha'
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)
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'
Theorem: systemOfUnits.IsFundamental.existence
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)
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'
Tactic:
rw [← ha]
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)
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'
Theorem: systemOfUnits.IsFundamental.existence
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)
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'
Tactic:
apply csInf_le (OrderBot.bddBelow _)
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)
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 a' ∈ {a | ∃ S x, a = index p G r S}
Theorem: systemOfUnits.IsFundamental.existence
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)
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 a' ∈ {a | ∃ S x, a = index p G r S}
Tactic:
use a', ha'
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.lemma2
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 : systemOfUnits p G r
hs : IsFundamental p G r S
i : Fin r
a : Fin r →₀ A
ha : a i = 1
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ (Finsupp.total (Fin r) G A S.units) a
Tactic:
cases' r with r
Proof state after:
case zero
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
hf : finrank ℤ G = 0 * (↑p - 1)
S : systemOfUnits p G 0
hs : IsFundamental p G 0 S
i : Fin 0
a : Fin 0 →₀ A
ha : a i = 1
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ (Finsupp.total (Fin 0) G A S.units) a

case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ (Finsupp.total (Fin (r + 1)) G A S.units) a
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ (Finsupp.total (Fin (r + 1)) G A S.units) a
Tactic:
intro g hg
Proof state after:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
⊢ False
Tactic:
letI := Fact.mk hp
Proof state after:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
⊢ False
Tactic:
let S' : systemOfUnits p G (r + 1) := ⟨Function.update S.units i g,
  LinearIndependent.update' _ _ _ _ _ _ (CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors p)
  hg (ha ▸ one_mem A⁰) S.linearIndependent⟩
Proof state after:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
⊢ False
Tactic:
let a' := a.comapDomain (Fin.succAbove i) Fin.succAbove_right_injective.injOn
Proof state after:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
⊢ False
Tactic:
have hS' : S'.units ∘ Fin.succAbove i = S.units ∘ Fin.succAbove i
Proof state after:
case hS'
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
⊢ S'.units ∘ i.succAbove = S.units ∘ i.succAbove

case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
hS' : S'.units ∘ i.succAbove = S.units ∘ i.succAbove
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
hS' : S'.units ∘ i.succAbove = S.units ∘ i.succAbove
⊢ False
Tactic:
have ha' : Finsupp.total _ G A (S'.units ∘ Fin.succAbove i) a' + S.units i = (1 - zeta p) • g
Proof state after:
case ha'
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
hS' : S'.units ∘ i.succAbove = S.units ∘ i.succAbove
⊢ (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' + S.units i = (1 - zeta ↑p) • g

case succ
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 σ = ⊤
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
inst✝ : Module A G
r : ℕ
hf : finrank ℤ G = (r + 1) * (↑p - 1)
S : systemOfUnits p G (r + 1)
hs : IsFundamental p G (r + 1) S
i : Fin (r + 1)
a : Fin (r + 1) →₀ A
ha : a i = 1
g : G
hg : (1 - zeta ↑p) • g = (Finsupp.total (Fin (r + 1)) G A S.units) a
this : Fact (↑p).Prime := { out := hp }
S' : systemOfUnits p G (r + 1) := { units := Function.update S.units i g, linearIndependent := ⋯ }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
hS' : S'.units ∘ i.succAbove = S.units ∘ i.succAbove
ha' : (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' + S.units i = (1 - zeta ↑p) • g
⊢ False