exact CyclotomicIntegers.not_isUnit_one_sub_zeta p
  (isUnit_of_mul_eq_one _ _ this)
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
no goals