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 : ℕ∞ω
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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target

Tactic:
rw [inter_self] at h1

Premises used: Set.inter_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
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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) (e.target ∩ e.target)
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
h1₁ : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
⊢ e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target

Tactic:
rw [inter_self] at h1

Premises used: Set.inter_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
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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
rwa : e.target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
⊢ EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)

Tactic:
rwa [inter_eq_right.mpr]

Premises used: Iff.mpr, Set.inter_eq_right
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
⊢ e.target ⊆ (↑c'.symm : H → M') ⁻¹' f.target

Tactic:
h2.trans ?_

Premises used: HasSubset.Subset.trans
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
refine : (c.symm ≫ₕ f ≫ₕ c').target ⊆ (↑c'.symm : H → M') ⁻¹' f.target
⊢ e.target ⊆ (↑c'.symm : H → M') ⁻¹' f.target

Tactic:
refine h2.trans ?_

Premises used: HasSubset.Subset.trans
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm : H → H) (↑e.symm : H → H) e.target
h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : H⦄, my_y ∈ (c.symm ≫ₕ f ≫ₕ c').target → my_y ∈ (↑c'.symm : H → M') ⁻¹' f.target
mfld_set_tac₃ mfld_set_tac₄ :
  ∀ ⦃my_y : H⦄,
    (my_y ∈ c'.target ∧ (↑c'.symm : H → M') my_y ∈ f.target) ∧
        (↑f.symm : M' → M) ((↑c'.symm : H → M') my_y) ∈ c.source →
      my_y ∈ (↑c'.symm : H → M') ⁻¹' f.target
⊢ (c.symm ≫ₕ f ≫ₕ c').target ⊆ (↑c'.symm : H → M') ⁻¹' f.target

Tactic:
mfld_set_tac
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
⊢ EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)

Tactic:
have h3e : EqOn (c ∘ f.symm ∘ c'.symm) e.symm (c'.symm ⁻¹' f.target ∩ e.target) := by
      have h1 : EqOn (c.symm ≫ₕ f ≫ₕ c').symm e.symm (e.target ∩ e.target) := by
        apply EqOn.symm
        refine e.isImage_source_target.symm_eqOn_of_inter_eq_of_eqOn ?_ ?_
        · rw [inter_self, inter_eq_right.mpr h2e]
        · rw [inter_self]; exact hef.symm
      have h2 : e.target ⊆ (c.symm ≫ₕ f ≫ₕ c').target := by
        intro x hx; rw [← e.right_inv hx, ← hef (e.symm.mapsTo hx)]
        exact OpenPartialHomeomorph.mapsTo _ (h2e <| e.symm.mapsTo hx)
      rw [inter_self] at h1
      rwa [inter_eq_right.mpr]
      refine h2.trans ?_
      mfld_set_tac
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f.symm : M' → M) X)) : M → H) ∘
          (↑f.symm : M' → M) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M'))
        (↑e.toPartialEquiv : H → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source ∩ e.source) ∧
      (↑(chartAt H X) : M' → H) X ∈ e.source

Tactic:
⟨e.symm, StructureGroupoid.symm _ he, h3e, ?_⟩

Premises used: And.intro, Exists.intro, StructureGroupoid.symm, 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
mp : (↑(chartAt H X) : M' → H) X ∈ e.symm.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    EqOn
        ((↑(chartAt H ((↑f.symm : M' → M) X)) : M → H) ∘
          (↑f.symm : M' → M) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M'))
        (↑e.toPartialEquiv : H → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source ∩ e.source) ∧
      (↑(chartAt H X) : M' → H) X ∈ e.source

Tactic:
refine ⟨e.symm, StructureGroupoid.symm _ he, h3e, ?_⟩
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
mp : (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X)) ∈ e.symm.source
⊢ (↑(chartAt H X) : M' → H) X ∈ e.symm.source

Tactic:
rw [h2X]
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
⊢ (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X)) ∈ e.symm.source

Tactic:
e.mapsTo hex

Premises used: Set.Mem, OpenPartialHomeomorph.mapsTo
-- 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'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source
X : M'
hX : X ∈ f.symm.source
x : M := (↑f.symm : M' → M) X
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H 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)
h2x : (↑(chartAt H X) : M' → H) X ∈ (↑(OpenPartialHomeomorph.symm (chartAt H X)) : H → M') ⁻¹' f.symm.source
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑e : H → H) e.source
hex : (↑c : M → H) x ∈ e.source
h2X : (↑c' : M' → H) X = (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X))
h3e :
  EqOn ((↑c : M → H) ∘ (↑f.symm : M' → M) ∘ (↑c'.symm : H → M')) (↑e.symm : H → H)
    ((↑c'.symm : H → M') ⁻¹' f.target ∩ e.target)
⊢ (↑e : H → H) ((↑c : M → H) ((↑f.symm : M' → M) X)) ∈ e.symm.source

Tactic:
exact e.mapsTo hex

Premises used: OpenPartialHomeomorph.mapsTo
-- 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'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source x

Tactic:
⟨(h₁ x hx).continuousWithinAt, ?_⟩

Premises used: ContMDiffWithinAt.continuousWithinAt, ChartedSpace.LiftPropWithinAt.mk
-- 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'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
mpr :
  (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)
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f : M → M') f.source x

Tactic:
refine ⟨(h₁ x hx).continuousWithinAt, ?_⟩