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'
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')
e_21 : f = - -f
h h₁ : f' = f'
⊢ f' = - -f'

Tactic:
rw [neg_neg]

Premises used: neg_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'
s : Set M
hf : MDiffAt[s] f z
⊢ MDiffAt[s] (-f) z

Tactic:
(hf.hasMFDerivWithinAt.neg).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.neg, 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
⊢ MDiffAt (-f) z

Tactic:
hf.hasMFDerivAt.neg.mdifferentiableAt

Premises used: HasMFDerivAt.neg, MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt
-- 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 : Set M
hf : MDiff[s] f
⊢ MDiff[s] (-f)

Tactic:
fun x hx ↦ (hf x hx).neg

Premises used: MDifferentiableOn, MDifferentiableWithinAt.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'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
⊢ MDiffAt[s] (- -f) z

Tactic:
hf.neg

Premises used: MDifferentiableWithinAt.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'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
h : f = - -f
⊢ MDiffAt[s] f z

Tactic:
convert hf.neg

Premises used: MDifferentiableWithinAt.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'
s : Set M
z : M
f : M → E'
hf : MDiffAt[s] (-f) z
h h₁ : f = f
⊢ f = - -f

Tactic:
rw [neg_neg]

Premises used: neg_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'
hf : MDiffAt (-f) z
⊢ MDiffAt (- -f) z

Tactic:
hf.neg

Premises used: MDifferentiableAt.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'
hf : MDiffAt (-f) z
h : f = - -f
⊢ MDiffAt f z

Tactic:
convert! hf.neg

Premises used: MDifferentiableAt.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'
hf : MDiffAt (-f) z
h h₁ : f = f
⊢ f = - -f

Tactic:
rw [neg_neg]

Premises used: neg_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'
f : M → E'
hf : MDiff f
⊢ MDiff (-f)

Tactic:
fun x ↦ (hf x).neg

Premises used: MDifferentiableAt.neg, 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
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
simp_rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderivWithin I 𝓘(𝕜, E') (-f) s x) (-mfderivWithin I 𝓘(𝕜, E') f s x)

Tactic:
simp_rw [mfderivWithin]

Premises used: mfderivWithin
-- 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'
x : M
hs : UniqueMDiffWithinAt I s x
pos :
  ∀ (hf : MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
      (if MDiffAt[s] (-f) x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
      (-if MDiffAt[s] f x then
          fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
            ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
        else 0)
neg :
  ∀ (hf : ¬MDiffAt[s] f x),
    Eq (α :=
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
      (if MDiffAt[s] (-f) x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)
      (-if MDiffAt[s] f x then
          fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
            ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
        else 0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)

Tactic:
by_cases hf : MDiffAt[s] f x

Premises used: modelWithCornersSelf, 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'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : MDiffAt[s] f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)

Tactic:
hf.hasMFDerivWithinAt.neg.mfderivWithin hs

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.neg, mfderivWithin, HasMFDerivWithinAt.mfderivWithin, instModuleTangentSpace._aux_1, 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
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] f x
neg :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-if MDiffAt[s] f x then
        fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x f)
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
      else 0)

Tactic:
rw [if_neg hf]

Premises used: if_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'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] f x
⊢ ¬MDiffAt[s] (-f) x

Tactic:
rw [← mdifferentiableWithinAt_neg] at hf

Premises used: mdifferentiableWithinAt_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'
s : Set M
f : M → E'
x : M
hs : UniqueMDiffWithinAt I s x
hf : ¬MDiffAt[s] (-f) x
neg :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    0 (-0)
neg₁ neg₂ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    0 0
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
    else 0)
    (-0)

Tactic:
rw [if_neg hf, neg_zero]

Premises used: neg_zero, if_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'
f : M → E'
x : M
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderivWithin I 𝓘(𝕜, E') (-f) univ x) (-mfderiv% f x)
rw₁ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (-mfderivWithin I 𝓘(𝕜, E') f univ x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (-mfderiv% f x)
rw₂ rw₃ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (-mfderiv% f x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') (f x)))
    (-mfderiv% f x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace 𝓘(𝕜, E') ((-f) x)))
    (mfderiv% (-f) x) (-mfderiv% f x)

Tactic:
rw [← mfderivWithin_univ, mfderivWithin_neg _ _ (uniqueMDiffWithinAt_univ I), mfderivWithin_univ]

Premises used: mfderivWithin_univ, uniqueMDiffWithinAt_univ, mfderivWithin_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'
s : Set M
z : M
f g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivWithinAt I 𝓘(𝕜, E') f s z f'
hg : HasMFDerivWithinAt I 𝓘(𝕜, E') g s z g'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (f - g) s z (f' - g')

Tactic:
⟨hf.1.sub hg.1, hf.2.sub hg.2⟩

Premises used: ContinuousWithinAt.sub, And.right, And.left, HasFDerivWithinAt.sub, 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 g : M → E'
f' g' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) E'
hf : HasMFDerivAt I 𝓘(𝕜, E') f z f'
hg : HasMFDerivAt I 𝓘(𝕜, E') g z g'
⊢ HasMFDerivAt I 𝓘(𝕜, E') (f - g) z (f' - g')

Tactic:
⟨hf.1.sub hg.1, hf.2.sub hg.2⟩

Premises used: ContinuousAt.sub, HasMFDerivAt, And.right, And.left, HasFDerivWithinAt.sub, 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 g : M → E'
hf : MDiffAt[s] f z
hg : MDiffAt[s] g z
⊢ MDiffAt[s] (f - g) z

Tactic:
(hf.hasMFDerivWithinAt.sub hg.hasMFDerivWithinAt).mdifferentiableWithinAt

Premises used: MDifferentiableWithinAt.hasMFDerivWithinAt, HasMFDerivWithinAt.sub, 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 g : M → E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ MDiffAt (f - g) z

Tactic:
(hf.hasMFDerivAt.sub hg.hasMFDerivAt).mdifferentiableAt

Premises used: MDifferentiableAt.hasMFDerivAt, HasMFDerivAt.mdifferentiableAt, HasMFDerivAt.sub
-- 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 g : M → E'
hf : MDiff[s] f
hg : MDiff[s] g
⊢ MDiff[s] (f - g)

Tactic:
fun x hx ↦ (hf x hx).sub (hg x hx)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.sub
-- 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 g : M → E'
hf : MDiff f
hg : MDiff g
⊢ MDiff (f - g)

Tactic:
fun x ↦ (hf x).sub (hg x)

Premises used: MDifferentiableAt.sub, 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'
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