awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
rw :
  ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [contMDiffWithinAt_iff_target]

Premises used: contMDiffWithinAt_iff_target
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
left : ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
right :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
    ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
      (↑(extChartAt I x).symm : E → M))
    (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
left : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)

Tactic:
apply ContinuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
apply :
  ContinuousAt.{u_3, u_4} (Y := M) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2
    ((↑I.symm : E → H) ((↑(extChartAt I x) : M → E) x))
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)

Tactic:
apply ContinuousAt.comp _ I.continuousAt_symm

Premises used: ContinuousAt.comp, ModelWithCorners.continuousAt_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
⊢ (↑I.symm : E → H) ((↑(extChartAt I x) : M → E) x) ∈
    (OpenPartialHomeomorph.toPartialEquiv (OpenPartialHomeomorph.symm (chartAt H x))).source

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
⊢ ContinuousAt.{u_3, u_4} (Y := M) (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).2
    ((↑I.symm : E → H) ((↑(extChartAt I x) : M → E) x))

Tactic:
exact (chartAt H x).symm.continuousAt (by simp)

Premises used: OpenPartialHomeomorph.continuousAt, chartAt, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
⊢ (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
apply :
  ∀ (y : E) (hy : y ∈ (extChartAt I x).target),
    ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
          (↑(extChartAt I x).symm : E → M))
        y =
      id y
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
    ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
      (↑(extChartAt I x).symm : E → M))
    (extChartAt I x).target ((↑(extChartAt I x) : M → E) x)

Tactic:
apply contMDiffWithinAt_id.congr_of_mem (fun y hy ↦ ?_) (by simp)

Premises used: ContMDiffWithinAt.congr_of_mem, contMDiffWithinAt_id
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) = y

Tactic:
PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
y : E
hy : y ∈ (extChartAt I x).target
h :
  ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      y =
    (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      y =
    id y

Tactic:
convert! PartialEquiv.right_inv (extChartAt I x) hy

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ ((↑(extChartAt I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))) : M → E) ∘
        (↑(extChartAt I x).symm : E → M))
      y =
    (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
x : M
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I n (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)

Tactic:
(contMDiffWithinAt_extChartAt_symm_target_self x).mono_of_mem_nhdsWithin
    (extChartAt_target_mem_nhdsWithin x)

Premises used: extChartAt_target_mem_nhdsWithin, ContMDiffWithinAt.mono_of_mem_nhdsWithin, contMDiffWithinAt_extChartAt_symm_target_self
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
e' : OpenPartialHomeomorph H H
h : e' ∈ contDiffGroupoid n I
⊢ ContMDiffOn I I n (↑e' : H → H) e'.source

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_groupoid contDiffWithinAtProp_id h

Premises used: ContMDiffWithinAt, contDiffWithinAtProp_id, ChartedSpace.LiftPropOn, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
h : ∀ x ∈ f.source, ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
⊢ ContMDiffOn I I n (↑f : M → M') f.source

Tactic:
apply contMDiffOn_of_locally_contMDiffOn

Premises used: contMDiffOn_of_locally_contMDiffOn
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
⊢ (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)

Tactic:
obtain ⟨-, hxf⟩ := hf x hx
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
⊢ (↑(chartAt H x) : M → H) x ∈ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
h :
  ∀ (e : OpenPartialHomeomorph H H) (he : e ∈ contDiffGroupoid n I)
    (he' :
      EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H)
        ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source))
    (hex : (↑c : M → H) x ∈ e.source), ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)

Tactic:
obtain
    ⟨e, he, he' : EqOn (c' ∘ f ∘ c.symm) e (c.symm ⁻¹' f.source ∩ e.source), hex :
      c x ∈ e.source⟩ :=
    hxf (by simp only [hx, mfld_simps])

Premises used: OpenPartialHomeomorph.toFun'
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)

Tactic:
⟨s, (f.trans c').open_source.inter ((c.trans e).trans c'.symm).open_source, ?_, ?_⟩

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.trans, And.intro, IsOpen.inter, Exists.intro, OpenPartialHomeomorph.symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
h : x ∈ s
h₁ : ContMDiffOn I I n (↑f : M → M') (f.source ∩ s)
⊢ ∃ (u : Set M), IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I n (↑f : M → M') (f.source ∩ u)

Tactic:
refine ⟨s, (f.trans c').open_source.inter ((c.trans e).trans c'.symm).open_source, ?_, ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
h :
  (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) x) ∈ c'.target
⊢ x ∈ s

Tactic:
simp only [s, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
h :
  (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧
      ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) x) ∈ c'.target
h₁ : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source
⊢ (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧ (↑e : H → H) ((↑c : M → H) x) ∈ c'.target

Tactic:
rw [← he']
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ (x ∈ f.source ∧ (↑f : M → M') x ∈ c'.source) ∧
    (x ∈ c.source ∧ (↑c : M → H) x ∈ e.source) ∧
      ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c : M → H) x) ∈ c'.target

Tactic:
simp only [c, c', hx, hex, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source ∩ e.source

Tactic:
simp only [c, c', hx, hex, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt
    ((↑(chartAt H ((↑f : M → M') x)) : M' → H) ∘ (↑f : M → M') ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source) ((↑(chartAt H x) : M → H) x)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) ((↑c.symm : H → M) ⁻¹' f.source ∩ e.source)
hex : (↑c : M → H) x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
⊢ ContMDiffOn I I n (↑c'.symm : H → M') (OpenPartialHomeomorph.toPartialEquiv (chartAt H ((↑f : M → M') x))).target

Tactic:
have hc' : ContMDiffOn I I n c'.symm _ := contMDiffOn_chart_symm