split <;> simp [*]
case this.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 σ✝ = ⊤
r : ℕ
inst✝⁵ : DistribMulAction H G
inst✝⁴ : Module.Free ℤ G
inst✝³ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r * (↑p - 1)
ι : Type u_5
inst✝² : DecidableEq ι
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R G
f : ι → G
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = f i
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l : ι →₀ R
hl : (Finsupp.total ι G R (Function.update f i g)) l = 0
x : ι
⊢ (if x = i then l i • f x else σ • l x • f x) = if x = i then l x • f i else σ • l x • f x
no goals