apply lemma2 p hp G r hf S hs i b hb (x • ∑ i, S.units i + y • g)
case intro.intro.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 σ = ⊤
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
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ False
case intro.intro.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 σ = ⊤
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
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (1 - zeta ↑p) • (x • ∑ i : Fin r, S.units i + y • g) = (Finsupp.total (Fin r) G A S.units) b