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
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)
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)
⊢ 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 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)]
-- 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 : 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) (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 s x) (mfderivWithin I I' f univ x)
Tactic: rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter 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
s : Set M
h : s ∈ 𝓝 x
rw :
  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 univ 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) (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 ∩ s) x) (mfderivWithin I I' f univ x)
Tactic: rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter 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
s : Set M
h : s ∈ 𝓝 x
rw :
  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 univ x)
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 ∩ s) x) (mfderivWithin I I' f univ 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) (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, ← univ_inter s, mfderivWithin_inter h]
-- 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 : 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))
y : M
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'
have this : T1Space M
Tactic: have : T1Space M := I.t1Space M
-- 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))
y : M
this : T1Space M
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'
have refine : ∀ (hf : HasMFDerivWithinAt I I' f s x f'), HasMFDerivWithinAt I I' f (insert y s) x f'
Tactic: refine ⟨fun h => h.mono <| subset_insert y s, fun hf ↦ ?_⟩
-- 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))
y : M
this : T1Space M
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I' f (insert y s) x f'
have inl : HasMFDerivWithinAt I I' f (insert x s) x f'
Tactic: rcases eq_or_ne x y with rfl | h
Cleared hypotheses: 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 : 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))
y : M
this : T1Space M
hf : HasMFDerivWithinAt I I' f s x f'
inl : HasMFDerivWithinAt I I' f (insert x s) x f'
⊢ HasMFDerivWithinAt I I' f (insert y s) x f'
have inr : ∀ (h : x ≠ y), HasMFDerivWithinAt I I' f (insert y s) x f'
Tactic: rcases eq_or_ne x y with rfl | h
-- 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 : 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))
this : T1Space M
hf : HasMFDerivWithinAt I I' f s x f'
⊢ HasMFDerivWithinAt I I' f (insert x s) x f'
have hf₁ : ContinuousWithinAt f s x ∧
  HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
Tactic: rw [HasMFDerivWithinAt] at hf ⊢
Cleared hypotheses: hf
-- 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))
this : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt f (insert x s) x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
      ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have inl : HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
  ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
Tactic: refine ⟨hf.1.insert, ?_⟩
-- 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 : 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))
this : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have this₁ : (extChartAt I x).target ∈
  𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
Tactic: have : (extChartAt I x).target ∈
        𝓝[(extChartAt I x).symm ⁻¹' insert x s ∩ range I] (extChartAt I x) x :=
      nhdsWithin_mono _ inter_subset_right (extChartAt_target_mem_nhdsWithin 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 : 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
have inl : HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
  ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target)
  ((↑(extChartAt I x) : M → E) x)
Tactic: rw [← hasFDerivWithinAt_inter' this]
-- 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ HasFDerivWithinAt (writtenInExtChartAt I I' x f) f'
    ((↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target)
    ((↑(extChartAt I x) : M → E) x)
have inl : (↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E) ∩ (extChartAt I x).target ⊆
  insert ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
Tactic: apply hf.2.insert.mono
-- 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
hz : z ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' insert x s
h2z : z ∈ range (↑I : H → E)
⊢ z ∈ insert ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
have inl : ∀ (hz : (↑(extChartAt I x).symm : E → M) z = x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s)
  (h2z : ∃ (y : H), (↑I : H → E) y = z),
  z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
Tactic: simp only [mem_inter_iff, mem_preimage, mem_insert_iff, mem_range] at hz h2z ⊢
Cleared hypotheses: hz, h2z
-- 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
hz : (↑(extChartAt I x).symm : E → M) z = x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s
h2z : ∃ (y : H), (↑I : H → E) y = z
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
have inl : ∀ (xz : (↑(extChartAt I x).symm : E → M) z = x),
  z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
Tactic: rcases hz with xz | h'z
Cleared hypotheses: hz
-- 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
hz : (↑(extChartAt I x).symm : E → M) z = x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s
h2z : ∃ (y : H), (↑I : H → E) y = z
inl :
  ∀ (xz : (↑(extChartAt I x).symm : E → M) z = x),
    z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
have inl₁ : ∀ (h'z : (↑(extChartAt I x).symm : E → M) z ∈ s),
  z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
Tactic: rcases hz with xz | h'z
Cleared hypotheses: hz
-- 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
⊢ z = (↑(extChartAt I x) : M → E) x ∨ (↑(extChartAt I x).symm : E → M) z ∈ s ∧ ∃ (y : H), (↑I : H → E) y = z
have inl : z = (↑(extChartAt I x) : M → E) x
Tactic: left
-- 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 : 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))
this_1 : T1Space M
hf :
  ContinuousWithinAt f s x ∧
    HasFDerivWithinAt (writtenInExtChartAt I I' x f) f' ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
this :
  (extChartAt I x).target ∈
    𝓝[(↑(extChartAt I x).symm : E → M) ⁻¹' insert x s ∩ range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
z : E
h'z : z ∈ (extChartAt I x).target
h2z : ∃ (y : H), (↑I : H → E) y = z
xz : (↑(extChartAt I x).symm : E → M) z = x
⊢ z = (↑(extChartAt I x) : M → E) x
have this₁ : x ∈ (extChartAt I x).source
Tactic: have : x ∈ (extChartAt I x).source := mem_extChartAt_source x