-- 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))
⊢ 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))),
  LinearIndepOn F (M := G → F) (⇑(toFun G F) : (a : F) → G → F) (insert a (↑s : Set F))
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]