awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
refine :
  ∀ (h : ContinuousOn f s) (x : M) (y : M'),
    ContDiffOn 𝕜 0 ((↑(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))
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 0 ((↑(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))) ↔
    ContinuousOn f s

Tactic:
refine ⟨fun h ↦ h.1, fun h ↦ ⟨h, ?_⟩⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
rw :
  ContinuousOn ((↑(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))
⊢ ContDiffOn 𝕜 0 ((↑(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))

Tactic:
rw [contDiffOn_zero]

Premises used: contDiffOn_zero
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
hf :
  ContinuousOn (f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
h₁ :
  MapsTo (f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
    (extChartAt I' y).source
⊢ ContinuousOn ((↑(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))

Tactic:
apply (continuousOn_extChartAt _).comp

Premises used: continuousOn_extChartAt, ContinuousOn.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
apply :
  ∀ (z : E)
    (hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)),
    (↑(extChartAt I x).symm : E → M) z ∈ s
⊢ ContinuousOn (f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
apply h.comp ((continuousOn_extChartAt_symm _).mono inter_subset_left) (fun z hz ↦ ?_)

Premises used: Set.inter_subset_left, ContinuousOn.comp, continuousOn_extChartAt_symm, ContinuousOn.mono
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
⊢ z ∈ (extChartAt I x).target ∧
    (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source

Tactic:
simp only [preimage_inter, mem_inter_iff, mem_preimage] at hz

Premises used: Set.preimage_inter, Set.mem_inter_iff, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
z : E
hz :
  z ∈ (extChartAt I x).target ∧
    (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
⊢ (↑(extChartAt I x).symm : E → M) z ∈ s

Tactic:
hz.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
z : E
hz :
  z ∈ (extChartAt I x).target ∧
    (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
⊢ (↑(extChartAt I x).symm : E → M) z ∈ s

Tactic:
exact hz.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
z : E
hz :
  z ∈ (extChartAt I x).target ∧
    (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
⊢ (f ∘ (↑(extChartAt I x).symm : E → M)) z ∈ (extChartAt I' y).source

Tactic:
hz.2.2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
h : ContinuousOn f s
x : M
y : M'
z : E
hz :
  z ∈ (extChartAt I x).target ∧
    (↑(extChartAt I x).symm : E → M) z ∈ s ∧ f ((↑(extChartAt I x).symm : E → M) z) ∈ (extChartAt I' y).source
⊢ (f ∘ (↑(extChartAt I x).symm : E → M)) z ∈ (extChartAt I' y).source

Tactic:
exact hz.2.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
simp :
  ContinuousOn f s →
    ((∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n
          ((↑(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'),
            ContDiffOn 𝕜 n
              ((↑(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)))
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)

Tactic:
simp only [contMDiffOn_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: extChartAt, OpenPartialHomeomorph.refl_partialEquiv, ModelWithCorners.source_eq, Set.inter_univ, and_congr_right_iff, contMDiffOn_iff, Set.preimage_univ, PartialEquiv.refl_trans, OpenPartialHomeomorph.extend, chartAt_self_eq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
⊢ (∀ (x : M) (y : M'),
      ContDiffOn 𝕜 n
        ((↑(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'),
          ContDiffOn 𝕜 n
            ((↑(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.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
mp :
  ∀
    (h' :
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n
          ((↑(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'),
      ContDiffOn 𝕜 n
        ((↑(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'),
          ContDiffOn 𝕜 n
            ((↑(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.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(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.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(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.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(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
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n
      ((↑(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
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source =
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source ∩
      (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)) : M' → H') ⁻¹' univ

Tactic:
simp