-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Mul (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸 : Type u_6
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) ↦ f i x) (f' i) x
m : E
h₁ :
  Eq.{u_6 + 1} (α := 𝔸)
    ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
            (∑ x_1 : Fin l.length,
              List.prod
                  (List.take (↑x_1 : ℕ) (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length))) •>
                (proj (φ := fun (a : Fin l.length) ↦ 𝔸) x_1 <•
                  List.prod
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                      (List.drop (↑x_1 : ℕ).succ (List.finRange l.length)))))
            (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
          (a : E) → 𝔸)
        m :
      𝔸)
    ((∑ x_1 : Fin l.length,
            List.prod
                (List.take (↑x_1 : ℕ) (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.map l.get (List.finRange l.length)))) •>
              (f' (l.get x_1) <•
                List.prod
                  (List.map (fun (x_2 : ι) ↦ f x_2 x)
                    (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))) :
          (a : E) → 𝔸)
        m :
      𝔸)
⊢ Eq.{u_6 + 1} (α := 𝔸)
    ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
            (∑ i : Fin l.length,
              List.prod
                  (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.take (↑i : ℕ) (List.finRange l.length))) •>
                (proj (φ := fun (a : Fin l.length) ↦ 𝔸) i <•
                  List.prod
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x)
                      (List.drop (↑i : ℕ).succ (List.finRange l.length)))))
            (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
          (a : E) → 𝔸)
        m :
      𝔸)
    ((∑ x_1 : Fin l.length,
            List.prod
                (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.take (↑x_1 : ℕ) (List.map l.get (List.finRange l.length)))) •>
              (f' (l.get x_1) <•
                List.prod
                  (List.map (fun (x_2 : ι) ↦ f x_2 x)
                    (List.drop (↑x_1 : ℕ).succ (List.map l.get (List.finRange l.length))))) :
          (a : E) → 𝔸)
        m :
      𝔸)
have h₂ : Eq.{u_6 + 1} (α := 𝔸)
  ((comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Fin l.length) → 𝔸)
          (∑ x_1 : Fin l.length,
            List.prod
                (List.take (↑x_1 : ℕ) (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length))) •>
              (proj (φ := fun (a : Fin l.length) ↦ 𝔸) x_1 <•
                List.prod
                  (List.drop (↑x_1 : ℕ).succ
                    (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length)))))
          (pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i)) :
        (a : E) → 𝔸)
      m :
    𝔸)
  ((∑ x_1 : Fin l.length,
          List.prod
              (List.take (↑x_1 : ℕ) (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.map l.get (List.finRange l.length)))) •>
            (f' (l.get x_1) <•
              List.prod
                (List.drop (↑x_1 : ℕ).succ
                  (List.map (fun (x_2 : ι) ↦ f x_2 x) (List.map l.get (List.finRange l.length))))) :
        (a : E) → 𝔸)
      m :
    𝔸)
Tactic: simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    proj_apply, pi_apply, Function.comp_def]