awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hs : HasMFDerivWithinAt I I' f s x f'
ht : HasMFDerivWithinAt I I' f t x f'
left : ContinuousWithinAt f (s ∪ t) x
⊢ HasMFDerivWithinAt I I' f (s ∪ t) x f'
have right : HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∪ t) ∩ range (↑I : H → E))
  ((↑(extChartAt I x) : M → E) x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s t : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
hs : HasMFDerivWithinAt I I' f s x f'
ht : HasMFDerivWithinAt I I' f t x f'
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∪ t) ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have h : (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∪ t) ∩ range (↑I : H → E) =
  (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∪
    (↑(extChartAt I x).symm : E → M) ⁻¹' t ∩ range (↑I : H → E)
Tactic: convert! HasFDerivWithinAt.union hs.2 ht.2 using 1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hs : s ∈ 𝓝 x
⊢ HasMFDerivAt I I' f x f'
have rwa : ∀ (h : HasMFDerivWithinAt I I' f (univ ∩ s) x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
Tactic: rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hs : s ∈ 𝓝 x
rwa : ∀ (h : HasMFDerivWithinAt I I' f (univ ∩ s) x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
⊢ HasMFDerivAt I I' f x f'
have rwa₁ : ∀ (h : HasMFDerivWithinAt I I' f univ x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
Tactic: rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hs : s ∈ 𝓝 x
rwa : ∀ (h : HasMFDerivWithinAt I I' f (univ ∩ s) x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
rwa₁ : ∀ (h : HasMFDerivWithinAt I I' f univ x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
⊢ HasMFDerivAt I I' f x f'
have rwa₂ : ∀ (h : HasMFDerivAt I I' f x f') (hs : s ∈ 𝓝 x), HasMFDerivAt I I' f x f'
Tactic: rwa [← univ_inter s, hasMFDerivWithinAt_inter hs, hasMFDerivWithinAt_univ] at h
Cleared hypotheses: h, hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)
have refine : HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderivWithin I I' f s x)
  ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨h.1, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderivWithin I I' f s x)
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have simp : HasFDerivWithinAt
  (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
    f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
  (fderivWithin 𝕜
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
  ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: simp only [mfderivWithin, h, if_pos, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
⊢ MDifferentiableWithinAt I I' f s x ↔
    ∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
      HasMFDerivWithinAt I I' f s x f'
have refine : (∃ (f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))),
    HasMFDerivWithinAt I I' f s x f') →
  MDifferentiableWithinAt I I' f s x
Tactic: refine ⟨fun h ↦ ⟨mfderivWithin I I' f s x, h.hasMFDerivWithinAt⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ HasMFDerivAt I I' f x (mfderiv I I' f x)
have refine : HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderiv I I' f x) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨h.continuousAt, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderiv I I' f x) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
have simp : HasFDerivWithinAt
  (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
    f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
  (fderivWithin 𝕜
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
  (range (↑I : H → E)) ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: simp only [mfderiv, h, if_pos, mfld_simps]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
⊢ mfderivWithin I I' f s x = f'
have h₁ : ∀ (x_1 : TangentSpace I x),
  Eq.{u_5 + 1} (α := TangentSpace I' (f x))
    (((mfderivWithin I I' f s x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
          (a : TangentSpace I x) → TangentSpace I' (f x))
        x_1 :
      TangentSpace I' (f x))
    ((f' : (a : TangentSpace I x) → TangentSpace I' (f x)) x_1 : TangentSpace I' (f x))
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
x_1 : TangentSpace I x
⊢ Eq.{u_5 + 1} (α := TangentSpace I' (f x))
    (((mfderivWithin I I' f s x :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
          (a : TangentSpace I x) → TangentSpace I' (f x))
        x_1 :
      TangentSpace I' (f x))
    ((f' : (a : TangentSpace I x) → TangentSpace I' (f x)) x_1 : TangentSpace I' (f x))
have h₁ : Eq.{u_5 + 1} (α := TangentSpace I' (f x))
  (((mfderivWithin I I' f s x :
          ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
        (a : TangentSpace I x) → TangentSpace I' (f x))
      x_1 :
    TangentSpace I' (f x))
  (((mfderivWithin I I' f s x :
          ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))) :
        (a : TangentSpace I x) → TangentSpace I' (f x))
      x_1 :
    TangentSpace I' (f x))
Tactic: rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
h : HasMFDerivWithinAt I I' f s x 0
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f s x) 0
have simp : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (fderivWithin 𝕜
    (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
      f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
  0
Tactic: simp only [mfld_simps, mfderivWithin, h.mdifferentiableWithinAt, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
h :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      0 ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (fderivWithin 𝕜
      (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
        f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)))
    0
have hc : HasFDerivWithinAt.{u_1, u_2, u_5} (𝕜 := 𝕜)
  (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘
    f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H))
  0 ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ∘ (↑I.symm : E → H) ⁻¹' s ∩ range (↑I : H → E))
  ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: rw [fderivWithin, if_pos]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s : Set M
h : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (_root_.mfderivWithin I I' f s x) (mfderiv I I' f x)
have apply : HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)
Tactic: apply HasMFDerivWithinAt.mfderivWithin _ hxs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f (s ∩ t) x) (mfderivWithin I I' f s x)
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableWithinAt I I' f (s ∩ t) x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (mfderivWithin I I' f s x)
Tactic: rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (mfderivWithin I I' f s x)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f (s ∩ t) x) (mfderivWithin I I' f s x)
have rw₁ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableWithinAt I I' f (s ∩ t) x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (if MDifferentiableWithinAt I I' f s x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
Tactic: rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (mfderivWithin I I' f s x)
rw₁ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (if MDifferentiableWithinAt I I' f s x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' 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 I' (f x)))
    (mfderivWithin I I' f (s ∩ t) x) (mfderivWithin I I' f s x)
have rw₂ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableWithinAt I I' f (s ∩ t) x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f)
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t)
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (if MDifferentiableWithinAt I I' f s x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
Tactic: rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]