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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
y : E
hy : y ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E)
h :
  ∀ (z : H) (hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target),
    writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr ((↑I : H → E) z) = id ((↑I : H → E) z)
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr y = id y

Tactic:
rcases hy with ⟨hyT, ⟨z, rfl⟩⟩

Premises used: 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
z : H
hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target
⊢ z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target

Tactic:
simpa [Set.mem_preimage, I.left_inv] using hyT

Premises used: ModelWithCorners.left_inv, Set.mem_preimage
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
hmem :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target ∩ range (↑I : H → E) ∈
    𝓝[range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q'
z : H
hyT : (↑I : H → E) z ∈ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H q')).target
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr ((↑I : H → E) z) = id ((↑I : H → E) z)

Tactic:
simp [writtenInExtChartAt, extChartAt, ChartedSpace.sum_chartAt_inr,
    Sum.inr_injective.extend_apply <| chartAt H q',
    (chartAt H q').right_inv (by simpa [Set.mem_preimage, I.left_inv] using hyT)]

Premises used: ChartedSpace.sum_chartAt_inr, extChartAt, Sum.inr_injective, chartAt, Function.Injective.extend_apply, writtenInExtChartAt, OpenPartialHomeomorph.right_inv
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ ContinuousWithinAt (Y := M ⊕ M') Sum.inl s q

Tactic:
fun_prop
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
refine :
  HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl) (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
    ((↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I q) : M → E) q)
⊢ HasMFDerivWithinAt I I (M' := M ⊕ M') Sum.inl s q (ContinuousLinearMap.id 𝕜 (TangentSpace I q))

Tactic:
refine ⟨by fun_prop, ?_⟩
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q
      Sum.inl =ᶠ[𝓝[(↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I q) : M → E) q]
    id

Tactic:
have : (writtenInExtChartAt I I q (@Sum.inl M M'))
      =ᶠ[𝓝[(extChartAt I q).symm ⁻¹' s ∩ Set.range I] (extChartAt I q q)] id :=
    writtenInExtChartAt_sumInl_eventuallyEq_id.filter_mono (nhdsWithin_mono _ (fun _y hy ↦ hy.2))
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
this :
  writtenInExtChartAt (M' := M ⊕ M') I I q
      Sum.inl =ᶠ[𝓝[(↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I q) : M → E) q]
    id
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl ((↑(extChartAt I q) : M → E) q) = id ((↑(extChartAt I q) : M → E) q)

Tactic:
simp [writtenInExtChartAt, extChartAt]

Premises used: extChartAt, writtenInExtChartAt
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q : M
this :
  writtenInExtChartAt (M' := M ⊕ M') I I q
      Sum.inl =ᶠ[𝓝[(↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I q) : M → E) q]
    id
⊢ HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q Sum.inl) (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
    ((↑(extChartAt I q).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I q) : M → E) q)

Tactic:
exact (hasFDerivWithinAt_id (extChartAt I q q) _).congr_of_eventuallyEq this
    (by simp [writtenInExtChartAt, extChartAt])

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, extChartAt, PartialEquiv.toFun, 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
q : M
⊢ HasMFDerivAt I I (M' := M ⊕ M') Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
simpa [HasMFDerivAt, hasMFDerivWithinAt_univ] using hasMFDerivWithinAt_inl (s := Set.univ)

Premises used: HasMFDerivAt, hasMFDerivWithinAt_univ, hasMFDerivWithinAt_inl
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
⊢ ContinuousWithinAt (Y := M ⊕ M') Sum.inr t q'

Tactic:
fun_prop
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
refine :
  HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
    ((↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I q') : M' → E) q')
⊢ HasMFDerivWithinAt I I (M' := M ⊕ M') Sum.inr t q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
refine ⟨by fun_prop, ?_⟩
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q'
      Sum.inr =ᶠ[𝓝[(↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q']
    id

Tactic:
have : (writtenInExtChartAt I I q' (@Sum.inr M M'))
      =ᶠ[𝓝[(extChartAt I q').symm ⁻¹' t ∩ Set.range I] (extChartAt I q' q')] id :=
    writtenInExtChartAt_sumInr_eventuallyEq_id.filter_mono (nhdsWithin_mono _ (fun _y hy ↦ hy.2))
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
this :
  writtenInExtChartAt (M' := M ⊕ M') I I q'
      Sum.inr =ᶠ[𝓝[(↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q']
    id
⊢ writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr ((↑(extChartAt I q') : M' → E) q') =
    id ((↑(extChartAt I q') : M' → E) q')

Tactic:
simp [writtenInExtChartAt, extChartAt]

Premises used: extChartAt, writtenInExtChartAt
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
this :
  writtenInExtChartAt (M' := M ⊕ M') I I q'
      Sum.inr =ᶠ[𝓝[(↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)] (↑(extChartAt I q') : M' → E) q']
    id
⊢ HasFDerivWithinAt (writtenInExtChartAt (M' := M ⊕ M') I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
    ((↑(extChartAt I q').symm : E → M') ⁻¹' t ∩ range (↑I : H → E)) ((↑(extChartAt I q') : M' → E) q')

Tactic:
exact (hasFDerivWithinAt_id (extChartAt I q' q') _).congr_of_eventuallyEq this
    (by simp [writtenInExtChartAt, extChartAt])

Premises used: HasFDerivWithinAt.congr_of_eventuallyEq, extChartAt, PartialEquiv.toFun, 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
q' : M'
⊢ HasMFDerivAt I I (M' := M ⊕ M') Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
simpa [HasMFDerivAt, hasMFDerivWithinAt_univ] using hasMFDerivWithinAt_inr (t := Set.univ)

Premises used: hasMFDerivWithinAt_inr, HasMFDerivAt, 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
s : Set M
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
q : M
hU : UniqueMDiffWithinAt I s q
⊢ Eq (α := TangentSpace I q →L[𝕜] TangentSpace I (M := M ⊕ M') (Sum.inl q)) (mfderivWithin I I Sum.inl s q)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
hasMFDerivWithinAt_inl.mfderivWithin hU

Premises used: HasMFDerivWithinAt.mfderivWithin, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, hasMFDerivWithinAt_inl, 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
p : M ⊕ M'
q : M
⊢ Eq (α := TangentSpace I q →L[𝕜] TangentSpace I (M := M ⊕ M') (Sum.inl q)) (mfderiv% Sum.inl q)
    (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
simpa [mfderivWithin_univ] using (mfderivWithin_sumInl (uniqueMDiffWithinAt_univ I))

Premises used: mfderivWithin_sumInl, mfderivWithin_univ, uniqueMDiffWithinAt_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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
t : Set M'
hU : UniqueMDiffWithinAt I t q'
⊢ Eq (α := TangentSpace I q' →L[𝕜] TangentSpace I (M := M ⊕ M') (Sum.inr q')) (mfderivWithin I I Sum.inr t q')
    (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
hasMFDerivWithinAt_inr.mfderivWithin hU

Premises used: hasMFDerivWithinAt_inr, HasMFDerivWithinAt.mfderivWithin, TangentSpace
-- 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
M' : Type u_21
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
q' : M'
⊢ Eq (α := TangentSpace I q' →L[𝕜] TangentSpace I (M := M ⊕ M') (Sum.inr q')) (mfderiv% Sum.inr q')
    (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
simpa [mfderivWithin_univ] using (mfderivWithin_sumInr (uniqueMDiffWithinAt_univ I))

Premises used: mfderivWithin_sumInr, mfderivWithin_univ, uniqueMDiffWithinAt_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
f g : M → E'
f' g' : 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'
hg : HasMFDerivWithinAt I 𝓘(𝕜, E') g s z g'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, E') (f + g) s z (f' + g')

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

Premises used: HasFDerivWithinAt.add, And.right, And.left, And.intro, ContinuousWithinAt.add, 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.add hg.1, hf.2.add hg.2⟩

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

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

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

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

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

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

Premises used: MDifferentiableWithinAt.add, 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
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).add (hg x)

Premises used: MDifferentiableAt.add, 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 f z
hg : MDiffAt g z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z))

Tactic:
exact mfderiv% f z

Premises used: mfderiv, 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 f z
hg : MDiffAt g z
⊢ ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') ((f + g) z))

Tactic:
exact mfderiv% g z

Premises used: mfderiv, 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'
z : M
f g : M → E'
hf : MDiffAt f z
hg : MDiffAt g z
⊢ mfderiv% (f + g) 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)))
      (mfderiv% f z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (f z)))
      (mfderiv% g z :
        ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I z) (TangentSpace 𝓘(𝕜, E') (g z)))

Tactic:
(hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv

Premises used: HasMFDerivAt.add, HasMFDerivAt.mfderiv, MDifferentiableAt.hasMFDerivAt, instModuleTangentSpace._aux_1, TangentSpace, instTopologicalSpaceTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_1, instAddCommGroupTangentSpace._aux_4