M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s : Finset F
this : IsEmpty ↑↑∅
⊢ (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s : Finset F
⊢ (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
haveI : IsEmpty ((∅ : Finset F) : Set F) := by simp
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : LinearIndependent { x // x ∈ subfield G F } fun i => ↑i
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s : Finset F
this : IsEmpty ↑↑∅
⊢ (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
refine' Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => _
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : LinearIndependent { x // x ∈ subfield G F } fun i => ↑i
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : LinearIndependent { x // x ∈ subfield G F } fun i => ↑i
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
rw [coe_insert] at hs ⊢
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : LinearIndependent { x // x ∈ subfield G F } fun i => ↑i
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
rw [linearIndependent_insert (mt mem_coe.1 has)] at hs
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
⊢ (LinearIndependent F fun x => ↑(toFun G F) ↑x) ∧ ¬↑(toFun G F) a ∈ Submodule.span F (↑(toFun G F) '' ↑s)
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
⊢ LinearIndependent F fun i => ↑(toFun G F) ↑i
rw [linearIndependent_insert' (mt mem_coe.1 has)]
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
ha : ↑(toFun G F) a ∈ Submodule.span F (↑(toFun G F) '' ↑s)
⊢ False
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
⊢ (LinearIndependent F fun x => ↑(toFun G F) ↑x) ∧ ¬↑(toFun G F) a ∈ Submodule.span F (↑(toFun G F) '' ↑s)
refine' ⟨ih hs.1, fun ha => _⟩
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
ha : ∃ l, l ∈ Finsupp.supported F F ↑s ∧ ↑(Finsupp.total F (G → F) F ↑(toFun G F)) l = ↑(toFun G F) a
⊢ False
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
ha : ↑(toFun G F) a ∈ Submodule.span F (↑(toFun G F) '' ↑s)
⊢ False
rw [Finsupp.mem_span_image_iff_total] at ha
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ↑(Finsupp.total F (G → F) F ↑(toFun G F)) l = ↑(toFun G F) a
⊢ False
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
ha : ∃ l, l ∈ Finsupp.supported F F ↑s ∧ ↑(Finsupp.total F (G → F) F ↑(toFun G F)) l = ↑(toFun G F) a
⊢ False
rcases ha with ⟨l, hl, hla⟩
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
⊢ False
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ↑(Finsupp.total F (G → F) F ↑(toFun G F)) l = ↑(toFun G F) a
⊢ False
rw [Finsupp.total_apply_of_mem_supported F hl] at hla
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
⊢ ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
⊢ False
suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
  replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
  simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
  refine' hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => _)
  change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
  exact Submodule.smul_mem _ _ (Submodule.subset_span <| mem_coe.2 hcs)
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ g • ↑l i = ↑l i
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
⊢ ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
intro i his g
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ ∑ i in attach s, (fun i => g • ↑l ↑i - ↑l ↑i) i • ↑(toFun G F) ↑i = 0
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ g • ↑l i = ↑l i
refine'
  eq_of_sub_eq_zero
    (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) _ ⟨i, his⟩
        (mem_attach _ _) :
      _)
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ ∑ x in s, (g • ↑l x - ↑l x) • ↑(toFun G F) x = 0
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ ∑ i in attach s, (fun i => g • ↑l ↑i - ↑l ↑i) i • ↑(toFun G F) ↑i = 0
refine' (@sum_attach _ _ s _ fun i => (g • l i - l i) • MulAction.toFun G F i).trans _
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ Finset.sum s (fun x => (g • ↑l x - ↑l x) • ↑(toFun G F) x) g' = OfNat.ofNat 0 g'
case intro.intro
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g : G
⊢ ∑ x in s, (g • ↑l x - ↑l x) • ↑(toFun G F) x = 0
ext g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ Finset.sum s (fun x => (g • ↑l x - ↑l x) • ↑(toFun G F) x) g' = OfNat.ofNat 0 g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ Finset.sum s (fun x => (g • ↑l x - ↑l x) • ↑(toFun G F) x) g' = OfNat.ofNat 0 g'
dsimp only
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x in s, g • ↑l x * ↑(toFun G F) x g' = ∑ x in s, ↑l x • ↑(toFun G F) x g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x in s, (g • ↑l x * ↑(toFun G F) x g' - ↑l x • ↑(toFun G F) x g') = OfNat.ofNat 0 g'
rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x in s, g • (fun y => ↑l y • ↑(toFun G F) y) x (g⁻¹ * g') = ∑ x in s, (fun y => ↑l y • ↑(toFun G F) y) x g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x in s, g • (↑l x * ↑(toFun G F) x (g⁻¹ * g')) = ∑ x in s, ↑l x • ↑(toFun G F) x g'
show
  (∑ x in s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
    ∑ x in s, (fun y => l y • MulAction.toFun G F y) x g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) (g⁻¹ * g') = Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ ∑ x in s, g • (fun y => ↑l y • ↑(toFun G F) y) x (g⁻¹ * g') = ∑ x in s, (fun y => ↑l y • ↑(toFun G F) y) x g'
rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
  sum_apply _ _ fun y => l y • toFun G F y]
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) (g⁻¹ * g') = Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) g'
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) (g⁻¹ * g') = Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) g'
dsimp only
no goals
case intro.intro.h
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
⊢ g • Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) (g⁻¹ * g') = Finset.sum s (fun c => ↑l c • ↑(toFun G F) c) g'
rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
no goals
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s : Finset F
⊢ IsEmpty ↑↑∅
simp
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ c in s, (↑l c • ↑(toFun G F) c) 1 = ↑(toFun G F) a 1
⊢ False
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
⊢ False
replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
⊢ False
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ c in s, (↑l c • ↑(toFun G F) c) 1 = ↑(toFun G F) a 1
⊢ False
simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
c : F
hcs : c ∈ s
⊢ ↑l c • c ∈ Submodule.span { x // x ∈ subfield G F } ↑s
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
⊢ False
refine' hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => _)
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
c : F
hcs : c ∈ s
⊢ { val := ↑l c, property := (_ : ↑l c ∈ subfield G F) } • c ∈ Submodule.span { x // x ∈ subfield G F } ↑s
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
c : F
hcs : c ∈ s
⊢ ↑l c • c ∈ Submodule.span { x // x ∈ subfield G F } ↑s
change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
no goals
M : Type u
inst✝⁴ : Monoid M
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction M F
inst✝ : MulSemiringAction G F
m : M
s✝ : Finset F
this✝ : IsEmpty ↑↑∅
a : F
s : Finset F
has : ¬a ∈ s
ih : (LinearIndependent { x // x ∈ subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(toFun G F) ↑i
hs : (LinearIndependent { x // x ∈ subfield G F } fun b => ↑b) ∧ ¬a ∈ Submodule.span { x // x ∈ subfield G F } ↑s
l : F →₀ F
hl : l ∈ Finsupp.supported F F ↑s
this : ∀ (i : F), i ∈ s → ↑l i ∈ subfield G F
hla : ∑ x in s, ↑l x • x = a
c : F
hcs : c ∈ s
⊢ { val := ↑l c, property := (_ : ↑l c ∈ subfield G F) } • c ∈ Submodule.span { x // x ∈ subfield G F } ↑s
exact Submodule.smul_mem _ _ (Submodule.subset_span <| mem_coe.2 hcs)