Theorem: systemOfUnits.IsFundamental.lemma2 (FltRegular/NumberTheory/Hilbert92.lean)

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
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

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
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

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
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

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⟩
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

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
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

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
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

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
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

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
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

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
this : S'.IsMaximal := isMaximal p hp G hf S'
⊢ False
Tactic:
suffices : Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units)
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'
this : Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units)
⊢ False

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)

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]
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)

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
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)

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
State after:
no goals

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
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✝

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]
State after:
no goals

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]
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

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
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

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
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

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]
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

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]
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

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
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

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]
State after:
no goals

State before:
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
Tactic:
rw [Finsupp.mapDomain_notin_range, zero_add, hij]
State after:
case pos.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
hij : i = j
⊢ j ∉ Set.range i.succAbove

State before:
case pos.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
hij : i = j
⊢ j ∉ Set.range i.succAbove
Tactic:
rwa [← this]
State after:
no goals

State before:
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
Tactic:
obtain ⟨j, rfl⟩ := not_imp_comm.mp this.mpr hij
State after:
case neg.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
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
this : i = i.succAbove j ↔ i.succAbove j ∉ Set.range i.succAbove
hij : ¬i = i.succAbove j
⊢ (Finsupp.mapDomain i.succAbove a') (i.succAbove j) + 0 = a (i.succAbove j)

State before:
case neg.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
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
this : i = i.succAbove j ↔ i.succAbove j ∉ Set.range i.succAbove
hij : ¬i = i.succAbove j
⊢ (Finsupp.mapDomain i.succAbove a') (i.succAbove j) + 0 = a (i.succAbove j)
Tactic:
rw [Finsupp.mapDomain_apply Fin.succAbove_right_injective, add_zero,
  Finsupp.comapDomain_apply]
State after:
no goals

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
this✝ : S'.IsMaximal := isMaximal p hp G hf S'
this : Submodule.span A (Set.range S.units) < Submodule.span A (Set.range S'.units)
⊢ False
Tactic:
exact (hs.maximal' S').not_lt (AddSubgroup.index_mono (h₁ := S.isMaximal hp hf) this)
State after:
no goals

State before:
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)
Tactic:
rw [Submodule.span_le]
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'
⊢ Set.range S.units ⊆ ↑(Submodule.span A (Set.range S'.units))

State before:
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'
⊢ Set.range S.units ⊆ ↑(Submodule.span A (Set.range S'.units))
Tactic:
rintro _ ⟨j, rfl⟩
State after:
case this.left.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
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'
j : Fin (r + 1)
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))

State before:
case this.left.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
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'
j : Fin (r + 1)
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))
Tactic:
by_cases hij : i = j
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
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'
j : Fin (r + 1)
hij : i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))

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
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'
j : Fin (r + 1)
hij : ¬i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))

State before:
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
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'
j : Fin (r + 1)
hij : i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))
Tactic:
rw [add_comm, ← eq_sub_iff_add_eq] at ha'
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
ha' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))

State before:
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
ha' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))
Tactic:
rw [← hij, ha']
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
ha' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' ∈ ↑(Submodule.span A (Set.range S'.units))

State before:
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
ha' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' ∈ ↑(Submodule.span A (Set.range S'.units))
Tactic:
apply sub_mem
State after:
case pos.hx
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (1 - zeta ↑p) • g ∈ Submodule.span A (Set.range S'.units)

case pos.hy
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' ∈ Submodule.span A (Set.range S'.units)

State before:
case pos.hx
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (1 - zeta ↑p) • g ∈ Submodule.span A (Set.range S'.units)
Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, Function.update_same _ _ _⟩)
State after:
no goals

State before:
case pos.hy
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a' ∈ Submodule.span A (Set.range S'.units)
Tactic:
rw [← Finsupp.range_total, Finsupp.total_comp, LinearMap.comp_apply]
State after:
case pos.hy
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (Finsupp.total (Fin (r + 1)) G A S'.units) ((Finsupp.lmapDomain A A i.succAbove) a') ∈
    LinearMap.range (Finsupp.total (Fin (r + 1)) G A S'.units)

State before:
case pos.hy
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' : S.units i = (1 - zeta ↑p) • g - (Finsupp.total (Fin r) G A (S'.units ∘ i.succAbove)) a'
this : S'.IsMaximal := isMaximal p hp G hf S'
j : Fin (r + 1)
hij : i = j
⊢ (Finsupp.total (Fin (r + 1)) G A S'.units) ((Finsupp.lmapDomain A A i.succAbove) a') ∈
    LinearMap.range (Finsupp.total (Fin (r + 1)) G A S'.units)
Tactic:
exact ⟨_, rfl⟩
State after:
no goals

State before:
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
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'
j : Fin (r + 1)
hij : ¬i = j
⊢ S.units j ∈ ↑(Submodule.span A (Set.range S'.units))
Tactic:
exact Submodule.subset_span ⟨j, Function.update_noteq (Ne.symm hij) _ _⟩
State after:
no goals

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 _ _ _⟩, ?_⟩
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)

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]
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)

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⟩
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

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
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

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
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

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
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

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
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

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
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

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
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

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) i = 1
⊢ False
Tactic:
exact CyclotomicIntegers.not_isUnit_one_sub_zeta p
  (isUnit_of_mul_eq_one _ _ this)
State after:
no goals