-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.LinearIndependent (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
H : ∀ (p : F[X]), Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E) → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) a : E) ≠ 0
b : E := ∏ j ∈ s, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)
h1 :
  ∀ i ∈ s,
    m i • (b * (HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) i : E))⁻¹) =
      HSMul.hSMul (β := E) (m i) (∏ j ∈ s.erase i, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E))
hm :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
    0
p : F[X] :=
  ∑ i ∈ s,
    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
      (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])
simp_rw :
  Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E)
    (∑ x_1 ∈ s,
        HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) :
      E)
simp_rw₁ :
  Eq.{u_2 + 1} (α := E)
    ((aeval x : (a : F[X]) → E)
        (∑ i ∈ s,
          HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m i) : F[X])
            (∏ j ∈ s.erase i, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])) :
      E)
    (∑ x_1 ∈ s,
        HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)) :
      E)
simp_rw₂ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      (aeval x : (a : F[X]) → E)
        (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (m x_1) : F[X])
          (∏ j ∈ s.erase x_1, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X]) : F[X])))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
simp_rw₃ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
        ((aeval x : (a : F[X]) → E)
            (∏ j ∈ s.erase x_1, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) j : F[X])) :
          E))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
simp_rw₄ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
        (∏ x_2 ∈ s.erase x_1,
            (aeval x : (a : F[X]) → E) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x_2 : F[X])) :
          E))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
simp_rw₅ :
  Eq.{u_2 + 1} (α := E)
    (∑ x_1 ∈ s,
      HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
        (∏ x_2 ∈ s.erase x_1,
            HSub.hSub (α := E) (β := E) ((aeval x : (a : F[X]) → E) X : E)
              ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) x_2 : F[X]) : E) :
          E))
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
⊢ Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
have simp_rw₆ : Eq.{u_2 + 1} (α := E)
  (∑ x_1 ∈ s,
    HMul.hMul (α := E) (β := E) ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) (m x_1) : F[X]) : E)
      (∏ x_2 ∈ s.erase x_1, HSub.hSub (β := E) x ((aeval x : (a : F[X]) → E) ((C : (a : F) → F[X]) x_2 : F[X]) : E) :
        E))
  (∑ x_1 ∈ s,
    HSMul.hSMul (β := E) (m x_1) (∏ j ∈ s.erase x_1, HSub.hSub (β := E) x ((algebraMap F E : (a : F) → E) j : E)))
Tactic: simp_rw [← hm, p, map_sum, map_mul, map_prod,
    map_sub, aeval_X, aeval_C, Algebra.smul_def]