-- 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
have : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
have₁ :
  ∀ (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₂ : IsEmpty.{v + 1} (↑(↑∅ : Set F) : Type v)
have₃ have₄ :
  ∀ (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₅ :
  ∀ (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₆ :
  ∀ (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₇ :
  ∀ (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₈ have₉ :
  ∀ (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₁₀ :
  ∀ (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₁₁ have₁₂ :
  ∀ (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₁₃ :
  ∀ (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
⊢ LinearIndepOn (↥(subfield G F)) id (↑s : Set F) →
    LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (↑s : Set F)
have have₁₄ : ∀ (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
Tactic: classical
  have : IsEmpty ((∅ : Finset F) : Set F) := by simp
  refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
  rw [coe_insert] at hs ⊢
  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
  rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
  rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
  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
  intro i his g
  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 _ _) :
        _)
  refine (sum_attach s fun i ↦ (g • l i - l i) • MulAction.toFun G F i).trans ?_
  ext g'; dsimp only
  conv_lhs =>
    rw [sum_apply]
    congr
    · skip
    · ext
      rw [Pi.smul_apply, sub_smul, smul_eq_mul]
  rw [sum_sub_distrib, Pi.zero_apply, sub_eq_zero]
  conv_lhs =>
    congr
    · skip
    · ext x
      rw [toFun_apply, ← mul_inv_cancel_left g g', mul_smul, ← smul_mul', ← toFun_apply _ x]
  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'
  rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ←
    sum_apply _ _ fun y => l y • toFun G F y]
  rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left]