-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
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, HasFDerivAt (fun (x : E) ↦ f i x) (f' i) x
m : E
h₁ :
  Eq.{u_6 + 1} (α := 𝔸)
    ((ContinuousLinearMap.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 :
      𝔸)
h₂ :
  Eq.{u_6 + 1} (α := 𝔸)
    ((ContinuousLinearMap.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 :
      𝔸)
h₃ :
  Eq.{u_6 + 1} (α := 𝔸)
    ((ContinuousLinearMap.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) ∘ 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) ∘ l.get) (List.finRange l.length)))) :
          (a : E) → 𝔸)
        m :
      𝔸)
h₄ :
  Eq.{u_6 + 1} (α := 𝔸)
    ((∑ 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)))) :
          (a : (i : Fin l.length) → 𝔸) → 𝔸)
        ((pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i) : (a : E) → (i : Fin l.length) → 𝔸)
            m :
          (i : Fin l.length) → 𝔸) :
      𝔸)
    ((∑ x_1 : Fin l.length,
            List.prod (List.take (↑x_1 : ℕ) (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ 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) ∘ l.get) (List.finRange l.length)))) :
          (a : E) → 𝔸)
        m :
      𝔸)
h₅ :
  Eq.{u_6 + 1} (α := 𝔸)
    (∑ d : Fin l.length,
      (List.prod (List.take (↑d : ℕ) (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length))) •>
            (proj (φ := fun (a : Fin l.length) ↦ 𝔸) d <•
              List.prod
                (List.drop (↑d : ℕ).succ
                  (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length)))) :
          (a : (i : Fin l.length) → 𝔸) → 𝔸)
        ((pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i) : (a : E) → (i : Fin l.length) → 𝔸)
            m :
          (i : Fin l.length) → 𝔸))
    (∑ d : Fin l.length,
      (List.prod (List.take (↑d : ℕ) (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length))) •>
            (f' (l.get d) <•
              List.prod
                (List.drop (↑d : ℕ).succ (List.map ((fun (x_1 : ι) ↦ f x_1 x) ∘ l.get) (List.finRange l.length)))) :
          (a : E) → 𝔸)
        m)
h₆ :
  Eq.{u_6 + 1} (α := 𝔸)
    (∑ 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 : (a : (i : Fin l.length) → 𝔸) → 𝔸)
              ((pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i) :
                    (a : E) → (i : Fin l.length) → 𝔸)
                  m :
                (i : Fin l.length) → 𝔸) :
            𝔸) <•
          List.prod
            (List.drop (↑x_1 : ℕ).succ (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length)))))
    (∑ x_1 : Fin l.length,
      List.prod (List.take (↑x_1 : ℕ) (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length))) •>
        (((f' (l.get x_1) : (a : E) → 𝔸) m : 𝔸) <•
          List.prod
            (List.drop (↑x_1 : ℕ).succ (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length)))))
h₇ :
  Eq.{u_6 + 1} (α := 𝔸)
    (∑ 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))) •>
        (((pi (φ := fun (i : Fin l.length) ↦ 𝔸) fun (i : Fin l.length) ↦ f' (l.get i) :
                (a : E) → (i : Fin l.length) → 𝔸)
              m 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)))))
    (∑ x_1 : Fin l.length,
      List.prod (List.take (↑x_1 : ℕ) (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length))) •>
        (((f' (l.get x_1) : (a : E) → 𝔸) m : 𝔸) <•
          List.prod
            (List.drop (↑x_1 : ℕ).succ (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length)))))
h₈ :
  Eq.{u_6 + 1} (α := 𝔸)
    (∑ 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))) •>
        (((f' (l.get x_1) : (a : E) → 𝔸) m : 𝔸) <•
          List.prod
            (List.drop (↑x_1 : ℕ).succ (List.map (fun (i : Fin l.length) ↦ f (l.get i) x) (List.finRange l.length)))))
    (∑ x_1 : Fin l.length,
      List.prod (List.take (↑x_1 : ℕ) (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length))) •>
        (((f' (l.get x_1) : (a : E) → 𝔸) m : 𝔸) <•
          List.prod
            (List.drop (↑x_1 : ℕ).succ (List.map ((fun (x_2 : ι) ↦ f x_2 x) ∘ l.get) (List.finRange l.length)))))
⊢ Eq.{u_6 + 1} (α := 𝔸)
    ((ContinuousLinearMap.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 :
      𝔸)

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]

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, List.map_drop, ContinuousLinearMap.pi_apply, ContinuousLinearMap.proj_apply, List.map_map, Function.comp_def, List.map_take, ContinuousLinearMap.comp_apply