[GOAL]
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
⊢ fixedPoints M F = ↑(⨅ (m : M), FixedBy.subfield F m)
[PROOFSTEP]
ext z
[GOAL]
case 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
z : F
⊢ z ∈ fixedPoints M F ↔ z ∈ ↑(⨅ (m : M), FixedBy.subfield F m)
[PROOFSTEP]
simp [fixedPoints, FixedBy.subfield, iInf, Subfield.mem_sInf]
[GOAL]
case 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
z : F
⊢ (∀ (m : M), m • z = z) ↔
    ∀ (i : M),
      z ∈
        {
          toSubmonoid :=
            {
              toSubsemigroup :=
                { carrier := fixedBy M F i,
                  mul_mem' := (_ : ∀ {a b : F}, a ∈ fixedBy M F i → b ∈ fixedBy M F i → i • (a * b) = a * b) },
              one_mem' := (_ : i • 1 = 1) },
          add_mem' :=
            (_ :
              ∀ {a b : F},
                a ∈
                    {
                          toSubsemigroup :=
                            { carrier := fixedBy M F i,
                              mul_mem' :=
                                (_ : ∀ {a b : F}, a ∈ fixedBy M F i → b ∈ fixedBy M F i → i • (a * b) = a * b) },
                          one_mem' := (_ : i • 1 = 1) }.toSubsemigroup.carrier →
                  b ∈
                      {
                            toSubsemigroup :=
                              { carrier := fixedBy M F i,
                                mul_mem' :=
                                  (_ : ∀ {a b : F}, a ∈ fixedBy M F i → b ∈ fixedBy M F i → i • (a * b) = a * b) },
                            one_mem' := (_ : i • 1 = 1) }.toSubsemigroup.carrier →
                    i • (a + b) = a + b),
          zero_mem' := (_ : i • 0 = 0) }
[PROOFSTEP]
rfl
[GOAL]
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 g : M
x : F
hx : x ∈ subfield M F
g' : M
⊢ g' • g • x = g • x
[PROOFSTEP]
rw [hx, hx]
[GOAL]
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 : M
f : { x // x ∈ subfield M F }
f' : F
⊢ m • (↑f * f') = ↑f * m • f'
[PROOFSTEP]
rw [smul_mul', f.prop m]
[GOAL]
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 : M
p : Polynomial { x // x ∈ subfield M F }
x : { x // x ∈ subfield M F }
⊢ m • ↑Polynomial.C x = ↑Polynomial.C x
[PROOFSTEP]
rw [Polynomial.smul_C, smul]
[GOAL]
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 : M
p✝ p q : Polynomial { x // x ∈ subfield M F }
ihp : m • p = p
ihq : m • q = q
⊢ m • (p + q) = p + q
[PROOFSTEP]
rw [smul_add, ihp, ihq]
[GOAL]
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 : M
p : Polynomial { x // x ∈ subfield M F }
n : ℕ
x : { x // x ∈ subfield M F }
x✝ : m • (↑Polynomial.C x * Polynomial.X ^ n) = ↑Polynomial.C x * Polynomial.X ^ n
⊢ m • (↑Polynomial.C x * Polynomial.X ^ (n + 1)) = ↑Polynomial.C x * Polynomial.X ^ (n + 1)
[PROOFSTEP]
rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
[GOAL]
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
⊢ Algebra { x // x ∈ subfield M F } F
[PROOFSTEP]
infer_instance
[GOAL]
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
[PROOFSTEP]
haveI : IsEmpty ((∅ : Finset F) : Set F) := by simp
[GOAL]
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 ↑↑∅
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
refine' Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => _
[GOAL]
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
[PROOFSTEP]
rw [coe_insert] at hs ⊢
[GOAL]
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
[PROOFSTEP]
rw [linearIndependent_insert (mt mem_coe.1 has)] at hs 
[GOAL]
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
[PROOFSTEP]
rw [linearIndependent_insert' (mt mem_coe.1 has)]
[GOAL]
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)
[PROOFSTEP]
refine' ⟨ih hs.1, fun ha => _⟩
[GOAL]
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
[PROOFSTEP]
rw [Finsupp.mem_span_image_iff_total] at ha 
[GOAL]
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
[PROOFSTEP]
rcases ha with ⟨l, hl, hla⟩
[GOAL]
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
[PROOFSTEP]
rw [Finsupp.total_apply_of_mem_supported F hl] at hla 
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
[GOAL]
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
[PROOFSTEP]
simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla 
[GOAL]
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
[PROOFSTEP]
refine' hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => _)
[GOAL]
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
[PROOFSTEP]
change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
[GOAL]
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
[PROOFSTEP]
exact Submodule.smul_mem _ _ (Submodule.subset_span <| mem_coe.2 hcs)
[GOAL]
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
[PROOFSTEP]
intro i his g
[GOAL]
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
[PROOFSTEP]
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 _ _) : _)
[GOAL]
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
[PROOFSTEP]
refine' (@sum_attach _ _ s _ fun i => (g • l i - l i) • MulAction.toFun G F i).trans _
[GOAL]
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
[PROOFSTEP]
ext g'
[GOAL]
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'
[PROOFSTEP]
dsimp only
[GOAL]
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'
[PROOFSTEP]
conv_lhs =>
  rw [sum_apply]
  congr
  ·skip
  · ext
    rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
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'
[PROOFSTEP]
  rw [sum_apply]
  congr
  ·skip
  · ext
    rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
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'
[PROOFSTEP]
  rw [sum_apply]
  congr
  ·skip
  · ext
    rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
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'
[PROOFSTEP]
rw [sum_apply]
[GOAL]
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
| ∑ c in s, ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
congr
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
case f
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
| fun c => ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
·skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case f
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
| fun c => ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
· ext
  rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
case f
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
| fun c => ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
  ext
  rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
case f
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
| fun c => ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
  ext
  rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
case f
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
| fun c => ((g • ↑l c - ↑l c) • ↑(toFun G F) c) g'
[PROOFSTEP]
ext
[GOAL]
case f.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✝ : F
| ((g • ↑l x✝ - ↑l x✝) • ↑(toFun G F) x✝) g'
[PROOFSTEP]
rw [Pi.smul_apply, sub_smul, smul_eq_mul]
[GOAL]
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'
[PROOFSTEP]
rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
[GOAL]
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'
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  · ext x
    rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
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'
[PROOFSTEP]
  congr
  ·skip
  · ext x
    rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
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'
[PROOFSTEP]
  congr
  ·skip
  · ext x
    rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
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'
[PROOFSTEP]
congr
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
case f
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
| fun x => g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
·skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case 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
hla : ∑ i in s, ↑l i • ↑(toFun G F) i = ↑(toFun G F) a
i : F
his : i ∈ s
g g' : G
| s
[PROOFSTEP]
skip
[GOAL]
case f
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
| fun x => g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
· ext x
  rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
case f
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
| fun x => g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
  ext x
  rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
case f
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
| fun x => g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
  ext x
  rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
case f
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
| fun x => g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
ext x
[GOAL]
case f.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 : F
| g • ↑l x * ↑(toFun G F) x g'
[PROOFSTEP]
rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
[GOAL]
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'
[PROOFSTEP]
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'
[GOAL]
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'
[PROOFSTEP]
rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ← sum_apply _ _ fun y => l y • toFun G F y]
[GOAL]
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'
[PROOFSTEP]
dsimp only
[GOAL]
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'
[PROOFSTEP]
rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
[GOAL]
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
inst✝ : Fintype G
x : F
⊢ Polynomial.Monic (minpoly G F x)
[PROOFSTEP]
simp only [minpoly, Polynomial.monic_toSubring]
[GOAL]
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
inst✝ : Fintype G
x : F
⊢ Polynomial.Monic (prodXSubSmul G F x)
[PROOFSTEP]
exact prodXSubSmul.monic G F x
[GOAL]
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
inst✝ : Fintype G
x : F
⊢ Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
[PROOFSTEP]
rw [← prodXSubSmul.eval G F x, Polynomial.eval₂_eq_eval_map]
[GOAL]
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
inst✝ : Fintype G
x : F
⊢ Polynomial.eval x (Polynomial.map (Subring.subtype (subfield G F).toSubring) (minpoly G F x)) =
    Polynomial.eval x (prodXSubSmul G F x)
[PROOFSTEP]
simp only [minpoly, Polynomial.map_toSubring]
[GOAL]
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
inst✝ : Fintype G
x : F
H : minpoly G F x = 1
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
⊢ 1 = 0
[PROOFSTEP]
rwa [H, Polynomial.eval₂_one] at this 
[GOAL]
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
inst✝ : Fintype G
x : F
f : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
⊢ minpoly G F x ∣ f
[PROOFSTEP]
have : (subfield G F).subtype = (subfield G F).toSubring.subtype := rfl
[GOAL]
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
inst✝ : Fintype G
x : F
f : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
this : Subfield.subtype (subfield G F) = Subring.subtype (subfield G F).toSubring
⊢ minpoly G F x ∣ f
[PROOFSTEP]
have h :
  Polynomial.map (MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f =
    Polynomial.map ((IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f :=
  rfl
[GOAL]
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
inst✝ : Fintype G
x : F
f : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
this : Subfield.subtype (subfield G F) = Subring.subtype (subfield G F).toSubring
h :
  Polynomial.map (MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f =
    Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f
⊢ minpoly G F x ∣ f
[PROOFSTEP]
erw [← Polynomial.map_dvd_map' (Subfield.subtype <| FixedPoints.subfield G F), minpoly, this,
  Polynomial.map_toSubring _ _, prodXSubSmul]
[GOAL]
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
inst✝ : Fintype G
x : F
f : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
this : Subfield.subtype (subfield G F) = Subring.subtype (subfield G F).toSubring
h :
  Polynomial.map (MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f =
    Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f
⊢ ∏ g : G ⧸ stabilizer G x, (Polynomial.X - ↑Polynomial.C (ofQuotientStabilizer G x g)) ∣
    Polynomial.map (Subring.subtype (subfield G F).toSubring) f
[PROOFSTEP]
refine'
  Fintype.prod_dvd_of_coprime (Polynomial.pairwise_coprime_X_sub_C <| MulAction.injective_ofQuotientStabilizer G x)
    fun y => QuotientGroup.induction_on y fun g => _
[GOAL]
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
inst✝ : Fintype G
x : F
f : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.eval₂ (Subfield.subtype (subfield G F)) x f = 0
this : Subfield.subtype (subfield G F) = Subring.subtype (subfield G F).toSubring
h :
  Polynomial.map (MulSemiringActionHom.toRingHom (IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f =
    Polynomial.map (↑(IsInvariantSubring.subtypeHom G (subfield G F).toSubring)) f
y : G ⧸ stabilizer G x
g : G
⊢ Polynomial.X - ↑Polynomial.C (ofQuotientStabilizer G x ↑g) ∣
    Polynomial.map (Subring.subtype (subfield G F).toSubring) f
[PROOFSTEP]
rw [Polynomial.dvd_iff_isRoot, Polynomial.IsRoot.def, MulAction.ofQuotientStabilizer_mk, Polynomial.eval_smul', ← this,
  ← Subfield.toSubring_subtype_eq_subtype, ← IsInvariantSubring.coe_subtypeHom' G (FixedPoints.subfield G F).toSubring,
  h, ← MulSemiringActionHom.coe_polynomial, ← MulSemiringActionHom.map_smul, smul_polynomial,
  MulSemiringActionHom.coe_polynomial, ← h, IsInvariantSubring.coe_subtypeHom', Polynomial.eval_map,
  Subfield.toSubring_subtype_eq_subtype, hf, smul_zero]
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
have hf2 : f ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_right _ _
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f ∣ minpoly G F x
[PROOFSTEP]
rw [← hfg]
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
⊢ f ∣ f * g
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
have hg2 : g ∣ minpoly G F x := by rw [← hfg]; exact dvd_mul_left _ _
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ minpoly G F x
[PROOFSTEP]
rw [← hfg]
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
⊢ g ∣ f * g
[PROOFSTEP]
exact dvd_mul_left _ _
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
have := eval₂ G F x
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x (minpoly G F x) = 0
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
rw [← hfg, Polynomial.eval₂_mul, mul_eq_zero] at this 
[GOAL]
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this :
  Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0 ∨
    Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
cases' this with this this
[GOAL]
case inl
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
right
[GOAL]
case inl.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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
⊢ g = 1
[PROOFSTEP]
have hf3 : f = minpoly G F x :=
  Polynomial.eq_of_monic_of_associated hf (monic G F x) (associated_of_dvd_dvd hf2 <| @of_eval₂ G _ F _ _ _ x f this)
[GOAL]
case inl.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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x f = 0
hf3 : f = minpoly G F x
⊢ g = 1
[PROOFSTEP]
rwa [← mul_one (minpoly G F x), hf3, mul_right_inj' (monic G F x).ne_zero] at hfg 
[GOAL]
case inr
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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1 ∨ g = 1
[PROOFSTEP]
left
[GOAL]
case inr.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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
⊢ f = 1
[PROOFSTEP]
have hg3 : g = minpoly G F x :=
  Polynomial.eq_of_monic_of_associated hg (monic G F x) (associated_of_dvd_dvd hg2 <| @of_eval₂ G _ F _ _ _ x g this)
[GOAL]
case inr.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
inst✝ : Fintype G
x : F
f g : Polynomial { x // x ∈ subfield G F }
hf : Polynomial.Monic f
hg : Polynomial.Monic g
hfg : f * g = minpoly G F x
hf2 : f ∣ minpoly G F x
hg2 : g ∣ minpoly G F x
this : Polynomial.eval₂ (Subring.subtype (subfield G F).toSubring) x g = 0
hg3 : g = minpoly G F x
⊢ f = 1
[PROOFSTEP]
rwa [← one_mul (minpoly G F x), hg3, mul_left_inj' (monic G F x).ne_zero] at hfg 
[GOAL]
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
inst✝ : Finite G
x : F
⊢ IsIntegral { x // x ∈ subfield G F } x
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case 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
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral { x // x ∈ subfield G F } x
[PROOFSTEP]
exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩
[GOAL]
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
inst✝ : Fintype G
x : F
s : Finset F
hs : LinearIndependent { x // x ∈ subfield G F } fun i => ↑i
⊢ card s ≤ Fintype.card G
[PROOFSTEP]
simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast, Cardinal.natCast_le] using
  cardinal_lift_le_rank_of_linearIndependent' (linearIndependent_smul_of_linearIndependent G F hs)
[GOAL]
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
inst✝ : Finite G
x : F
⊢ Polynomial.Splits (RingHom.id F)
    (Polynomial.map (algebraMap { x // x ∈ subfield G F } F) (_root_.minpoly { x // x ∈ subfield G F } x))
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case 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
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ Polynomial.Splits (RingHom.id F)
    (Polynomial.map (algebraMap { x // x ∈ subfield G F } F) (_root_.minpoly { x // x ∈ subfield G F } x))
[PROOFSTEP]
rw [← minpoly_eq_minpoly, minpoly, coe_algebraMap, ← Subfield.toSubring_subtype_eq_subtype,
  Polynomial.map_toSubring _ (subfield G F).toSubring, prodXSubSmul]
[GOAL]
case 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
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ Polynomial.Splits (RingHom.id F)
    (∏ g : G ⧸ stabilizer G x, (Polynomial.X - ↑Polynomial.C (ofQuotientStabilizer G x g)))
[PROOFSTEP]
exact Polynomial.splits_prod _ fun _ _ => Polynomial.splits_X_sub_C _
[GOAL]
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
inst✝ : Finite G
x : F
⊢ Polynomial.Separable (_root_.minpoly { x // x ∈ subfield G F } x)
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case 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
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ Polynomial.Separable (_root_.minpoly { x // x ∈ subfield G F } x)
[PROOFSTEP]
erw [← minpoly_eq_minpoly, ← Polynomial.separable_map (FixedPoints.subfield G F).subtype, minpoly,
  Polynomial.map_toSubring _ (subfield G F).toSubring]
[GOAL]
case 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
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ Polynomial.Separable (prodXSubSmul G F x)
[PROOFSTEP]
exact Polynomial.separable_prod_X_sub_C_iff.2 (injective_ofQuotientStabilizer G x)
[GOAL]
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
inst✝ : Finite G
⊢ FiniteDimensional { x // x ∈ subfield G F } F
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case 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
inst✝ : Finite G
val✝ : Fintype G
⊢ FiniteDimensional { x // x ∈ subfield G F } F
[PROOFSTEP]
exact
  IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt <| Cardinal.nat_lt_aleph0 _)
[GOAL]
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
inst✝ : Fintype G
⊢ finrank { x // x ∈ subfield G F } F ≤ Fintype.card G
[PROOFSTEP]
rw [← Cardinal.natCast_le, finrank_eq_rank]
[GOAL]
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
inst✝ : Fintype G
⊢ Module.rank { x // x ∈ subfield G F } F ≤ ↑(Fintype.card G)
[PROOFSTEP]
apply rank_le_card
[GOAL]
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
⊢ Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case 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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
[PROOFSTEP]
rw [Fintype.bijective_iff_injective_and_card]
[GOAL]
case 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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F) ∧
    Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
[PROOFSTEP]
constructor
[GOAL]
case intro.left
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Function.Injective (MulSemiringAction.toAlgHom { x // x ∈ subfield G F } F)
[PROOFSTEP]
exact MulSemiringAction.toAlgHom_injective _ F
[GOAL]
case intro.right
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G = Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case intro.right.a
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card G ≤ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F)
[PROOFSTEP]
exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
[GOAL]
case intro.right.a
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ Fintype.card G
[PROOFSTEP]
rw [← finrank_eq_card G F]
[GOAL]
case intro.right.a
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
G : Type u
F : Type v
inst✝⁴ : Group G
inst✝³ : Field F
inst✝² : Finite G
inst✝¹ : MulSemiringAction G F
inst✝ : FaithfulSMul G F
val✝ : Fintype G
⊢ Fintype.card (F →ₐ[{ x // x ∈ subfield G F }] F) ≤ finrank { x // x ∈ subfield G F } F
[PROOFSTEP]
exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linear_map' _ _ _)
