internlm/Lean-Github huggingface dataset:
Theorem: systemOfUnits.IsFundamental.maximal'
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)
inst✝¹ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index
Tactic:
letI := hs.choose
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)
inst✝¹ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
this : S.IsMaximal := Exists.choose hs
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index
Theorem: systemOfUnits.IsFundamental.maximal'
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)
inst✝¹ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : systemOfUnits p G r
inst✝ : a.IsMaximal
this : S.IsMaximal := Exists.choose hs
⊢ (Submodule.span A (Set.range S.units)).toAddSubgroup.index ≤
    (Submodule.span A (Set.range a.units)).toAddSubgroup.index
Tactic:
convert hs.choose_spec a ‹_› <;> symm <;> exact Nat.card_eq_fintype_card.symm
Proof state after:
no goals
Theorem: Finsupp.prod_congr'
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
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ f₁.prod g1 = f₂.prod g2
Tactic:
classical
rw [f₁.prod_of_support_subset Finset.subset_union_left _ (fun i _ ↦ hg1 i),
  f₂.prod_of_support_subset Finset.subset_union_right _ (fun i _ ↦ hg2 i)]
exact Finset.prod_congr rfl (fun x _ ↦ h x)
Proof state after:
no goals
Theorem: Finsupp.prod_congr'
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
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ ∏ x ∈ f₁.support ∪ ?m.76044, g1 x (f₁ x) = ∏ x ∈ ?m.76647 ∪ f₂.support, g2 x (f₂ x)

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
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

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
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α

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
N : Type u_7
inst✝¹ : Zero M
inst✝ : CommMonoid N
f₁ f₂ : α →₀ M
g1 g2 : α → M → N
h : ∀ (x : α), g1 x (f₁ x) = g2 x (f₂ x)
hg1 : ∀ (i : α), g1 i 0 = 1
hg2 : ∀ (i : α), g2 i 0 = 1
⊢ Finset α
Tactic:
exact Finset.prod_congr rfl (fun x _ ↦ h x)
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
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 ⊢
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
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
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
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
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
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
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
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
Proof 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
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
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
Proof 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
Theorem: LinearIndependent.update
Proof 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
Proof 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
Theorem: LinearIndependent.update
Proof 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
Proof 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
Theorem: LinearIndependent.update
Proof 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
Proof 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
Theorem: LinearIndependent.update
Proof 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]
Proof 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
Theorem: LinearIndependent.update
Proof 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'
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

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