internlm/Lean-Github huggingface dataset:
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right
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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ ∃ x ∈ Submodule.span A (Set.range S'.units), x ∉ Submodule.span A (Set.range S.units)
Tactic:
refine ⟨g, Submodule.subset_span ⟨i, Function.update_same _ _ _⟩, ?_⟩
Proof state after:
case this.right
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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ g ∉ Submodule.span A (Set.range S.units)
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right
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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ g ∉ Submodule.span A (Set.range S.units)
Tactic:
rw [← Finsupp.range_total]
Proof state after:
case this.right
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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ g ∉ LinearMap.range (Finsupp.total (Fin (r + 1)) G A S.units)
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right
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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ g ∉ LinearMap.range (Finsupp.total (Fin (r + 1)) G A S.units)
Tactic:
rintro ⟨l, rfl⟩
Proof state after:
case this.right.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 σ = ⊤
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
this✝ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ False
Tactic:
letI := (Algebra.id A).toModule
Proof state after:
case this.right.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 σ = ⊤
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
this✝¹ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝ : S'.IsMaximal := isMaximal p hp G hf S'
this : Module A A := Algebra.toModule
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝¹ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝ : S'.IsMaximal := isMaximal p hp G hf S'
this : Module A A := Algebra.toModule
⊢ False
Tactic:
letI : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
Proof state after:
case this.right.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 σ = ⊤
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
this✝² : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝¹ : S'.IsMaximal := isMaximal p hp G hf S'
this✝ : Module A A := Algebra.toModule
this : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝² : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝¹ : S'.IsMaximal := isMaximal p hp G hf S'
this✝ : Module A A := Algebra.toModule
this : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
⊢ False
Tactic:
letI : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
Proof state after:
case this.right.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 σ = ⊤
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
this✝³ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝² : S'.IsMaximal := isMaximal p hp G hf S'
this✝¹ : Module A A := Algebra.toModule
this✝ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝³ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝² : S'.IsMaximal := isMaximal p hp G hf S'
this✝¹ : Module A A := Algebra.toModule
this✝ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
⊢ False
Tactic:
rw [← LinearMap.map_smul, ← sub_eq_zero,
  ← (Finsupp.total (Fin _) G A S.units).map_sub] at hg
Proof state after:
case this.right.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 σ = ⊤
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
this✝³ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝² : S'.IsMaximal := isMaximal p hp G hf S'
this✝¹ : Module A A := Algebra.toModule
this✝ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝³ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝² : S'.IsMaximal := isMaximal p hp G hf S'
this✝¹ : Module A A := Algebra.toModule
this✝ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
⊢ False
Tactic:
have := DFunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i
Proof state after:
case this.right.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 σ = ⊤
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
this✝⁴ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝³ : S'.IsMaximal := isMaximal p hp G hf S'
this✝² : Module A A := Algebra.toModule
this✝¹ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this✝ : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
this : ((1 - zeta ↑p) • l - a) i = 0 i
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this.right.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 σ = ⊤
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
this✝⁴ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝³ : S'.IsMaximal := isMaximal p hp G hf S'
this✝² : Module A A := Algebra.toModule
this✝¹ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this✝ : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
this : ((1 - zeta ↑p) • l - a) i = 0 i
⊢ False
Tactic:
simp only [algebraMap_int_eq, Int.coe_castRingHom, Finsupp.coe_sub, Finsupp.coe_smul, ha,
  Pi.sub_apply, Finsupp.mapRange_apply, Finsupp.coe_zero, Pi.zero_apply, sub_eq_zero] at this
Proof state after:
case this.right.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 σ = ⊤
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
this✝⁴ : Fact (↑p).Prime := { out := hp }
a' : Fin r →₀ A := Finsupp.comapDomain i.succAbove a ⋯
l : Fin (r + 1) →₀ A
hg✝ : (1 - zeta ↑p) • (Finsupp.total (Fin (r + 1)) G A S.units) l = (Finsupp.total (Fin (r + 1)) G A S.units) a
hg : (Finsupp.total (Fin (r + 1)) G A S.units) ((1 - zeta ↑p) • l - a) = 0
S' : systemOfUnits p G (r + 1) :=
  { units := Function.update S.units i ((Finsupp.total (Fin (r + 1)) G A S.units) l), linearIndependent := ⋯ }
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) • (Finsupp.total (Fin (r + 1)) G A S.units) l
this✝³ : S'.IsMaximal := isMaximal p hp G hf S'
this✝² : Module A A := Algebra.toModule
this✝¹ : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
this✝ : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
this : ((1 - zeta ↑p) • ⇑l) i = 1
⊢ False