awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ (i : Fin (List.finRange n).length),
    Membership.mem (γ := Finset (Fin (List.finRange n).length)) Finset.univ i ↔
      Membership.mem (α := Fin n) (γ := Finset (Fin n)) Finset.univ
        ((finCongr ⋯ : (a : Fin (List.finRange n).length) → Fin n) i : Fin n)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ ∀ (i : Fin (List.finRange n).length),
    Membership.mem (γ := Finset (Fin (List.finRange n).length)) Finset.univ i →
      (List.map x (List.take (↑i : ℕ) (List.finRange n))).prod •>
          (proj (φ := fun (a : Fin n) ↦ 𝔸)
              (getElem (valid := fun (xs : List (Fin n)) (i : Fin (List.finRange n).length) ↦ (↑i : ℕ) < xs.length)
                (List.finRange n) i ⋯) <•
            (List.map x (List.drop (↑i : ℕ).succ (List.finRange n))).prod) =
        (List.map x
              (List.take (↑((finCongr ⋯ : (a : Fin (List.finRange n).length) → Fin n) i) : ℕ)
                (List.finRange n))).prod •>
          ((proj (φ := fun (a : Fin n) ↦ 𝔸) ((finCongr ⋯ : (a : Fin (List.finRange n).length) → Fin n) i) :
              ((i : Fin n) → 𝔸) →L[𝕜] 𝔸) <•
            (List.map x
                (List.drop (↑((finCongr ⋯ : (a : Fin (List.finRange n).length) → Fin n) i) : ℕ).succ
                  (List.finRange n))).prod)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ ∀ (i : Fin l.length),
    Membership.mem (γ := Finset (Fin l.length)) Finset.univ i ↔
      Membership.mem (α := Fin l.attach.length) (γ := Finset (Fin l.attach.length)) Finset.univ
        ((finCongr ⋯ : (a : Fin l.length) → Fin l.attach.length) i : Fin l.attach.length)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ ∀ (i : Fin l.length),
    Membership.mem (γ := Finset (Fin l.length)) Finset.univ i →
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
          (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
              (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
                l.attach (Fin.cast ⋯ i) ⋯) <•
            (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod) =
        (List.map x (List.take (↑((finCongr ⋯ : (a : Fin l.length) → Fin l.attach.length) i) : ℕ) l.attach)).prod •>
          (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
              (getElem (idx := Fin l.attach.length) (valid :=
                fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length) l.attach
                ((finCongr ⋯ : (a : Fin l.length) → Fin l.attach.length) i : Fin l.attach.length) ⋯) <•
            (List.map x
                (List.drop (↑((finCongr ⋯ : (a : Fin l.length) → Fin l.attach.length) i) : ℕ).succ l.attach)).prod)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : { x : ι // x ∈ l } → 𝔸) ↦ (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
        (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
            (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
              l.attach (Fin.cast ⋯ i) ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod))
    x

Tactic:
exact hasStrictFDerivAt_list_prod'.congr_fderiv <| Eq.symm <|
    Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

Premises used: finCongr, List.length_attach, HasStrictFDerivAt.congr_fderiv, hasStrictFDerivAt_list_prod', Eq.symm, Finset.sum_equiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : { x : ι // x ∈ l } → 𝔸) ↦ (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
        (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
            (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
              l.attach (Fin.cast ⋯ i) ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod))
    x

Tactic:
classical exact hasStrictFDerivAt_list_prod'.congr_fderiv <| Eq.symm <|
    Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

Premises used: finCongr, List.length_attach, HasStrictFDerivAt.congr_fderiv, hasStrictFDerivAt_list_prod', Eq.symm, Finset.sum_equiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : Finite ι
l : List ι
x : ι → 𝔸'
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x

Tactic:
have := Fintype.ofFinite ι
  hasStrictFDerivAt_list_prod'.hasFDerivAt

Premises used: Fintype.ofFinite, HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_list_prod'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : Fin n → 𝔸
⊢ HasFDerivAt.{u_1, u_6, u_6} (𝕜 := 𝕜) (F := 𝔸) (fun (x : Fin n → 𝔸) ↦ (List.map x (List.finRange n)).prod)
    (∑ i : Fin n,
      (List.map x (List.take (↑i : ℕ) (List.finRange n))).prod •>
        (proj (φ := fun (a : Fin n) ↦ 𝔸) i <• (List.map x (List.drop (↑i : ℕ).succ (List.finRange n))).prod))
    x

Tactic:
hasStrictFDerivAt_list_prod_finRange'.hasFDerivAt

Premises used: hasStrictFDerivAt_list_prod_finRange', HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : { x : ι // x ∈ l } → 𝔸) ↦ (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
        (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
            (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
              l.attach (Fin.cast ⋯ i) ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod))
    x

Tactic:
hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_list_prod_attach'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : { x : ι // x ∈ l } → 𝔸) ↦ (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
        (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
            (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
              l.attach (Fin.cast ⋯ i) ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod))
    x

Tactic:
exact hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_list_prod_attach'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i : ι // i ∈ l } → 𝔸
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : { x : ι // x ∈ l } → 𝔸) ↦ (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l.attach)).prod •>
        (proj (φ := fun (a : { x : ι // x ∈ l }) ↦ 𝔸)
            (getElem (valid := fun (xs : List { x : ι // x ∈ l }) (i : Fin l.attach.length) ↦ (↑i : ℕ) < xs.length)
              l.attach (Fin.cast ⋯ i) ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l.attach)).prod))
    x

Tactic:
classical exact hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Premises used: HasStrictFDerivAt.hasFDerivAt, hasStrictFDerivAt_list_prod_attach'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
have :
  ∀ (this : Fintype ι),
    HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
      (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x

Tactic:
hasStrictFDerivAt_list_prod'.congr_fderiv ?_

Premises used: HasStrictFDerivAt.congr_fderiv, hasStrictFDerivAt_list_prod'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
refine :
  Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l))
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (List.map x l).prod)
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)) x

Tactic:
refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_

Premises used: HasStrictFDerivAt.congr_fderiv, hasStrictFDerivAt_list_prod'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
arg : List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l
| List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)

Tactic:
arg 1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
arg : l
| List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l

Tactic:
arg 2
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
rw : List.map l.get (List.finRange l.length)
| l

Tactic:
rw [← List.map_get_finRange l]

Premises used: List.map_get_finRange
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
arg : List.map l.get (List.finRange l.length)
| List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l)

Tactic:
arg 1; arg 2; rw [← List.map_get_finRange l]

Premises used: List.map_get_finRange
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
conv_rhs :
  Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum
      (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i)
        (List.map l.get (List.finRange l.length))))
⊢ Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) l))

Tactic:
conv_rhs => arg 1; arg 2; rw [← List.map_get_finRange l]

Premises used: List.map_get_finRange
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
simp :
  Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ x_1 : Fin l.length,
      (List.map x (List.take (↑x_1 : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) ⋯) <•
          (List.map x (List.drop ((↑x_1 : ℕ) + 1) l)).prod))
    (∑ x_1 : Fin l.length,
      ((List.map x (List.take (↑x_1 : ℕ) l)).prod * (List.map x (List.drop ((↑x_1 : ℕ) + 1) l)).prod) •>
        proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) ⋯))
⊢ Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸')
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    (List.sum
      (List.map (fun (i : ι) ↦ (List.map x (l.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i)
        (List.map l.get (List.finRange l.length))))

Tactic:
simp only [List.map_map, ← List.sum_toFinset _ (List.nodup_finRange _), List.toFinset_finRange,
    Function.comp_def, ((List.erase_getElem _).map _).prod_eq, List.eraseIdx_eq_take_drop_succ,
    List.map_append, List.prod_append, List.get_eq_getElem, Fin.getElem_fin, Nat.succ_eq_add_one]

Premises used: List.prod_append, Nat.succ_eq_add_one, List.Perm.prod_eq, List.get_eq_getElem, List.sum_toFinset, List.toFinset_finRange, List.erase_getElem, List.map_map, List.eraseIdx_eq_take_drop_succ, Function.comp_def, Fin.getElem_fin, List.nodup_finRange, List.map_append, List.Perm.map
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
h_1 : Membership.mem (γ := Finset (Fin l.length)) Finset.univ i
h :
  ∀ (x_1 : ι → 𝔸'),
    Eq.{u_7 + 1} (α := 𝔸')
      (((List.map x (List.take (↑i : ℕ) l)).prod •>
              (proj (φ := fun (a : ι) ↦ 𝔸')
                  (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) <•
                (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) :
            (a : ι → 𝔸') → 𝔸')
          x_1 :
        𝔸')
      ((((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) •>
              proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
            (a : ι → 𝔸') → 𝔸')
          x_1 :
        𝔸')
⊢ (List.map x (List.take (↑i : ℕ) l)).prod •>
      (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) <•
        (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) =
    ((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) •>
      proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
h_1 : Membership.mem (γ := Finset (Fin l.length)) Finset.univ i
x_1 : ι → 𝔸'
h :
  (List.map x (List.take (↑i : ℕ) l)).prod *
      HMul.hMul (β := 𝔸') (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod
        ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
              (a : ι → 𝔸') → 𝔸')
            x_1 :
          𝔸') =
    HMul.hMul (β := 𝔸') ((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod)
      ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
            (a : ι → 𝔸') → 𝔸')
          x_1 :
        𝔸')
⊢ Eq.{u_7 + 1} (α := 𝔸')
    (((List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) <•
              (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')
    ((((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod) •>
            proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
          (a : ι → 𝔸') → 𝔸')
        x_1 :
      𝔸')

Tactic:
simp only [smul_apply, op_smul_eq_smul, smul_eq_mul]

Premises used: ContinuousLinearMap.smul_apply, smul_eq_mul, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
i : Fin l.length
h : Membership.mem (γ := Finset (Fin l.length)) Finset.univ i
x_1 : ι → 𝔸'
⊢ (List.map x (List.take (↑i : ℕ) l)).prod *
      HMul.hMul (β := 𝔸') (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod
        ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
              (a : ι → 𝔸') → 𝔸')
            x_1 :
          𝔸') =
    HMul.hMul (β := 𝔸') ((List.map x (List.take (↑i : ℕ) l)).prod * (List.map x (List.drop ((↑i : ℕ) + 1) l)).prod)
      ((proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑i : ℕ) ⋯) :
            (a : ι → 𝔸') → 𝔸')
          x_1 :
        𝔸')

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
l : List ι
x : ι → 𝔸'
this : Fintype ι
⊢ Eq (α := (ι → 𝔸') →L[𝕜] 𝔸')
    (∑ x_1 : Fin l.length,
      (List.map x (List.take (↑x_1 : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) ⋯) <•
          (List.map x (List.drop ((↑x_1 : ℕ) + 1) l)).prod))
    (∑ x_1 : Fin l.length,
      ((List.map x (List.take (↑x_1 : ℕ) l)).prod * (List.map x (List.drop ((↑x_1 : ℕ) + 1) l)).prod) •>
        proj (φ := fun (a : ι) ↦ 𝔸') (getElem (valid := fun (as : List ι) (i : ℕ) ↦ i < as.length) l (↑x_1 : ℕ) ⋯))

Tactic:
exact Finset.sum_congr rfl fun i _ ↦ by
    ext; simp only [smul_apply, op_smul_eq_smul, smul_eq_mul]; ring

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
u : Multiset ι
x : ι → 𝔸'
this : Fintype ι
l : List ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (Multiset.map x ⟦l⟧).prod)
    (Multiset.sum
      (Multiset.map (fun (i : ι) ↦ (Multiset.map x (Multiset.erase ⟦l⟧ i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) ⟦l⟧))
    x

Tactic:
simpa using hasStrictFDerivAt_list_prod

Premises used: hasStrictFDerivAt_list_prod
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
inst_3 : DecidableEq ι
inst_4 : Finite ι
u : Multiset ι
x : ι → 𝔸'
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (Multiset.map x u).prod)
    (Multiset.sum (Multiset.map (fun (i : ι) ↦ (Multiset.map x (u.erase i)).prod •> proj (φ := fun (a : ι) ↦ 𝔸') i) u))
    x

Tactic:
have := Fintype.ofFinite ι
  hasStrictFDerivAt_multiset_prod.hasFDerivAt

Premises used: Fintype.ofFinite, hasStrictFDerivAt_multiset_prod, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst_3 : DecidableEq ι
inst_4 : Finite ι
x : ι → 𝔸'
simp :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (Multiset.map x u.val).prod)
    (Multiset.sum
      (Multiset.map (fun (x_1 : ι) ↦ (Multiset.map x (u.erase x_1).val).prod •> proj (φ := fun (a : ι) ↦ 𝔸') x_1)
        u.val))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ ∏ i ∈ u, x i)
    (∑ i ∈ u, (∏ j ∈ u.erase i, x j) •> proj (φ := fun (a : ι) ↦ 𝔸') i) x

Tactic:
simp only [Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod]

Premises used: Finset.sum_eq_multiset_sum, Finset.prod_eq_multiset_prod
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸' : Type u_7
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
inst_3 : DecidableEq ι
inst_4 : Finite ι
x : ι → 𝔸'
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸') (fun (x : ι → 𝔸') ↦ (Multiset.map x u.val).prod)
    (Multiset.sum
      (Multiset.map (fun (x_1 : ι) ↦ (Multiset.map x (u.erase x_1).val).prod •> proj (φ := fun (a : ι) ↦ 𝔸') x_1)
        u.val))
    x

Tactic:
hasStrictFDerivAt_multiset_prod

Premises used: hasStrictFDerivAt_multiset_prod, Multiset.erase