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 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'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h₂ :
  writtenInExtChartAt I I' x
      f₁ =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    writtenInExtChartAt I I' x f
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f₁) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
have hx₁ : writtenInExtChartAt I I' x f₁ ((↑(extChartAt I x) : M → E) x) =
  writtenInExtChartAt I I' x f ((↑(extChartAt I x) : M → E) x)
Tactic: apply HasFDerivWithinAt.congr_of_eventuallyEq h.2
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (hypothesis)
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 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'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ writtenInExtChartAt I I' x
      f₁ =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    writtenInExtChartAt I I' x f
have this : (↑(extChartAt I x).symm : E → M) ⁻¹' {y : M | f₁ y = f y} ∈
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: have :
      (extChartAt I x).symm ⁻¹' {y | f₁ y = f y} ∈
        𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] (extChartAt I x) x :=
      extChartAt_preimage_mem_nhdsWithin h₁
-- 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 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'
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
this :
  (↑(extChartAt I x).symm : E → M) ⁻¹' {y : M | f₁ y = f y} ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ writtenInExtChartAt I I' x
      f₁ =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    writtenInExtChartAt I I' x f
have apply : ∀ y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' {y : M | f₁ y = f y},
  Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ writtenInExtChartAt I I' x f₁ x_2 = writtenInExtChartAt I I' x f x_2) x_1} y
Tactic: apply Filter.mem_of_superset this fun y => _
-- 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 f₁ : M → M'
x : M
f' : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x))
h : HasMFDerivAt I I' f x f'
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasMFDerivAt I I' f₁ x f'
have rw : ∀ (h : HasMFDerivWithinAt I I' f univ x f') (h₁ : f₁ =ᶠ[𝓝 x] f), HasMFDerivWithinAt I I' f₁ univ x f'
Tactic: rw [← hasMFDerivWithinAt_univ] at h ⊢
Cleared hypotheses: h, h₁
-- 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 f₁ : M → M'
x : 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 univ x f'
h₁ : f₁ =ᶠ[𝓝 x] f
⊢ HasMFDerivWithinAt I I' f₁ univ x f'
have apply : f₁ =ᶠ[𝓝[univ] x] f
Tactic: apply h.congr_of_eventuallyEq _ (mem_of_mem_nhds h₁ :)
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f 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 x) (mfderivWithin I I' f s x)
have pos : ∀ (h : MDifferentiableWithinAt 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 x) (mfderivWithin I I' f s x)
Tactic: by_cases h : MDifferentiableWithinAt I I' f s x
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
pos :
  ∀ (h : MDifferentiableWithinAt 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 x) (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 x) (mfderivWithin I I' f s x)
have neg : ∀ (h : ¬MDifferentiableWithinAt 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 x) (mfderivWithin I I' f s x)
Tactic: by_cases h : MDifferentiableWithinAt I I' f s x
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f s x
⊢ 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 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)
    (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)
have pos : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
  (fderivWithin 𝕜 ((↑(extChartAt I' (f₁ x)) : M' → E') ∘ f₁ ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
  (fderivWithin 𝕜 ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
Tactic: simp only [h, (hL.mdifferentiableWithinAt_iff hx).1 h, ↓reduceIte, writtenInExtChartAt]
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f s x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
    (fderivWithin 𝕜 ((↑(extChartAt I' (f₁ x)) : M' → E') ∘ f₁ ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (fderivWithin 𝕜 ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
have pos : (↑(extChartAt I' (f₁ x)) : M' → E') ∘
    f₁ ∘
      (↑(extChartAt I x).symm :
        E → M) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
  (↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)
Tactic: apply Filter.EventuallyEq.fderivWithin_eq
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f s x
pos :
  (↑(extChartAt I' (f₁ x)) : M' → E') ∘
      f₁ ∘
        (↑(extChartAt I x).symm :
          E → M) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
    (fderivWithin 𝕜 ((↑(extChartAt I' (f₁ x)) : M' → E') ∘ f₁ ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
    (fderivWithin 𝕜 ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x))
have pos₁ : ((↑(extChartAt I' (f₁ x)) : M' → E') ∘ f₁ ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x) =
  ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x)
Tactic: apply Filter.EventuallyEq.fderivWithin_eq
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f s x
⊢ (↑(extChartAt I' (f₁ x)) : M' → E') ∘
      f₁ ∘
        (↑(extChartAt I x).symm :
          E → M) =ᶠ[𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x]
    (↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)
have h₁ : ∀ (y : E) (hy : y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' {x : M | f₁ x = f x}),
  ((↑(extChartAt I' (f₁ x)) : M' → E') ∘ f₁ ∘ (↑(extChartAt I x).symm : E → M)) y =
    ((↑(extChartAt I' (f x)) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M)) y
Tactic: filter_upwards [extChartAt_preimage_mem_nhdsWithin (I := I) hL] with y hy
-- 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 f₁ : M → M'
x : M
s : Set M
hL : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : ¬MDifferentiableWithinAt I I' f s x
⊢ 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 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)
    (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)
have neg : ¬MDifferentiableWithinAt I I' f₁ s x
Tactic: rw [if_neg h, if_neg]
-- 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 f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj (E := TangentSpace I) ∈ s
⊢ Eq (α := TangentBundle I' M') (tangentMapWithin I I' f s p) (tangentMapWithin I I' f₁ s p)
have refine : HEq (α := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f s p)))
  (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f s p)) (β :=
  TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
  (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))
Tactic: refine TotalSpace.ext (h p.1 hp) ?_
-- 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 f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj (E := TangentSpace I) ∈ s
⊢ HEq (α := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f s p)) (β :=
    TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))
have rw : HEq (α :=
  TangentSpace I'
    (TotalSpace.proj (F := E') (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I))))))
  (TotalSpace.snd (E := TangentSpace I')
    (TotalSpace.mk (E := TangentSpace I') (f (p.proj (E := TangentSpace I)))
      (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
            ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
              (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
          (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
        (p.snd (E := TangentSpace I)))))
  (β := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
  (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))
Tactic: rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr h (h _ hp)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (hypothesis)
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 f₁ : M → M'
x : M
hL : f₁ =ᶠ[𝓝 x] f
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
    (mfderiv I I' f₁ x) (mfderiv I I' f x)
have A : f₁ x = f x
Tactic: have A : f₁ x = f x := (mem_of_mem_nhds hL :)
-- 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 f₁ : M → M'
x : M
hL : f₁ =ᶠ[𝓝 x] f
A : f₁ x = f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
    (mfderiv I I' f₁ x) (mfderiv I I' f x)
have rw : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
  (mfderivWithin I I' f₁ univ x) (mfderivWithin I I' f univ x)
Tactic: rw [← mfderivWithin_univ, ← mfderivWithin_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (hypothesis)
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 f₁ : M → M'
x : M
hL : f₁ =ᶠ[𝓝 x] f
A : f₁ x = f x
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f₁ x)))
    (mfderivWithin I I' f₁ univ x) (mfderivWithin I I' f univ x)
have hL₁ : f₁ =ᶠ[𝓝[univ] x] f
Tactic: rw [← nhdsWithin_univ] at hL
Cleared hypotheses: hL, A
-- 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 x' : M
h : x = x'
⊢ Eq (α := E →L[𝕜] E')
    (mfderiv I I' f x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderiv I I' f x')
have subst : Eq (α := E →L[𝕜] E')
  (mfderiv I I' f x :
    ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (mfderiv I I' f x)
Tactic: subst h
Cleared hypotheses: x', h
-- 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
f' : M → M'
h : f = f'
⊢ Eq (α := E →L[𝕜] E')
    (mfderiv I I' f x :
      ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderiv I I' f' x)
have subst : Eq (α := E →L[𝕜] E')
  (mfderiv I I' f x :
    ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (mfderiv I I' f x)
Tactic: subst h
Cleared hypotheses: f', h