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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
F : Type u_11
inst_16 : NormedAddCommGroup F
inst_17 : NormedSpace 𝕜 F
G : Type u_12
inst_18 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_19 : TopologicalSpace N
inst_20 : ChartedSpace G N
F' : Type u_14
inst_21 : NormedAddCommGroup F'
inst_22 : NormedSpace 𝕜 F'
G' : Type u_15
inst_23 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_24 : TopologicalSpace N'
inst_25 : ChartedSpace G' N'
F₁ : Type u_17
inst_26 : NormedAddCommGroup F₁
inst_27 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_28 : NormedAddCommGroup F₂
inst_29 : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst_30 : NormedAddCommGroup F₃
inst_31 : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst_32 : NormedAddCommGroup F₄
inst_33 : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
hs : UniqueMDiffWithinAt I s z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z))

Tactic:
exact mfderiv[s] f z

Premises used: mfderivWithin, modelWithCornersSelf
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
E'' : Type u_8
inst_11 : NormedAddCommGroup E''
inst_12 : NormedSpace 𝕜 E''
H'' : Type u_9
inst_13 : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst_14 : TopologicalSpace M''
inst_15 : ChartedSpace H'' M''
F : Type u_11
inst_16 : NormedAddCommGroup F
inst_17 : NormedSpace 𝕜 F
G : Type u_12
inst_18 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst_19 : TopologicalSpace N
inst_20 : ChartedSpace G N
F' : Type u_14
inst_21 : NormedAddCommGroup F'
inst_22 : NormedSpace 𝕜 F'
G' : Type u_15
inst_23 : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst_24 : TopologicalSpace N'
inst_25 : ChartedSpace G' N'
F₁ : Type u_17
inst_26 : NormedAddCommGroup F₁
inst_27 : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst_28 : NormedAddCommGroup F₂
inst_29 : NormedSpace 𝕜 F₂
F₃ : Type u_19
inst_30 : NormedAddCommGroup F₃
inst_31 : NormedSpace 𝕜 F₃
F₄ : Type u_20
inst_32 : NormedAddCommGroup F₄
inst_33 : NormedSpace 𝕜 F₄
s : Set M
x z : M
f g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
hs : UniqueMDiffWithinAt I s z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z))

Tactic:
exact mfderiv[s] g z

Premises used: mfderivWithin, modelWithCornersSelf
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
f g : M → E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
hs : UniqueMDiffWithinAt I s z
⊢ mfderivWithin I 𝓘(𝕜, E') (f + g) s z =
    HAdd.hAdd (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z)))
      (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z)))
      (mfderivWithin I 𝓘(𝕜, E') f s z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (f z)))
      (mfderivWithin I 𝓘(𝕜, E') g s z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (g z)))

Tactic:
(hf.hasMFDerivWithinAt.add hg.hasMFDerivWithinAt).mfderivWithin hs

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mfderivWithin, instModuleTangentSpace._aux_1, HasMFDerivWithinAt.add, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)

Tactic:
simpa using hasMFDerivWithinAt_const ..

Premises used: hasMFDerivWithinAt_const
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s_1 : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
i : ι
s : Finset ι
hi : i ∉ s
IH :
  ∀ (hf : ∀ i ∈ s, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s_1 z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ s, f i) s_1 z (∑ i ∈ s, f' i)
hf : ∀ i_1 ∈ insert i s, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i_1) s_1 z (f' i_1)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ insert i s, f i) s_1 z (∑ i ∈ insert i s, f' i)

Tactic:
grind [HasMFDerivWithinAt.add]

Premises used: HasMFDerivWithinAt.add
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
insert :
  ∀ (i : ι) (s_1 : Finset ι) (hi : i ∉ s_1)
    (IH :
      ∀ (hf : ∀ i ∈ s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
        HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ s_1, f i) s z (∑ i ∈ s_1, f' i))
    (hf : ∀ i_1 ∈ Insert.insert i s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i_1) s z (f' i_1)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ Insert.insert i s_1, f i) s z (∑ i ∈ Insert.insert i s_1, f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)

Tactic:
induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]

Premises used: Insert.insert, hasMFDerivWithinAt_const, HasMFDerivWithinAt.add
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ ∅, f i) s z (∑ i ∈ ∅, f' i)
insert :
  ∀ (i : ι) (s_1 : Finset ι) (hi : i ∉ s_1)
    (IH :
      ∀ (hf : ∀ i ∈ s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) s z (f' i)),
        HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ s_1, f i) s z (∑ i ∈ s_1, f' i))
    (hf : ∀ i_1 ∈ Insert.insert i s_1, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i_1) s z (f' i_1)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ Insert.insert i s_1, f i) s z (∑ i ∈ Insert.insert i s_1, f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) s z (∑ i ∈ t, f' i)

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simpa using hasMFDerivWithinAt_const ..
  | insert i s hi IH => grind [HasMFDerivWithinAt.add]

Premises used: Insert.insert, hasMFDerivWithinAt_const, HasMFDerivWithinAt.add
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivAt I 𝓘(𝕜, E') (f i) z (f' i)
simp_all :
  ∀ (hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) univ z (f' i)),
    HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) univ z (∑ i ∈ t, f' i)
⊢ HasMFDerivAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) z (∑ i ∈ t, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) univ z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) univ z (∑ i ∈ t, f' i)

Tactic:
HasMFDerivWithinAt.sum hf

Premises used: HasMFDerivWithinAt.sum
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
f' : ι → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : ∀ i ∈ t, HasMFDerivWithinAt I 𝓘(𝕜, E') (f i) univ z (f' i)
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (M' := E') (∑ i ∈ t, f i) univ z (∑ i ∈ t, f' i)

Tactic:
exact HasMFDerivWithinAt.sum hf

Premises used: HasMFDerivWithinAt.sum
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiffAt[s] (f i) z
⊢ MDiffAt[s] (∑ i ∈ t, f i) z

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

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.mdifferentiableWithinAt, HasMFDerivWithinAt.sum
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiffAt[univ] (f i) z
⊢ MDiffAt[univ] (∑ i ∈ t, f i) z

Tactic:
.sum hf

Premises used: MDifferentiableWithinAt.sum
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiffAt[univ] (f i) z
⊢ MDiffAt[univ] (∑ i ∈ t, f i) z

Tactic:
exact .sum hf
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiff[s] (f i)
⊢ MDiff[s] (∑ i ∈ t, f i)

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

Premises used: MDifferentiableOn, MDifferentiableWithinAt.sum
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
ι : Type
t : Finset ι
f : ι → M → E'
hf : ∀ i ∈ t, MDiff (f i)
⊢ MDiff (∑ i ∈ t, f i)

Tactic:
fun z ↦ .sum fun i hi ↦ hf i hi z

Premises used: MDifferentiableAt.sum, MDifferentiable
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivWithinAt I 𝓘(𝕜, E') f s z f'
a : 𝕜
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (a • f) s z (a • f')

Tactic:
⟨hf.1.const_smul a, hf.2.const_smul a⟩

Premises used: ContinuousWithinAt.const_smul, HasFDerivWithinAt.const_smul, And.right, And.left, And.intro, HasMFDerivWithinAt
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') f z f'
s : 𝕜
⊢ HasMFDerivAt I 𝓘(𝕜, E') (s • f) z (s • f')

Tactic:
⟨hf.1.const_smul s, hf.2.const_smul s⟩

Premises used: HasFDerivWithinAt.const_smul, HasMFDerivAt, ContinuousAt.const_smul, And.right, And.left, And.intro
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] f z
a : 𝕜
⊢ MDiffAt[s] (a • f) z

Tactic:
(hf.hasMFDerivWithinAt.const_smul a).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.const_smul, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
hf : MDiffAt f z
s : 𝕜
⊢ MDiffAt (s • f) z

Tactic:
(hf.hasMFDerivAt.const_smul s).mdifferentiableAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt, HasMFDerivAt.const_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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
s : Set M
f : M → E'
a : 𝕜
hf : MDiff[s] f
⊢ MDiff[s] (a • f)

Tactic:
fun x hx ↦ (hf x hx).const_smul a

Premises used: MDifferentiableOn, MDifferentiableWithinAt.const_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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
f : M → E'
s : 𝕜
hf : MDiff f
⊢ MDiff (s • f)

Tactic:
fun x ↦ (hf x).const_smul s

Premises used: MDifferentiableAt.const_smul, MDifferentiable
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
hf : MDiffAt f z
s : 𝕜
⊢ mfderiv% (s • f) z =
    HSMul.hSMul (β :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (f z))) s
      (mfderiv% f z)

Tactic:
(hf.hasMFDerivAt.const_smul s).mfderiv

Premises used: HasMFDerivAt.mfderiv, MDifferentiableAt.hasMFDerivAt, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, HasMFDerivAt.const_smul, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
s : Set M
hf : HasMFDerivWithinAt I 𝓘(𝕜, E') f s z f'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (-f) s z (-f')

Tactic:
⟨hf.1.neg, hf.2.neg⟩

Premises used: HasFDerivWithinAt.neg, And.right, And.left, And.intro, ContinuousWithinAt.neg, HasMFDerivWithinAt
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') f z f'
⊢ HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')

Tactic:
⟨hf.1.neg, hf.2.neg⟩

Premises used: HasFDerivWithinAt.neg, HasMFDerivAt, ContinuousAt.neg, And.right, And.left, And.intro
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
⊢ HasMFDerivAt I 𝓘(𝕜, E') (- -f) z (- -f')

Tactic:
hf.neg

Premises used: HasMFDerivAt.neg
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
h : f = - -f
h₁ : f = - -f → f' = - -f'
⊢ HasMFDerivAt I 𝓘(𝕜, E') f z f'

Tactic:
convert! hf.neg

Premises used: HasMFDerivAt.neg
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
z : M
f : M → E'
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f')
h h₁ : f = f
⊢ f = - -f

Tactic:
rw [neg_neg]

Premises used: neg_neg