awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  ContinuousWithinAt f s x ∧
    DifferentiableWithinAtProp I I'
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
refine differentiableWithinAt_localInvariantProp.liftPropWithinAt_iff.mpr ?_

Premises used: Iff.mpr, differentiableWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ ContinuousWithinAt f s x ∧
    DifferentiableWithinAtProp I I'
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)

Tactic:
⟨hcont x hx, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  DifferentiableWithinAtProp I I'
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)
⊢ ContinuousWithinAt f s x ∧
    DifferentiableWithinAtProp I I'
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)

Tactic:
refine ⟨hcont x hx, ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  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.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ DifferentiableWithinAtProp I I'
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)

Tactic:
dsimp [DifferentiableWithinAtProp]

Premises used: DifferentiableWithinAtProp
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
h :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E) =
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
⊢ 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.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
convert! hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1

Premises used: extChartAt, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
h h₁ h₂ h₃ :
  ∀ (my_y : E),
    my_y ∈
        (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
            ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
              (↑I.symm : E → H) ⁻¹'
                (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
                  f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
          range (↑I : H → E) ↔
      my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E) =
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
simp :
  ContinuousOn f s →
    ((∀ (x : M) (y : M'),
        DifferentiableOn 𝕜
          ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
            f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
          ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
            (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
              (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) ↔
      ∀ (y : M'),
        ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
          ∀ (x : M) (y_1 : E'),
            DifferentiableOn 𝕜
              ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
                ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                  (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
              ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                  (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)))
⊢ MDifferentiableOn I I' f s ↔
    ContinuousOn f s ∧
      ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)

Tactic:
simp only [mdifferentiableOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
    OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_trans, extChartAt,
    OpenPartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, and_congr_right_iff]

Premises used: mdifferentiableOn_iff, extChartAt, OpenPartialHomeomorph.refl_partialEquiv, ModelWithCorners.source_eq, Set.inter_univ, and_congr_right_iff, Set.preimage_univ, PartialEquiv.refl_trans, OpenPartialHomeomorph.extend, chartAt_self_eq
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))

Tactic:
fun h' y => ⟨?_, fun x _ => h' x y⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
mp :
  ∀
    (h' :
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜
          ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
            f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
          ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
            (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
              (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)))
    (y : M'),
    ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
      (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)
⊢ (∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))

Tactic:
refine fun h' y => ⟨?_, fun x _ => h' x y⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
        (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
y : M'
⊢ ContinuousOn (↑I' : H' → E') univ

Tactic:
have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
        (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I' : H' → E') univ
⊢ ContinuousOn (((↑I' : H' → E') ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)) : M' → H')) ∘ f)
    (s ∩
      f ⁻¹'
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)) : M' → H') ⁻¹' univ))

Tactic:
(h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h

Premises used: chartAt, ContinuousOn.comp_inter, OpenPartialHomeomorph.continuousOn_toFun
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
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
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
        f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
        (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I' : H' → E') univ
h₁ :
  (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source ∩
      (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)) : M' → H') ⁻¹' univ
⊢ ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
    (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source)

Tactic:
convert! (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h

Premises used: chartAt, ContinuousOn.comp_inter, OpenPartialHomeomorph.continuousOn_toFun