awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
s₁ : s
| (∑ 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 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: 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
⊢ 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')
have 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')
Tactic: conv_lhs =>
    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
⊢ 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')
have 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))
Tactic: rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
-- 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,
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
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
| ∑ 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)
have 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: 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 (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)
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)
Tactic: ext x
-- 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
| HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
have f : g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
Tactic: rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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 (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)
have f : ∀ (x : F), g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
Tactic: ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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 (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)
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)
Tactic: · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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),
    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)
have f₁ : ∀ (x : F), g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F)
Tactic: · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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,
    HMul.hMul (β := F) (HSMul.hSMul (β := F) g ((l : (a : F) → F) x : F)) ((toFun G F : (a : F) → G → F) x g' : F)
have s₁ : s
Tactic: congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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
| ∑ 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)
have 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: congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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
⊢ 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))
have h : Eq (α := F)
  (∑ x ∈ s, g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F))
  (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))
Tactic: conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
-- 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
⊢ Eq (α := F)
    (∑ x ∈ s,
      g • HMul.hMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x (g⁻¹ * g') : F))
    (∑ x ∈ s, HSMul.hSMul (α := F) (β := F) ((l : (a : F) → F) x : F) ((toFun G F : (a : F) → G → F) x g' : F))
have h : Eq (α := F)
  (∑ x ∈ s,
    HSMul.hSMul (β := F) g
      ((fun (y : F) ↦
          HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
        x (g⁻¹ * g')))
  (∑ x ∈ s,
    (fun (y : F) ↦
        HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
      x g')
Tactic: change
    (∑ x ∈ s, g • (fun y => l y • MulAction.toFun G F y) x (g⁻¹ * g')) =
      ∑ x ∈ s, (fun y => l y • MulAction.toFun G F y) x 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
⊢ Eq (α := F)
    (∑ x ∈ s,
      HSMul.hSMul (β := F) g
        ((fun (y : F) ↦
            HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
          x (g⁻¹ * g')))
    (∑ x ∈ s,
      (fun (y : F) ↦
          HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) y : F) ((toFun G F : (a : F) → G → F) y : G → F))
        x g')
have h : HSMul.hSMul (β := F) g
    ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
      (g⁻¹ * g')) =
  (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'
Tactic: rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
-- 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
⊢ HSMul.hSMul (β := F) g
      ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
        (g⁻¹ * g')) =
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'
have h : HSMul.hSMul (β := F) g ((toFun G F : (a : F) → G → F) a (g⁻¹ * g') : F) = (toFun G F : (a : F) → G → F) a g'
Tactic: rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- 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
h : HSMul.hSMul (β := F) g ((toFun G F : (a : F) → G → F) a (g⁻¹ * g') : F) = (toFun G F : (a : F) → G → F) a g'
⊢ HSMul.hSMul (β := F) g
      ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
        (g⁻¹ * g')) =
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'
have h₁ : g • (g⁻¹ * g') • a = (toFun G F : (a : F) → G → F) a g'
Tactic: rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]
-- 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
h : HSMul.hSMul (β := F) g ((toFun G F : (a : F) → G → F) a (g⁻¹ * g') : F) = (toFun G F : (a : F) → G → F) a g'
h₁ : g • (g⁻¹ * g') • a = (toFun G F : (a : F) → G → F) a g'
⊢ HSMul.hSMul (β := F) g
      ((∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F))
        (g⁻¹ * g')) =
    (∑ c ∈ s, HSMul.hSMul (α := F) (β := G → F) ((l : (a : F) → F) c : F) ((toFun G F : (a : F) → G → F) c : G → F)) g'
have h₂ : g • (g⁻¹ * g') • a = g' • a
Tactic: rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]