awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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)
⊢ False
have 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)
Tactic: rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
Cleared hypotheses: hla
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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)
⊢ False
have 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)
Tactic: replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
Cleared hypotheses: hla
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (hypothesis)
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)
⊢ False
have hla₁ : ∑ 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
Cleared hypotheses: hla
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
have 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)
Tactic: refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 (α := F) ((l : (a : F) → F) c : F) c)
have 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) sorry :
      ↥(subfield G F))
    c)
Tactic: change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
⊢ False
have suffices : ∀ i ∈ s, Membership.mem (α := F) (γ := Subfield F) (subfield G F) ((l : (a : F) → F) i : F)
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
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
have 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
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 _ _) :
        _)
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
have 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
Tactic: refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
    (∑ 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
have 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')
Tactic: ext g'
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 ∈ 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'
have 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'
Tactic: rw [sum_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| ∑ 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'
have s₁ : s
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| ∑ 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'
have 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: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| 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'
have 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'
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| 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'
have 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)
Tactic: rw [Pi.smul_apply, sub_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| 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'
have 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)
Tactic: ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
| 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'
have 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'
Tactic: · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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'
have 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)
Tactic: · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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 ∈ 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'
have 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'
Tactic: rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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'
have s₁ : s
Tactic: rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]