awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Valuation (goal)
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
⊢ Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
have have : ∀ (this : Fintype Fq), Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
Tactic: have : Fintype Fq := Fintype.ofFinite Fq
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Valuation (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
have hpow : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Valuation (goal)
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
⊢ LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
have pos : a = 0 → LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Valuation (goal)
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 : Γ)
⊢ LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
have neg : ¬a = 0 → LE.le.{u_3} (α := Γ) ((v : (a : A) → Γ) ((algebraMap Fq A : (a : Fq) → A) a : A) : Γ) (1 : Γ)
Tactic: by_cases a = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ fixedPoints M F = (↑(⨅ (m : M), FixedBy.subfield F m) : Set F)
have h : ∀ (x : F), x ∈ fixedPoints M F ↔ x ∈ (↑(⨅ (m : M), FixedBy.subfield F m) : Set F)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ g' • g • x = g • x
have rw : g' • x = x
Tactic: rw [hx, hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ g' • g • x = g • x
have rw₁ : x = x
Tactic: rw [hx, hx]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ m • ((↑f : F) * f') = (↑f : F) * m • f'
have rw : m • (↑f : F) * m • f' = (↑f : F) * m • f'
Tactic: rw [smul_mul', f.prop m]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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'
⊢ m • ((↑f : F) * f') = (↑f : F) * m • f'
have rw₁ : (↑f : F) * m • f' = (↑f : F) * m • f'
Tactic: rw [smul_mul', f.prop m]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
⊢ 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
have 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))
Tactic: rw [Polynomial.smul_C, smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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))
⊢ 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
have 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))
Tactic: rw [Polynomial.smul_C, smul]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ m • (p + q) = p + q
have rw : m • p + m • q = p + q
Tactic: rw [smul_add, ihp, ihq]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ m • (p + q) = p + q
have rw₁ : p + m • q = p + q
Tactic: rw [smul_add, ihp, ihq]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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
⊢ m • (p + q) = p + q
have rw₂ : p + q = p + q
Tactic: rw [smul_add, ihp, ihq]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
n : ℕ
x : ↥(subfield M F)
h :
  m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n)
⊢ m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
have rw : HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) *
    m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1) =
  HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
Tactic: rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
n : ℕ
x : ↥(subfield M F)
h :
  m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n)
rw :
  HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) *
      m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
⊢ m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
have rw₁ : HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) (m • x) : Polynomial ↥(subfield M F))
    (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
  HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
Tactic: rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
n : ℕ
x : ↥(subfield M F)
h :
  m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n)
rw :
  HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) *
      m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₁ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) (m • x) : Polynomial ↥(subfield M F))
      (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
⊢ m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
have rw₂ : HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
  HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
Tactic: rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
-- Lean 4 proof step from Mathlib.FieldTheory.Fixed (goal)
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)
n : ℕ
x : ↥(subfield M F)
h :
  m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X n)
rw :
  HSMul.hSMul (β := Polynomial ↥(subfield M F)) m
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F)) *
      m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₁ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) (m • x) : Polynomial ↥(subfield M F))
      (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
rw₂ :
  HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (m • HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
⊢ m •
      HMul.hMul (α := Polynomial ↥(subfield M F))
        ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
        (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1)) =
    HMul.hMul (α := Polynomial ↥(subfield M F))
      ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
      (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
have rw₃ : HMul.hMul (α := 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.X ^ (n + 1)) =
  HMul.hMul (α := Polynomial ↥(subfield M F))
    ((Polynomial.C : (a : ↥(subfield M F)) → Polynomial ↥(subfield M F)) x : Polynomial ↥(subfield M F))
    (HPow.hPow (α := Polynomial ↥(subfield M F)) Polynomial.X (n + 1))
Tactic: rw [smul_mul', Polynomial.smul_C, smul, smul_pow', Polynomial.smul_X]
-- 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 : Finset F
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have this : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
Tactic: have : IsEmpty ((∅ : Finset F) : Set F) := by simp
-- 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 : 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)
have 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)
Tactic: refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
-- 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 (↑(insert a s) : Set F)
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑(insert a s) : Set F)
have 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))
Tactic: rw [coe_insert] at hs ⊢
Cleared hypotheses: hs
-- 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 (insert a (↑s : Set F))
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (insert a (↑s : Set F))
have hs₁ : 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
Cleared hypotheses: hs
-- 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))
⊢ LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (insert a (↑s : Set F))
have 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))
Tactic: rw [linearIndepOn_insert (mt mem_coe.1 has)]
-- 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))
⊢ 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))
have 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
Tactic: refine ⟨ih hs.1, fun ha => ?_⟩
-- 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))
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
have 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)
Tactic: rw [Finsupp.mem_span_image_iff_linearCombination] at ha
Cleared hypotheses: ha
-- 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))
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)
⊢ False
have 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
Tactic: rcases ha with ⟨l, hl, hla⟩
Cleared hypotheses: ha