awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
h :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
        (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
      ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
    ∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) =
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (f i z)
        (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
h₁ :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
        (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
      ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F' →
    HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i) = HSMul.hSMul (α := F') ((∏ i ∈ t, f i) z) (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (f i * ∏ x ∈ t, f x) s z
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) +
      HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i))

Tactic:
convert! hf.1.mul (IH hf.2) using 2

Premises used: And.right, And.left, HasMFDerivWithinAt.mul
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
h :
  Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)))
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x))
    (∑ x ∈ t, (f i z * ∏ j ∈ t.erase x, f j z) • f' x)
⊢ ∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F') (f i z)
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
simp only [t.smul_sum, ← mul_smul]

Premises used: Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)))
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x))
    (∑ x ∈ t, (f i z * ∏ j ∈ t.erase x, f j z) • f' x)

Tactic:
t.sum_congr rfl (fun j hj ↦ ?_)

Premises used: Multiset.foldr, Multiset.prod, instModuleTangentSpace._aux_1, Finset.prod, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, Finset.sum_congr, rfl, instAddCommGroupTangentSpace._aux_4
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
h :
  ∀ (j : ι) (hj : j ∈ t),
    HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase j, f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
⊢ Eq (α :=
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)))
    (∑ x ∈ t, HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase x, f j z) (f' x))
    (∑ x ∈ t, (f i z * ∏ j ∈ t.erase x, f j z) • f' x)

Tactic:
refine t.sum_congr rfl (fun j hj ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
j : ι
hj : j ∈ t
⊢ i ≠ j

Tactic:
grind
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
j : ι
hj : j ∈ t
⊢ i ∉ t.erase j

Tactic:
grind
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_1 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
j : ι
hj : j ∈ t
h : HSMul.hSMul (α := F') (∏ j ∈ insert i (t.erase j), f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
h₁ h₂ : (f i z * ∏ x ∈ t.erase j, f x z) • f' j = (f i z * ∏ j ∈ t.erase j, f j z) • f' j
⊢ HSMul.hSMul (α := F') (∏ j ∈ (insert i t).erase j, f j z) (f' j) = (f i z * ∏ j ∈ t.erase j, f j z) • f' j

Tactic:
rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]

Premises used: Finset.prod_insert, Finset.erase_insert_of_ne
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t_1 : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
i : ι
t : Finset ι
hi : i ∉ t
IH :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
hf : HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i) ∧ ∀ x ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f x) s z (f' x)
e_2 :
  ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z)
      (TangentSpace 𝓘(𝕜, F') (HMul.hMul (β := M → F') (f i) (∏ x ∈ t, f x) z)) =
    ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
⊢ HSMul.hSMul (α := F') (∏ j ∈ t, f j z) (f' i) = HSMul.hSMul (α := F') ((∏ i ∈ t, f i) z) (f' i)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ ∅, f i) s z
      (∑ i ∈ ∅, HSMul.hSMul (α := F') (∏ j ∈ Finset.erase ∅ i, f j z) (f' i))
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (IH :
      ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
        HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
          (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i)))
    (hf : ∀ i_1 ∈ Insert.insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ Insert.insert i t, f i) s z
      (∑ i_1 ∈ Insert.insert i t, HSMul.hSMul (α := F') (∏ j ∈ (Insert.insert i t).erase i_1, f j z) (f' i_1))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i t hi IH =>
    rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]
    rw [t.forall_mem_insert] at hf
    convert! hf.1.mul (IH hf.2) using 2
    · simp only [t.smul_sum, ← mul_smul]
      refine t.sum_congr rfl (fun j hj ↦ ?_)
      rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
    · simp

Premises used: Finset.prod_insert, Finset.forall_mem_insert, Insert.insert, add_comm, Finset.erase_insert_of_ne, hasMFDerivWithinAt_const, Finset.smul_sum, Finset.sum_congr, SemigroupAction.mul_smul, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ ∅, f i) s z
      (∑ i ∈ ∅, HSMul.hSMul (α := F') (∏ j ∈ Finset.erase ∅ i, f j z) (f' i))
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (IH :
      ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) s z (f' i)),
        HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
          (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i)))
    (hf : ∀ i_1 ∈ Insert.insert i t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i_1) s z (f' i_1)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ Insert.insert i t, f i) s z
      (∑ i_1 ∈ Insert.insert i t, HSMul.hSMul (α := F') (∏ j ∈ (Insert.insert i t).erase i_1, f j z) (f' i_1))
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) s z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i t hi IH =>
    rw [t.sum_insert hi, t.erase_insert hi, t.prod_insert hi, add_comm]
    rw [t.forall_mem_insert] at hf
    convert! hf.1.mul (IH hf.2) using 2
    · simp only [t.smul_sum, ← mul_smul]
      refine t.sum_congr rfl (fun j hj ↦ ?_)
      rw [t.erase_insert_of_ne (by grind), Finset.prod_insert (by grind)]
    · simp

Premises used: Finset.prod_insert, Finset.forall_mem_insert, Insert.insert, add_comm, Finset.erase_insert_of_ne, hasMFDerivWithinAt_const, Finset.smul_sum, Finset.sum_congr, SemigroupAction.mul_smul, rfl
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivAt I 𝓘(𝕜, F') (f i) z (f' i)
simp_all :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) univ z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) univ z
      (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))
⊢ HasMFDerivAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) z (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
simp_all only [← hasMFDerivWithinAt_univ]

Premises used: hasMFDerivWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) univ z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) univ z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
HasMFDerivWithinAt.prod hf

Premises used: HasMFDerivWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_21} (RingHom.id 𝕜) (TangentSpace I z) F'
inst_8 : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, F') (f i) univ z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (M' := F') (∏ i ∈ t, f i) univ z
    (∑ i ∈ t, HSMul.hSMul (α := F') (∏ j ∈ t.erase i, f j z) (f' i))

Tactic:
exact HasMFDerivWithinAt.prod hf

Premises used: HasMFDerivWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[s] (f i) z
⊢ MDiffAt[s] (∏ i ∈ t, f i) z

Tactic:
(HasMFDerivWithinAt.prod
    fun i hi ↦ (hf i hi).hasMFDerivWithinAt).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[s] (f i) z
⊢ MDiffAt[s] (∏ i ∈ t, f i) z

Tactic:
exact (HasMFDerivWithinAt.prod
    fun i hi ↦ (hf i hi).hasMFDerivWithinAt).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[s] (f i) z
⊢ MDiffAt[s] (∏ i ∈ t, f i) z

Tactic:
classical exact (HasMFDerivWithinAt.prod
    fun i hi ↦ (hf i hi).hasMFDerivWithinAt).mdifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt (f i) z
⊢ ∀ i ∈ t, MDiffAt[univ] (f i) z

Tactic:
simp_all only [← mdifferentiableWithinAt_univ]

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[univ] (f i) z
⊢ MDiffAt[univ] (∏ i ∈ t, f i) z

Tactic:
MDifferentiableWithinAt.prod hf

Premises used: MDifferentiableWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
z : M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[univ] (f i) z
⊢ MDiffAt[univ] (∏ i ∈ t, f i) z

Tactic:
exact MDifferentiableWithinAt.prod hf

Premises used: MDifferentiableWithinAt.prod
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
s : Set M
F' : Type u_21
inst_6 : NormedCommRing F'
inst_7 : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiff[s] (f i)
⊢ MDiff[s] (∏ i ∈ t, f i)

Tactic:
fun z hz ↦ .prod fun i hi ↦ hf i hi z hz

Premises used: MDifferentiableOn, MDifferentiableWithinAt.prod