awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
f g : M → 𝕜
x : M
hf : MDiffAt f x
hg : MDiffAt g x
v : TangentSpace I x
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((↑(NormedSpace.fromTangentSpace ((f • g) x)) : TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x) →L[𝕜] 𝕜) ∘SL
            HAdd.hAdd (β :=
              ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)))
              (HSMul.hSMul (β :=
                ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                  (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)))
                (f x)
                ((↑(ContinuousLinearEquiv.symm (NormedSpace.fromTangentSpace ((f • g) x))) :
                    𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x)) ∘SL
                  (↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, 𝕜) (g x) →L[𝕜] 𝕜) ∘SL mfderiv% g x))
              (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
                  (ContinuousLinearMap.toSpanSingleton 𝕜
                      ((ContinuousLinearEquiv.symm (NormedSpace.fromTangentSpace ((f • g) x)) :
                          (a : 𝕜) → TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))
                        (g x)) :
                    𝕜 →L[𝕜] TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))
                  (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := TangentSpace 𝓘(𝕜, 𝕜) (f x))
                      (↑(NormedSpace.fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) (mfderiv% f x) :
                    ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x)
                  (TangentSpace 𝓘(𝕜, 𝕜) ((f • g) x))) :
          (a : TangentSpace I x) → 𝕜)
        v :
      𝕜)
    ((HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (f x)
              ((↑(NormedSpace.fromTangentSpace (g x)) : TangentSpace 𝓘(𝕜, 𝕜) (g x) →L[𝕜] 𝕜) ∘SL mfderiv% g x) +
            HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (TangentSpace I x) 𝕜) (g x)
              ((↑(NormedSpace.fromTangentSpace (f x)) : TangentSpace 𝓘(𝕜, 𝕜) (f x) →L[𝕜] 𝕜) ∘SL mfderiv% f x) :
          (a : TangentSpace I x) → 𝕜)
        v :
      𝕜)

Tactic:
simp [mul_comm _ (g x)]

Premises used: mul_comm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ MDiffAt 0 x

Tactic:
mdifferentiable_const ..

Premises used: mdifferentiable_const
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ MDiffAt 0 x

Tactic:
exact mdifferentiable_const ..

Premises used: mdifferentiable_const
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    (d% (HAdd.hAdd (α := M → F) 0 0) x) (d% 0 x)
⊢ HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) (d% 0 x) =
    d% 0 x

Tactic:
rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]

Premises used: mvfderiv_add
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F)
    (d% (HAdd.hAdd (α := M → F) 0 0) x) (d% 0 x)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
⊢ HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) (d% 0 x) =
    d% 0 x

Tactic:
have : d% (0 : M → F) x + d% (0 : M → F) x = d% (0 : M → F) x := by
    rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
    simp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
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
F : Type u_8
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
x : M
this :
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) (d% 0 x) =
    d% 0 x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_8} (RingHom.id 𝕜) (TangentSpace I x) F) (d% 0 x) 0

Tactic:
simpa using this
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
s : Set E
x : E
⊢ HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (M' := E') (⇑f : (a : E) → E') s x f

Tactic:
f.hasFDerivWithinAt.hasMFDerivWithinAt

Premises used: ContinuousLinearMap.hasFDerivWithinAt, HasFDerivWithinAt.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
x : E
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') (M' := E') (⇑f : (a : E) → E') x f

Tactic:
f.hasFDerivAt.hasMFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
s : Set E
x : E
⊢ MDiffAt[s] (⇑f : (a : E) → E') x

Tactic:
f.differentiableWithinAt.mdifferentiableWithinAt

Premises used: DifferentiableWithinAt.mdifferentiableWithinAt, ContinuousLinearMap.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
s : Set E
⊢ MDiff[s] (⇑f : (a : E) → E')

Tactic:
f.differentiableOn.mdifferentiableOn

Premises used: DifferentiableOn.mdifferentiableOn, ContinuousLinearMap.differentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
x : E
⊢ MDiffAt (⇑f : (a : E) → E') x

Tactic:
f.differentiableAt.mdifferentiableAt

Premises used: ContinuousLinearMap.differentiableAt, DifferentiableAt.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
⊢ MDiff (⇑f : (a : E) → E')

Tactic:
f.differentiable.mdifferentiable

Premises used: ContinuousLinearMap.differentiable, Differentiable.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
x : E
⊢ mfderiv% (⇑f : (a : E) → E') x = f

Tactic:
f.hasMFDerivAt.mfderiv

Premises used: HasMFDerivAt.mfderiv, ContinuousLinearMap.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E →L[𝕜] E'
s : Set E
x : E
hs : UniqueMDiffWithinAt 𝓘(𝕜, E) s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f : (a : E) → E') s x = f

Tactic:
f.hasMFDerivWithinAt.mfderivWithin hs

Premises used: HasMFDerivWithinAt.mfderivWithin, ContinuousLinearMap.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
s : Set E
x : E
⊢ HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') (M' := E') (⇑f : (a : E) → E') s x (↑f : E →L[𝕜] E')

Tactic:
f.hasFDerivWithinAt.hasMFDerivWithinAt

Premises used: ContinuousLinearEquiv.hasFDerivWithinAt, HasFDerivWithinAt.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
x : E
⊢ HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') (M' := E') (⇑f : (a : E) → E') x (↑f : E →L[𝕜] E')

Tactic:
f.hasFDerivAt.hasMFDerivAt

Premises used: HasFDerivAt.hasMFDerivAt, ContinuousLinearEquiv.hasFDerivAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
s : Set E
x : E
⊢ MDiffAt[s] (⇑f : (a : E) → E') x

Tactic:
f.differentiableWithinAt.mdifferentiableWithinAt

Premises used: DifferentiableWithinAt.mdifferentiableWithinAt, ContinuousLinearEquiv.differentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
s : Set E
⊢ MDiff[s] (⇑f : (a : E) → E')

Tactic:
f.differentiableOn.mdifferentiableOn

Premises used: DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.differentiableOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
x : E
⊢ MDiffAt (⇑f : (a : E) → E') x

Tactic:
f.differentiableAt.mdifferentiableAt

Premises used: ContinuousLinearEquiv.differentiableAt, DifferentiableAt.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
⊢ MDiff (⇑f : (a : E) → E')

Tactic:
f.differentiable.mdifferentiable

Premises used: ContinuousLinearEquiv.differentiable, Differentiable.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
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
x : E
⊢ mfderiv% (⇑f : (a : E) → E') x = (↑f : E →L[𝕜] E')

Tactic:
f.hasMFDerivAt.mfderiv

Premises used: HasMFDerivAt.mfderiv, ContinuousLinearEquiv.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_5
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
f : E ≃L[𝕜] E'
s : Set E
x : E
hs : UniqueMDiffWithinAt 𝓘(𝕜, E) s x
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') (⇑f : (a : E) → E') s x = (↑f : E →L[𝕜] E')

Tactic:
f.hasMFDerivWithinAt.mfderivWithin hs

Premises used: ContinuousLinearEquiv.hasMFDerivWithinAt, HasMFDerivWithinAt.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
x : M
⊢ HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
⟨continuousAt_id, ?_⟩

Premises used: HasMFDerivAt, And.intro, continuousAt_id
-- 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
x : M
refine :
  HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
⊢ HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
refine ⟨continuousAt_id, ?_⟩
-- 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
x : M
apply :
  (extChartAt I x).target ⊆
    {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1}
⊢ ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y

Tactic:
apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)

Premises used: extChartAt_target_mem_nhdsWithin, Filter.mem_of_superset
-- 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
x : M
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (extChartAt I x).target →
      Membership.mem (γ := Set E)
        {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1} my_y
mfld_set_tac₃ mfld_set_tac₄ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target →
      Membership.mem (γ := Set E)
        {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1} my_y
⊢ (extChartAt I x).target ⊆
    {x_1 : E | (fun (y : E) ↦ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y) x_1}

Tactic:
mfld_set_tac
-- 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
x : M
⊢ ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y

Tactic:
have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
    apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
    mfld_set_tac
-- 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
x : M
this :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y
apply :
  ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x) =
    id ((↑(extChartAt I x) : M → E) x)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq (hasFDerivWithinAt_id _ _) this

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, hasFDerivWithinAt_id
-- 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
x : M
this :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) y = y
⊢ ((↑(extChartAt I x) : M → E) ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x) =
    id ((↑(extChartAt I x) : M → E) x)

Tactic:
simp only [mfld_simps]
-- 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
x : M
⊢ HasMFDerivWithinAt I I id s x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
(hasMFDerivAt_id x).hasMFDerivWithinAt

Premises used: hasMFDerivAt_id, HasMFDerivAt.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
x : M
⊢ MDiffAt id x

Tactic:
(hasMFDerivAt_id x).mdifferentiableAt

Premises used: hasMFDerivAt_id, 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
s : Set M
x : M
⊢ MDiffAt[s] id x

Tactic:
mdifferentiableAt_id.mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, mdifferentiableAt_id
-- 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
⊢ MDiff id

Tactic:
fun _ ↦ mdifferentiableAt_id

Premises used: mdifferentiableAt_id, 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
s : Set M
⊢ MDiff[s] id

Tactic:
mdifferentiable_id.mdifferentiableOn

Premises used: mdifferentiable_id, MDifferentiable.mdifferentiableOn
-- 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
x : M
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
(hasMFDerivAt_id x).mfderiv

Premises used: HasMFDerivAt.mfderiv, hasMFDerivAt_id
-- 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
x : M
hxs : UniqueMDiffWithinAt I s x
rw :
  Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderivWithin I I id s x)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]

Premises used: MDifferentiable.mfderivWithin, mdifferentiableAt_id
-- 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
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
mfderiv_id

Premises used: mfderiv_id
-- 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
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ Eq (α := TangentSpace I x →L[𝕜] TangentSpace I (id x)) (mfderiv% id x) (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
exact mfderiv_id

Premises used: mfderiv_id
-- 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
h : ∀ (x : M) (v : TangentSpace I x), tangentMap I I id ⟨x, v⟩ = id ⟨x, v⟩
⊢ Eq (α := TangentBundle I M → TangentBundle I M) (tangentMap I I id) id

Tactic:
ext1 ⟨x, v⟩
-- 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
x : M
v : TangentSpace I x
⊢ tangentMap I I id ⟨x, v⟩ = id ⟨x, v⟩

Tactic:
simp [tangentMap]

Premises used: tangentMap