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 : Set M
cont :
  ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f s x ∧
      DifferentiableWithinAtProp I I'
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    (ContinuousWithinAt f s x ∧ ContinuousWithinAt ((↑(extChartAt I' (f x)) : M' → E') ∘ f) s x) ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        ((↑(chartAt E' (((↑(extChartAt I' (f x)) : M' → E') ∘ f) x)) : E' → E') ∘
          ((↑(extChartAt I' (f x)) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
have simp_rw : ContinuousWithinAt f s x ∧
    DifferentiableWithinAt 𝕜
      ((↑I' : H' → E') ∘
        ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
          (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x)) ↔
  ContinuousWithinAt f s x ∧
    DifferentiableWithinAt 𝕜
      (id ∘
        (id ∘
            (((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H')) ∘ f) ∘
              (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘
          (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
Tactic: simp_rw [cont, DifferentiableWithinAtProp, extChartAt, OpenPartialHomeomorph.extend,
    PartialEquiv.coe_trans,
    ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
    chartAt_self_eq, OpenPartialHomeomorph.refl_apply]
-- 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
⊢ MDifferentiableAt I I' f x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw : MDifferentiableWithinAt I I' f univ x ↔
  ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
Tactic: rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
    mdifferentiableWithinAt_iff_target, continuousWithinAt_univ]
-- 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
rw :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
⊢ MDifferentiableAt I I' f x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw₁ : MDifferentiableWithinAt I I' f univ x ↔
  ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
Tactic: rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
    mdifferentiableWithinAt_iff_target, continuousWithinAt_univ]
-- 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
rw :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
rw₁ :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
⊢ MDifferentiableAt I I' f x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw₂ : ContinuousWithinAt f univ x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x ↔
  ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
Tactic: rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
    mdifferentiableWithinAt_iff_target, continuousWithinAt_univ]
-- 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
rw :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
rw₁ :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
rw₂ :
  ContinuousWithinAt f univ x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
⊢ MDifferentiableAt I I' f x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) x
have rw₃ : ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x ↔
  ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' (f x)) : M' → E') ∘ f) univ x
Tactic: rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ,
    mdifferentiableWithinAt_iff_target, continuousWithinAt_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 : M → M'
x : M
s : Set M
e : OpenPartialHomeomorph M H
inst_11 : IsManifold I 1 M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
hx h2x : x ∈ e.source
⊢ MDifferentiableWithinAt I I' f s x ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(e.extend I).symm : E → M))
      ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x)
have h2x₁ : x ∈ (e.extend I).source
Tactic: rw [← e.extend_source (I := I)] at h2x
Cleared hypotheses: h2x
-- 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
e : OpenPartialHomeomorph M H
inst_11 : IsManifold I 1 M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ MDifferentiableWithinAt I I' f s x ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(e.extend I).symm : E → M))
      ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x)
have simp_rw : ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
    DifferentiableWithinAt 𝕜
      ((↑I' : H' → E') ∘ ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : M → H) x)) ↔
  ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
    DifferentiableWithinAt 𝕜 ((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(e.extend I).symm : E → M))
      ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x)
Tactic: simp_rw [MDifferentiableWithinAt,
    differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_source he hx,
    StructureGroupoid.liftPropWithinAt_self_source,
    e.extend_symm_continuousWithinAt_comp_right_iff, differentiableWithinAtProp_self_source,
    DifferentiableWithinAtProp, Function.comp, e.left_inv hx, (e.extend I).left_inv h2x]
-- 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
inst_11 : IsManifold I 1 M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ MDifferentiableAt I I' f x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
have simp_rw : MDifferentiableWithinAt I I' f univ x' ↔
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x')
Tactic: simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx',
    preimage_univ, univ_inter]
-- 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
inst_11 : IsManifold I 1 M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
simp_rw :
  MDifferentiableWithinAt I I' f univ x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
⊢ MDifferentiableAt I I' f x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
have simp_rw₁ : MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x')
Tactic: simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx',
    preimage_univ, univ_inter]
-- 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
inst_11 : IsManifold I 1 M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
simp_rw :
  MDifferentiableWithinAt I I' f univ x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
simp_rw₁ :
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
⊢ MDifferentiableAt I I' f x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
have simp_rw₂ : MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (univ ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x') ↔
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x')
Tactic: simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx',
    preimage_univ, univ_inter]
-- 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'
s : Set M
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔
    ContinuousWithinAt f s x ∧
      LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x
have rw : ContinuousWithinAt f s x →
  (LiftPropWithinAt (DifferentiableWithinAtProp I I') ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x)
Tactic: rw [differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_target
      (chart_mem_maximalAtlas y) hy,
    and_congr_right]
-- 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'
s : Set M
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x
have simp_rw : ContinuousWithinAt ((↑(chartAt H' y) : M' → H') ∘ f) s x ∧
    DifferentiableWithinAtProp I I'
      (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
  ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
    DifferentiableWithinAtProp I 𝓘(𝕜, E')
      (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [StructureGroupoid.liftPropWithinAt_self_target]
-- 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'
s : Set M
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt ((↑(chartAt H' y) : M' → H') ∘ f) s x ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
have simp_rw : True ∧
    DifferentiableWithinAtProp I I'
      (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
  ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
    DifferentiableWithinAtProp I 𝓘(𝕜, E')
      (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]
-- 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'
s : Set M
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
⊢ True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
have hy₁ : f x ∈ (extChartAt I' y).source
Tactic: rw [← extChartAt_source I'] at hy
Cleared hypotheses: hy, 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'
s : Set M
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (extChartAt I' y).source
hf : ContinuousWithinAt f s x
⊢ True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
have simp_rw : True ∧
    DifferentiableWithinAtProp I I'
      (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
  True ∧
    DifferentiableWithinAtProp I 𝓘(𝕜, E')
      (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
Tactic: simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt 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'
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x
have rw : MDifferentiableWithinAt I I' f univ x ↔
  ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x
Tactic: rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_target_of_mem_source hy,
    continuousWithinAt_univ, ← mdifferentiableWithinAt_univ]