internlm/Lean-Github huggingface dataset:
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
ha' : (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' + S.units i = (1 - zeta ↑p) • g
⊢ False
Tactic:
letI := S'.isMaximal hp hf
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 ⋯
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'
⊢ False
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case this
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'
⊢ Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units)
Tactic:
rw [SetLike.lt_iff_le_and_exists]
Proof state after:
case this
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'
⊢ Submodule.span A (Set.range S.units) ≤ Submodule.span A (Set.range S'.units) ∧
    ∃ x ∈ Submodule.span A (Set.range S'.units), x ∉ Submodule.span A (Set.range S.units)
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
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
Tactic:
exact isEmptyElim i
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
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
Tactic:
ext
Proof state after:
case hS'.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 σ = ⊤
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 ⋯
x✝ : Fin r
⊢ (S'.units ∘ i.succAbove) x✝ = (S.units ∘ i.succAbove) x✝
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case hS'.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 σ = ⊤
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 ⋯
x✝ : Fin r
⊢ (S'.units ∘ i.succAbove) x✝ = (S.units ∘ i.succAbove) x✝
Tactic:
simp only [Function.comp_apply, ne_eq, Fin.succAbove_ne, not_false_eq_true,
Function.update_noteq]
Proof state after:
no goals
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
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
Tactic:
rw [hS', Finsupp.total_comp, LinearMap.comp_apply, Finsupp.lmapDomain_apply,
  ← one_smul A (S.units i), hg, ← ha, ← Finsupp.total_single, ← map_add]
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 + 1)) G A S.units) (Finsupp.mapDomain i.succAbove a' + fun₀ | i => a i) =
    (Finsupp.total (Fin (r + 1)) G A S.units) a
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
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 + 1)) G A S.units) (Finsupp.mapDomain i.succAbove a' + fun₀ | i => a i) =
    (Finsupp.total (Fin (r + 1)) G A S.units) a
Tactic:
congr 1
Proof state after:
case ha'.h.e_6.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 σ = ⊤
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.mapDomain i.succAbove a' + fun₀ | i => a i) = a
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case ha'.h.e_6.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 σ = ⊤
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.mapDomain i.succAbove a' + fun₀ | i => a i) = a
Tactic:
ext j
Proof state after:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
⊢ (Finsupp.mapDomain i.succAbove a' + fun₀ | i => a i) j = a j
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
⊢ (Finsupp.mapDomain i.succAbove a' + fun₀ | i => a i) j = a j
Tactic:
rw [Finsupp.coe_add, Pi.add_apply, Finsupp.single_apply]
Proof state after:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
⊢ ((Finsupp.mapDomain i.succAbove a') j + if i = j then a i else 0) = a j
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
⊢ ((Finsupp.mapDomain i.succAbove a') j + if i = j then a i else 0) = a j
Tactic:
have : i = j ↔ j ∉ Set.range (Fin.succAbove i) := by simp [@eq_comm _ i]
Proof state after:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
this : i = j ↔ j ∉ Set.range i.succAbove
⊢ ((Finsupp.mapDomain i.succAbove a') j + if i = j then a i else 0) = a j
Theorem: systemOfUnits.IsFundamental.lemma2
Proof state before:
case ha'.h.e_6.h.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 σ = ⊤
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
j : Fin (r + 1)
this : i = j ↔ j ∉ Set.range i.succAbove
⊢ ((Finsupp.mapDomain i.succAbove a') j + if i = j then a i else 0) = a j
Tactic:
split_ifs with hij
Proof state after:
case pos
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
j : Fin (r + 1)
this : i = j ↔ j ∉ Set.range i.succAbove
hij : i = j
⊢ (Finsupp.mapDomain i.succAbove a') j + a i = a j

case neg
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
j : Fin (r + 1)
this : i = j ↔ j ∉ Set.range i.succAbove
hij : ¬i = j
⊢ (Finsupp.mapDomain i.succAbove a') j + 0 = a j
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 σ = ⊤
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
j : Fin (r + 1)
⊢ i = j ↔ j ∉ Set.range i.succAbove
Tactic:
simp [@eq_comm _ i]
Proof state after:
no goals