awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
suffices : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
⊢ False

Tactic:
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 <| by simpa
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g : G
⊢ HSMul.hSMul (β := F) g ((l : (a : F) → F) i : F) = (l : (a : F) → F) i

Tactic:
eq_of_sub_eq_zero
      (linearIndependent_iff'.1 (ih hs.1) s.attach (fun i => g • l i - l i) ?_ ⟨i, his⟩
          (mem_attach _ _) :
        _)

Premises used: HSub.hSub, Finset.mem_attach, linearIndependent_iff', eq_of_sub_eq_zero, Subtype.mk, And.left, Finset.attach, Iff.mp, HSMul.hSMul, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g : G
i₁ :
  Eq (α := G → F)
    (∑ i ∈ s.attach,
      HSMul.hSMul (α := F) (β := G → F)
        ((fun (i : (↑(↑s : Set F) : Type v)) ↦
            HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) (↑i : F) : F))
              ((l : (a : F) → F) (↑i : F) : F))
          i)
        ((toFun G F : (a : F) → G → F) (↑i : F) : G → F))
    0
⊢ HSMul.hSMul (β := F) g ((l : (a : F) → F) i : F) = (l : (a : F) → F) i

Tactic:
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 _ _) :
        _)

Premises used: HSub.hSub, Finset.mem_attach, linearIndependent_iff', eq_of_sub_eq_zero, Subtype.mk, And.left, Finset.attach, Iff.mp, HSMul.hSMul, Subtype.val, DFunLike.coe
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g : G
⊢ Eq (α := G → F)
    (∑ i ∈ s.attach,
      HSMul.hSMul (α := F) (β := G → F)
        ((fun (i : (↑(↑s : Set F) : Type v)) ↦
            HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) (↑i : F) : F))
              ((l : (a : F) → F) (↑i : F) : F))
          i)
        ((toFun G F : (a : F) → G → F) (↑i : F) : G → F))
    0

Tactic:
(sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_

Premises used: HSub.hSub, Finset.sum_attach, HSMul.hSMul, MulAction.toFun, DFunLike.coe, Eq.trans
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g : G
refine :
  Eq (α := G → F)
    (∑ x ∈ s,
      HSMul.hSMul (β := G → F)
        (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
        ((toFun G F : (a : F) → G → F) x : G → F))
    0
⊢ Eq (α := G → F)
    (∑ i ∈ s.attach,
      HSMul.hSMul (α := F) (β := G → F)
        ((fun (i : (↑(↑s : Set F) : Type v)) ↦
            HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) (↑i : F) : F))
              ((l : (a : F) → F) (↑i : F) : F))
          i)
        ((toFun G F : (a : F) → G → F) (↑i : F) : G → F))
    0

Tactic:
refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_

Premises used: HSub.hSub, Finset.sum_attach, HSMul.hSMul, MulAction.toFun, DFunLike.coe, Eq.trans
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g : G
h :
  ∀ (g' : G),
    Eq.{v + 1} (α := F)
      ((∑ x ∈ s,
          HSMul.hSMul (β := G → F)
            (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
            ((toFun G F : (a : F) → G → F) x : G → F))
        g')
      (0 g')
⊢ Eq (α := G → F)
    (∑ x ∈ s,
      HSMul.hSMul (β := G → F)
        (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
        ((toFun G F : (a : F) → G → F) x : G → F))
    0

Tactic:
ext g'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
rw :
  ∑ c ∈ s,
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'
| (∑ x ∈ s,
      HSMul.hSMul (β := G → F)
        (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
        ((toFun G F : (a : F) → G → F) x : G → F))
    g'

Tactic:
rw [sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
s₁ : s
f :
  fun (c : F) ↦
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'
| ∑ c ∈ s,
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'

Tactic:
congr
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
| s

Tactic:
· skip
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F),
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
      ((toFun G F : (a : F) → G → F) x : G → F) g'
| fun (c : F) ↦
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'

Tactic:
ext
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
x : F
f :
  HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F) -
    HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F)
| HSMul.hSMul (β := G → F)
    (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
    ((toFun G F : (a : F) → G → F) x : G → F) g'

Tactic:
rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Premises used: sub_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F),
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F) -
      HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F)
| fun (c : F) ↦
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'

Tactic:
ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Premises used: sub_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F),
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
      ((toFun G F : (a : F) → G → F) x : G → F) g'
f₁ :
  ∀ (x : F),
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F) -
      HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F)
| fun (c : F) ↦
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'

Tactic:
· ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Premises used: sub_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
rw :
  ∑ c ∈ s,
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'
s₁ : s
f f₁ :
  fun (c : F) ↦
    HSMul.hSMul (β := G → F)
      (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) c : F)) ((l : (a : F) → F) c : F))
      ((toFun G F : (a : F) → G → F) c : G → F) g'
| (∑ x ∈ s,
      HSMul.hSMul (β := G → F)
        (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
        ((toFun G F : (a : F) → G → F) x : G → F))
    g'

Tactic:
rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Premises used: Finset.sum_apply, sub_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h :
  Eq (α := F)
    (∑ x ∈ s,
      (HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F) -
        HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F)))
    (0 g')
⊢ Eq.{v + 1} (α := F)
    ((∑ x ∈ s,
        HSMul.hSMul (β := G → F)
          (HSub.hSub (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((l : (a : F) → F) x : F))
          ((toFun G F : (a : F) → G → F) x : G → F))
      g')
    (0 g')

Tactic:
conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]

Premises used: Finset.sum_apply, sub_smul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
h :
  Eq (α := F)
    (∑ x ∈ s,
      HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F))
    (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))
⊢ Eq (α := F)
    (∑ x ∈ s,
      (HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F) -
        HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F)))
    (0 g')

Tactic:
rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]

Premises used: sub_eq_zero, Pi.zero_apply, Finset.sum_sub_distrib
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
s₁ : s
f :
  fun (x : F) ↦
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
| ∑ x ∈ s,
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
congr
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s_1 : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
a : F
s : Finset F
has : a ∉ s
ih :
  LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
hs : LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))
l : F →₀ F
hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l
hla :
  Eq (α := G → F)
    (∑ i ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) i : F) ((toFun G F : (a : F) → G → F) i : G → F) :
      G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
i : F
his : i ∈ s
g g' : G
f :
  ∀ (x : F),
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
| fun (x : F) ↦
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)

Tactic:
ext x