awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
ha : a ≠ 0
this : Fintype Fq
⊢ HPow.hPow (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (Fintype.card Fq - 1) = 1

Tactic:
simp [← map_pow, FiniteField.pow_card_sub_one_eq_one a ha]

Premises used: FiniteField.pow_card_sub_one_eq_one, map_pow
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
ha : a ≠ 0
this : Fintype Fq
⊢ HPow.hPow (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (Fintype.card Fq - 1) = 1

Tactic:
have hpow : (v (algebraMap Fq A a)) ^ (Fintype.card Fq - 1) = 1 := by
    simp [← map_pow, FiniteField.pow_card_sub_one_eq_one a ha]
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
ha : a ≠ 0
this : Fintype Fq
hpow : HPow.hPow (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (Fintype.card Fq - 1) = 1
⊢ Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)

Tactic:
grind [pow_eq_one_iff, → IsPrimePow.two_le, FiniteField.isPrimePow_card]

Premises used: FiniteField.isPrimePow_card, IsPrimePow.two_le, pow_eq_one_iff
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
pos : a = 0 → LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
neg : ¬a = 0 → LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)

Tactic:
by_cases a = 0
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
h : a = 0
⊢ LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)

Tactic:
grind [zero_le']

Premises used: zero_le'
-- Module: Mathlib.FieldTheory.Finite.Valuation
Goal:
Fq : Type u_1
A : Type u_2
Γ : Type u_3
inst : Field Fq
inst_1 : Finite Fq
inst_2 : Ring A
inst_3 : Algebra Fq A
inst_4 : LinearOrderedCommMonoidWithZero Γ
v : Valuation A Γ
a : Fq
h : ¬a = 0
⊢ LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)

Tactic:
grind [zero_le']

Premises used: zero_le'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
x : F
⊢ Membership.mem (γ := Subfield F) (subfield F m) x ↔ m • x = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedBy
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
K : Type u_1
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
inst_3 : Field K
inst_4 : Algebra K F
inst_5 : SMulCommClass M K F
x : F
⊢ Membership.mem (γ := IntermediateField K F) (intermediateField K F m) x ↔ m • x = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, MulAction.fixedBy
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
h : ∀ (x : F), x ∈ fixedPoints M F ↔ x ∈ (↑(⨅ (m : M), FixedBy.subfield F m) : Set F)
⊢ fixedPoints M F = (↑(⨅ (m : M), FixedBy.subfield F m) : Set F)

Tactic:
ext
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
x : F
⊢ x ∈ fixedPoints M F ↔ x ∈ (↑(⨅ (m : M), FixedBy.subfield F m) : Set F)

Tactic:
simp [FixedBy.subfield]

Premises used: FixedBy.subfield
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
g : M
x : F
hx : Membership.mem (γ := Subfield F) (subfield M F) x
g' : M
rw : g' • x = x
rw₁ rw₂ : x = x
⊢ g' • g • x = g • x

Tactic:
rw [hx, hx]
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m_1 : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
m : M
f : ↥(subfield M F)
f' : F
rw : m • (↑f : F) * m • f' = (↑f : F) * m • f'
rw₁ rw₂ : (↑f : F) * m • f' = (↑f : F) * m • f'
⊢ m • ((↑f : F) * f') = (↑f : F) * m • f'

Tactic:
rw [smul_mul', f.prop m]

Premises used: Subtype.prop, smul_mul'
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
⊢ SMulCommClass (↥(subfield M F)) M F

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
x : ↥(subfield M F)
⊢ m • x = x

Tactic:
Subtype.ext <| x.2 m

Premises used: Subtype.property, Subtype.ext
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
p : Polynomial ↥(subfield M F)
x : ↥(subfield M F)
rw :
  Eq (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) (m • x) : Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
rw₁ rw₂ :
  Eq (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
⊢ HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) =
    (Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x

Tactic:
rw [Polynomial.smul_C, smul]

Premises used: Polynomial.smul_C, FixedPoints.smul
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
m : M
p_1 p q : Polynomial ↥(subfield M F)
ihp : m • p = p
ihq : m • q = q
rw : m • p + m • q = p + q
rw₁ : p + m • q = p + q
rw₂ rw₃ : p + q = p + q
⊢ m • (p + q) = p + q

Tactic:
rw [smul_add, ihp, ihq]

Premises used: smul_add
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
G : Type u
inst_1 : Group G
K : Type u_1
F : Type v
inst_2 : Field F
inst_3 : MulSemiringAction M F
inst_4 : MulSemiringAction G F
m : M
inst_5 : Field K
inst_6 : Algebra K F
inst_7 : SMulCommClass M K F
⊢ Algebra (↥(subfield M F)) F

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Fixed
Goal:
M : Type u
inst : Monoid M
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction M F
⊢ Eq (α := ↥(subfield M F) →+* F) (algebraMap (↥(subfield M F)) F) (Subfield.subtype (subfield M F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
⊢ IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)

Tactic:
simp
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
⊢ IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)

Tactic:
have : IsEmpty ((∅ : Finset F) : Set F) := by simp
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)

Tactic:
Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_

Premises used: Finset.induction_on
-- Module: Mathlib.FieldTheory.Fixed
Goal:
G : Type u
inst : Group G
F : Type v
inst_1 : Field F
inst_2 : MulSemiringAction G F
s : Finset F
this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
refine :
  ∀ (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 (↑(insert a s) : Set F)),
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑(insert a s) : Set F)
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)

Tactic:
refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
-- 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 (↑(insert a s) : Set F)
rw :
  ∀ (hs : LinearIndepOn (↥(subfield G F)) id (insert a (↑s : Set F))),
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (insert a (↑s : Set F))
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑(insert a s) : Set F)

Tactic:
rw [coe_insert] at hs ⊢

Premises used: Finset.coe_insert
-- 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 (insert a (↑s : Set F))
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' (↑s : Set F))

Tactic:
rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs

Premises used: mt, Iff.mp, linearIndepOn_insert, Finset.mem_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))
rw :
  LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F) ∧
    ((toFun G F : (a : F) → G → F) a : G → F) ∉ Submodule.span F ((⇑(toFun G F) : (a : F) → G → F) '' (↑s : Set F))
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (insert a (↑s : Set F))

Tactic:
rw [linearIndepOn_insert (mt mem_coe.1 has)]

Premises used: mt, Iff.mp, linearIndepOn_insert, Finset.mem_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))
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F) ∧
    ((toFun G F : (a : F) → G → F) a : G → F) ∉ Submodule.span F ((⇑(toFun G F) : (a : F) → G → F) '' (↑s : Set F))

Tactic:
⟨ih hs.1, fun ha => ?_⟩

Premises used: And.left, And.intro
-- 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))
refine :
  ∀
    (ha :
      Membership.mem (α := G → F) (γ := Submodule F (G → F))
        (Submodule.span F ((⇑(toFun G F) : (a : F) → G → F) '' (↑s : Set F)))
        ((toFun G F : (a : F) → G → F) a : G → F)),
    False
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F) ∧
    ((toFun G F : (a : F) → G → F) a : G → F) ∉ Submodule.span F ((⇑(toFun G F) : (a : F) → G → F) '' (↑s : Set F))

Tactic:
refine ⟨ih hs.1, fun ha => ?_⟩
-- 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))
ha :
  Membership.mem (α := G → F) (γ := Submodule F (G → F))
    (Submodule.span F ((⇑(toFun G F) : (a : F) → G → F) '' (↑s : Set F))) ((toFun G F : (a : F) → G → F) a : G → F)
⊢ ∃ (l : F →₀ F),
    Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l ∧
      Eq (α := G → F) ((Finsupp.linearCombination F (⇑(toFun G F) : (a : F) → G → F) : (a : F →₀ F) → G → F) l : G → F)
        ((toFun G F : (a : F) → G → F) a : G → F)

Tactic:
rw [Finsupp.mem_span_image_iff_linearCombination] at ha

Premises used: Finsupp.mem_span_image_iff_linearCombination
-- 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))
ha :
  ∃ (l : F →₀ F),
    Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l ∧
      Eq (α := G → F) ((Finsupp.linearCombination F (⇑(toFun G F) : (a : F) → G → F) : (a : F →₀ F) → G → F) l : G → F)
        ((toFun G F : (a : F) → G → F) a : G → F)
rcases :
  ∀ (l : F →₀ F) (hl : Membership.mem (γ := Submodule F (F →₀ F)) (Finsupp.supported F F (↑s : Set F)) l)
    (hla :
      Eq (α := G → F) ((Finsupp.linearCombination F (⇑(toFun G F) : (a : F) → G → F) : (a : F →₀ F) → G → F) l : G → F)
        ((toFun G F : (a : F) → G → F) a : G → F)),
    False
⊢ False

Tactic:
rcases ha with ⟨l, hl, hla⟩
-- 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) ((Finsupp.linearCombination F (⇑(toFun G F) : (a : F) → G → F) : (a : F →₀ F) → G → F) l : G → F)
    ((toFun G F : (a : F) → G → F) a : G → F)
⊢ 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)

Tactic:
rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla

Premises used: Finsupp.linearCombination_apply_of_mem_supported
-- 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_1 : 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)
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
⊢ Eq (α := F)
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F) 1 :
      F)
    ((toFun G F : (a : F) → G → F) a 1 : F)

Tactic:
replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
-- 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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla :
  Eq (α := F)
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F) 1 :
      F)
    ((toFun G F : (a : F) → G → F) a 1 : F)
⊢ ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a

Tactic:
simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla

Premises used: MulAction.toFun_apply, one_smul, 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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla : ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a
⊢ False

Tactic:
hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)

Premises used: Submodule.sum_mem, Eq.rec, And.right
-- 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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla : ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a
refine :
  ∀ (c : F) (hcs : c ∈ s),
    Membership.mem (γ := Submodule (↥(subfield G F)) F) (Submodule.span (↥(subfield G F)) (id '' (↑s : Set F)))
      (HSMul.hSMul (α := F) ((l : (a : F) → F) c : F) c)
⊢ False

Tactic:
refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)

Premises used: Submodule.sum_mem, Eq.rec, And.right
-- 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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla : ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a
c : F
hcs : c ∈ s
change :
  Membership.mem (γ := Submodule (↥(subfield G F)) F) (Submodule.span (↥(subfield G F)) (id '' (↑s : Set F)))
    (HSMul.hSMul (α := ↥(subfield G F))
      (Subtype.mk (p := fun (x : F) ↦ Membership.mem (γ := Subfield F) (subfield G F) x) ((l : (a : F) → F) c) ⋯ :
        ↥(subfield G F))
      c)
⊢ Membership.mem (γ := Submodule (↥(subfield G F)) F) (Submodule.span (↥(subfield G F)) (id '' (↑s : Set F)))
    (HSMul.hSMul (α := F) ((l : (a : F) → F) c : F) c)

Tactic:
change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _

Premises used: Subtype.mk, 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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla : ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a
c : F
hcs : c ∈ s
⊢ c ∈ id '' (↑s : Set F)

Tactic:
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_1 : 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
this : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
hla : ∑ x ∈ s, HSMul.hSMul (α := F) ((l : (a : F) → F) x : F) x = a
c : F
hcs : c ∈ s
⊢ Membership.mem (γ := Submodule (↥(subfield G F)) F) (Submodule.span (↥(subfield G F)) (id '' (↑s : Set F)))
    (HSMul.hSMul (α := ↥(subfield G F))
      (Subtype.mk (p := fun (x : F) ↦ Membership.mem (γ := Subfield F) (subfield G F) x) ((l : (a : F) → F) c) ⋯ :
        ↥(subfield G F))
      c)

Tactic:
exact Submodule.smul_mem _ _ <| Submodule.subset_span <| by simpa

Premises used: Submodule.subset_span, Submodule.smul_mem