awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
p : TangentBundle I M
q : TangentBundle I H
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).target
rw :
  ⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
      (fderivWithin 𝕜
            (writtenInExtChartAt I I (q.proj (E := TangentSpace I))
              (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M))
            (range (↑I : H → E))
            ((↑(extChartAt I (q.proj (E := TangentSpace I))) : H → E) (q.proj (E := TangentSpace I))) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
        (q.snd (E := TangentSpace I))⟩ =
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p) :
            OpenPartialHomeomorph (ModelProd H E) (TangentBundle I M)) :
        ModelProd H E → TangentBundle I M)
      ((TotalSpace.toProd H E : (a : TotalSpace E fun (x : H) ↦ E) → H × E) q : H × E)
⊢ ⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
      (mfderiv% (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M)
            (q.proj (E := TangentSpace I)) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
        (q.snd (E := TangentSpace I))⟩ =
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p) :
            OpenPartialHomeomorph (ModelProd H E) (TangentBundle I M)) :
        ModelProd H E → TangentBundle I M)
      ((TotalSpace.toProd H E : (a : TotalSpace E fun (x : H) ↦ E) → H × E) q : H × E)

Tactic:
rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]

Premises used: MDifferentiableAt.mfderiv, chart_mem_atlas, mdifferentiableAt_atlas_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
x y : M
hsrc : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H y)).source
⊢ MDiffAt (↑(ChartedSpace.chartAt y) : M → H) x

Tactic:
have := mdifferentiableAt_atlas (I := I) (ChartedSpace.chart_mem_atlas _) hsrc
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
x y : M
hsrc : x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H y)).source
this : MDiffAt (↑(ChartedSpace.chartAt y) : M → H) x
⊢ mfderiv% (↑(chartAt H y) : M → H) x = tangentCoordChange I x y x

Tactic:
simp [mfderiv, if_pos this, Function.comp_assoc]

Premises used: mfderiv, if_pos, Function.comp_assoc
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
s : Set M
hs : UniqueMDiffOn I s
⊢ UniqueMDiffOn I.tangent (M := TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I))
    (TotalSpace.proj (E := TangentSpace I) ⁻¹' s)

Tactic:
hs.bundle_preimage _

Premises used: UniqueMDiffOn.bundle_preimage
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
rw :
  Eq (α := E →L[𝕜] E')
    (fderivWithin 𝕜
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
            (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
          (range (↑I' : H' → E'))
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) ∘SL
        ϕ x ∘SL
          VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M)
            (achart H (f x₀)) (achart H (f x)) (f x) :
      E →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
        ϕ x ∘SL
          mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I (f x₀)) : M → E) (f x)) :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜)
        (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
        (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x))))
⊢ inTangentCoordinates I I' f g ϕ x₀ x =
    mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
      ϕ x ∘SL
        mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I (f x₀)) : M → E) (f x))

Tactic:
rw [inTangentCoordinates_eq _ _ _ hx hy, tangentBundleCore_coordChange]

Premises used: inTangentCoordinates_eq, tangentBundleCore_coordChange
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_g :
  Eq (α := E' →L[𝕜] E')
    (fderivWithin 𝕜
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
          (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
        (range (↑I' : H' → E'))
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) :
      E' →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) :
      TangentSpace I' (g x) →L[𝕜] TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x)))
e_f :
  VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
      ((↑(extChartAt I (f x₀)) : M → E) (f x))
⊢ Eq (α := E →L[𝕜] E')
    (fderivWithin 𝕜
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
            (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
          (range (↑I' : H' → E'))
          ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) ∘SL
        ϕ x ∘SL
          VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M)
            (achart H (f x₀)) (achart H (f x)) (f x) :
      E →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) ∘SL
        ϕ x ∘SL
          mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
            ((↑(extChartAt I (f x₀)) : M → E) (f x)) :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜)
        (TangentSpace 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x)))
        (TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x))))

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ MDiffAt (↑(extChartAt I' (g x₀)) : M' → E') (g x)

Tactic:
have : MDiffAt (extChartAt I' (g x₀)) (g x) := mdifferentiableAt_extChartAt hy
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
this : MDiffAt (↑(extChartAt I' (g x₀)) : M' → E') (g x)
⊢ Eq (α := E' →L[𝕜] E')
    (fderivWithin 𝕜
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x₀)) : OpenPartialHomeomorph M' H') I') : M' → E') ∘
          (↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I').symm : E' → M'))
        (range (↑I' : H' → E'))
        ((↑(OpenPartialHomeomorph.extend (↑(achart H' (g x)) : OpenPartialHomeomorph M' H') I') : M' → E') (g x)) :
      E' →L[𝕜] E')
    (mfderiv% (↑(extChartAt I' (g x₀)) : M' → E') (g x) :
      TangentSpace I' (g x) →L[𝕜] TangentSpace 𝓘(𝕜, E') ((↑(extChartAt I' (g x₀)) : M' → E') (g x)))

Tactic:
simp_all [mfderiv]

Premises used: mfderiv
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_f :
  VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    if MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)) then
      fderivWithin 𝕜
        ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
          (↑(extChartAt I (f x₀)).symm : E → M) ∘
            (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
          ((↑(extChartAt I (f x₀)) : M → E) (f x)))
    else 0
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm : E → M) (range (↑I : H → E))
      ((↑(extChartAt I (f x₀)) : M → E) (f x))

Tactic:
simp only [mfderivWithin, writtenInExtChartAt, modelWithCornersSelf_coe, range_id, inter_univ]

Premises used: Set.inter_univ, mfderivWithin, Set.range_id, writtenInExtChartAt, modelWithCornersSelf_coe
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_f :
  VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    fderivWithin 𝕜
      ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
        (↑(extChartAt I (f x₀)).symm : E → M) ∘
          (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
        ((↑(extChartAt I (f x₀)) : M → E) (f x)))
e_f₁ : MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x))
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    if MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)) then
      fderivWithin 𝕜
        ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
          (↑(extChartAt I (f x₀)).symm : E → M) ∘
            (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
        ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
          ((↑(extChartAt I (f x₀)) : M → E) (f x)))
    else 0

Tactic:
rw [if_pos]

Premises used: if_pos
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ VectorBundleCore.coordChange (ι := (↑(atlas H M) : Type (max u_3 u_4))) (tangentBundleCore I M) (achart H (f x₀))
      (achart H (f x)) (f x) =
    fderivWithin 𝕜
      ((↑(extChartAt I ((↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x)))) : M → E) ∘
        (↑(extChartAt I (f x₀)).symm : E → M) ∘
          (↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))).symm : E → E) ⁻¹' range (↑I : H → E))
      ((↑(extChartAt 𝓘(𝕜, E) ((↑(extChartAt I (f x₀)) : M → E) (f x))) : E → E)
        ((↑(extChartAt I (f x₀)) : M → E) (f x)))

Tactic:
simp [Function.comp_def, OpenPartialHomeomorph.left_inv (chartAt H (f x₀)) hx]

Premises used: chartAt, OpenPartialHomeomorph.left_inv, Function.comp_def
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_f : (↑(extChartAt I (f x₀)) : M → E) (f x) ∈ (extChartAt I (f x₀)).target
⊢ MDiffAt[range (↑I : H → E)] (↑(extChartAt I (f x₀)).symm : E → M) ((↑(extChartAt I (f x₀)) : M → E) (f x))

Tactic:
apply mdifferentiableWithinAt_extChartAt_symm

Premises used: mdifferentiableWithinAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
e_f : f x ∈ (extChartAt I (f x₀)).source
⊢ (↑(extChartAt I (f x₀)) : M → E) (f x) ∈ (extChartAt I (f x₀)).target

Tactic:
apply (extChartAt I (f x₀)).map_source

Premises used: extChartAt, PartialEquiv.map_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
inst_6 : IsManifold I 1 M
E' : Type u_5
inst_7 : NormedAddCommGroup E'
inst_8 : NormedSpace 𝕜 E'
H' : Type u_6
inst_9 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_10 : TopologicalSpace M'
inst_11 : ChartedSpace H' M'
inst_12 : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (f x)) (TangentSpace I' (g x))
x₀ x : N
hx : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (f x₀))).source
hy : g x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (g x₀))).source
⊢ f x ∈ (extChartAt I (f x₀)).source

Tactic:
simpa using hx
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
⊢ UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x

Tactic:
have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds (I := I') (f x))
-- Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
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'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivWithinAt I I' f s x f'
hd : DenseRange.{u_5, u_2} (X := E') (α := E) (⇑f' : (a : E) → E')
this : UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
⊢ UniqueMDiffWithinAt I' (f '' s) (f x)

Tactic:
(((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt

Premises used: UniqueMDiffWithinAt, UniqueDiffWithinAt.congr_pt, HasFDerivWithinAt.uniqueDiffWithinAt, And.right, UniqueDiffWithinAt.mono, HasFDerivWithinAt.mono