Theorem: LinearIndependent.update (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)
ι : 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 : LinearIndependent R f
⊢ LinearIndependent R (Function.update f i g)
Tactic:
rw [linearIndependent_iff] at hf ⊢
State after:
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), (Finsupp.total ι G R (Function.update f i g)) l = 0 → l = 0

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)
ι : 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), (Finsupp.total ι G R (Function.update f i g)) l = 0 → l = 0
Tactic:
intros l hl
State after:
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
⊢ l = 0

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)
ι : 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
⊢ l = 0
Tactic:
have : (Finsupp.total ι G R f) (Finsupp.update (σ • l) i (l i)) = 0
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 σ✝ = ⊤
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
⊢ (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0

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
this : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
⊢ l = 0

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)
ι : 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
this : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
⊢ l = 0
Tactic:
ext j
State after:
case 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
this : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
⊢ l j = 0 j

State before:
case 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
this : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
⊢ l j = 0 j
Tactic:
have := DFunLike.congr_fun (hf (Finsupp.update (σ • l) i (l i)) this) j
State after:
case 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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
this : ((σ • l).update i (l i)) j = 0 j
⊢ l j = 0 j

State before:
case 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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
this : ((σ • l).update i (l i)) j = 0 j
⊢ l j = 0 j
Tactic:
simp only [Finsupp.coe_update, Finsupp.coe_smul, ne_eq, Function.update_apply, Finsupp.coe_zero,
  Pi.zero_apply] at this
State after:
case 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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
this : (if j = i then l i else (σ • ⇑l) j) = 0
⊢ l j = 0 j

State before:
case 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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
this : (if j = i then l i else (σ • ⇑l) j) = 0
⊢ l j = 0 j
Tactic:
split_ifs at this 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 σ✝ = ⊤
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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
hij : j = i
this : l i = 0
⊢ l j = 0 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 σ✝ = ⊤
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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
hij : ¬j = i
this : (σ • ⇑l) j = 0
⊢ l j = 0 j

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 σ✝ = ⊤
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
⊢ (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
Tactic:
rw [← smul_zero σ, ← hl, Finsupp.total_apply, Finsupp.total_apply, Finsupp.smul_sum]
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 σ✝ = ⊤
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
⊢ (((σ • l).update i (l i)).sum fun i a => a • f i) = l.sum fun a b => σ • b • Function.update f i g a

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 σ✝ = ⊤
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
⊢ (((σ • l).update i (l i)).sum fun i a => a • f i) = l.sum fun a b => σ • b • Function.update f i g a
Tactic:
apply Finsupp.sum_congr'
State after:
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 : ι), ((σ • l).update i (l i)) x • f x = σ • l x • Function.update f i g x

case this.hg1
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
⊢ ∀ (i : ι), 0 • f i = 0

case this.hg2
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
⊢ ∀ (i_1 : ι), σ • 0 • Function.update f i g i_1 = 0

State before:
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 : ι), ((σ • l).update i (l i)) x • f x = σ • l x • Function.update f i g x
Tactic:
intro x
State after:
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 : ι
⊢ ((σ • l).update i (l i)) x • f x = σ • l x • Function.update f i g x

State before:
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 : ι
⊢ ((σ • l).update i (l i)) x • f x = σ • l x • Function.update f i g x
Tactic:
simp only [Finsupp.coe_update, Finsupp.coe_smul, Function.update_apply, ite_smul, smul_ite]
State after:
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 • g else σ • l x • f x

State before:
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 • g else σ • l x • f x
Tactic:
rw [smul_smul, mul_comm σ, ← smul_smul, hg, Pi.smul_apply, smul_eq_mul, ← smul_smul]
State after:
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

State before:
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
Tactic:
split <;> simp [*]
State after:
no goals

State before:
case this.hg1
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
⊢ ∀ (i : ι), 0 • f i = 0
Tactic:
simp
State after:
no goals

State before:
case this.hg2
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
⊢ ∀ (i_1 : ι), σ • 0 • Function.update f i g i_1 = 0
Tactic:
simp
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 σ✝ = ⊤
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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
hij : j = i
this : l i = 0
⊢ l j = 0 j
Tactic:
exact hij ▸ 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 σ✝ = ⊤
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
this✝ : (Finsupp.total ι G R f) ((σ • l).update i (l i)) = 0
j : ι
hij : ¬j = i
this : (σ • ⇑l) j = 0
⊢ l j = 0 j
Tactic:
exact hσ (l j) ((mul_comm _ _).trans this)
State after:
no goals