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) ∧
    ∃ x ∈ Submodule.span A (Set.range S'.units), x ∉ Submodule.span A (Set.range S.units)
Tactic:
constructor
Proof state after:
case this.left
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)

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)