internlm/Lean-Github huggingface dataset:
Theorem: LinearIndependent.update
Proof 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
Proof 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
Theorem: LinearIndependent.update
Proof 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]
Proof 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
Theorem: LinearIndependent.update
Proof 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]
Proof 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
Theorem: LinearIndependent.update
Proof 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 [*]
Proof state after:
no goals
Theorem: LinearIndependent.update
Proof 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
Proof state after:
no goals
Theorem: LinearIndependent.update
Proof 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
Proof state after:
no goals
Theorem: LinearIndependent.update
Proof 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
Proof state after:
no goals
Theorem: LinearIndependent.update
Proof 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)
Proof state after:
no goals
Theorem: Finsupp.total_pi_single
Proof 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
M : Type u_6
R : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
i : α
m : M
f : α →₀ R
⊢ (Finsupp.total α M R (Pi.single i m)) f = f i • m
Tactic:
simp only [Finsupp.total, ne_eq, Pi.single_apply, coe_lsum, LinearMap.coe_smulRight,
  LinearMap.id_coe, id_eq, smul_ite, smul_zero, sum_ite_eq', mem_support_iff, ite_eq_left_iff,
  not_not]
Proof 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
M : Type u_6
R : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
i : α
m : M
f : α →₀ R
⊢ f i = 0 → 0 = f i • m
Theorem: Finsupp.total_pi_single
Proof 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
M : Type u_6
R : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq α
i : α
m : M
f : α →₀ R
⊢ f i = 0 → 0 = f i • m
Tactic:
exact fun e ↦ e ▸ (zero_smul R m).symm
Proof state after:
no goals
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : LinearIndependent R f
⊢ LinearIndependent R (Function.update f i g)
Tactic:
rw [linearIndependent_iff] at hf ⊢
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
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
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
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'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
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
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
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:
rw [Pi.update_eq_sub_add_single, ← Finsupp.ltotal_apply, map_add, map_sub] at hl'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' :
  σ •
      ((Finsupp.ltotal ι G R) f - (Finsupp.ltotal ι G R) (Pi.single i (f i)) + (Finsupp.ltotal ι G R) (Pi.single i g))
        l' =
    σ • 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' :
  σ •
      ((Finsupp.ltotal ι G R) f - (Finsupp.ltotal ι G R) (Pi.single i (f i)) + (Finsupp.ltotal ι G R) (Pi.single i g))
        l' =
    σ • 0
⊢ l' = 0
Tactic:
simp only [Finsupp.ltotal_apply, LinearMap.add_apply, LinearMap.sub_apply,
  Finsupp.total_pi_single, smul_add, smul_sub, smul_zero] at hl'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : σ • (Finsupp.total ι G R f) l' - σ • l' i • f i + σ • l' i • g = 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : σ • (Finsupp.total ι G R f) l' - σ • l' i • f i + σ • l' i • g = 0
⊢ l' = 0
Tactic:
rw [smul_comm σ (l' i) g, hg, ← LinearMap.map_smul, ← LinearMap.map_smul, smul_smul,
  ← Finsupp.total_single, ← (Finsupp.total ι G R f).map_sub, ← map_add] at hl'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : (Finsupp.total ι G R f) ((σ • l' - fun₀ | i => σ * l' i) + l' i • l) = 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : (Finsupp.total ι G R f) ((σ • l' - fun₀ | i => σ * l' i) + l' i • l) = 0
⊢ l' = 0
Tactic:
replace hl' : ∀ j, (σ * l' j - (fun₀ | i => σ * l' i) j) + l' i * l j = 0 := by
  intro j
  exact DFunLike.congr_fun (hf _ hl') j
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), σ * l' j - (fun₀ | i => σ * l' i) j + l' i * l j = 0
⊢ l' = 0
Theorem: LinearIndependent.update'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), σ * l' j - (fun₀ | i => σ * l' i) j + l' i * l j = 0
⊢ l' = 0
Tactic:
simp only [Finsupp.single_apply] at hl'
Proof 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
l : ι →₀ R
i : ι
g : G
σ : R
hσ : σ ∈ R⁰
hg : σ • g = (Finsupp.total ι G R f) l
hl : l i ∈ R⁰
hf : ∀ (l : ι →₀ R), (Finsupp.total ι G R f) l = 0 → l = 0
l' : ι →₀ R
hl' : ∀ (j : ι), (σ * l' j - if i = j then σ * l' i else 0) + l' i * l j = 0
⊢ l' = 0