-- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : PartialHomeomorph M M') :
    LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt f f.source ↔
      ContMDiffOn I I n f f.source ∧ ContMDiffOn I I n f.symm f.target

Proof state:
case mpr.intro.refine_4
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : PartialHomeomorph M H := chartAt H x
c' : PartialHomeomorph M' H := chartAt H (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ ↑(chartAt H x) x ∈ ((c.symm ≫ₕ f) ≫ₕ c').source

Tactic:
simp only [c, c', hx', mfld_simps]

Result:
no goals

Proof state:
case mpr.intro.refine_1
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H✝ : Type u_3
inst✝⁵ : TopologicalSpace H✝
I : ModelWithCorners 𝕜 E H✝
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H✝ M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H✝ M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : PartialHomeomorph M H✝ := chartAt H✝ x
c' : PartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (↑f x)) ∘ ↑f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I) (↑(extChartAt I x) (↑(extChartAt I x).symm y))
hy' : ↑(extChartAt I x).symm y ∈ c.source
hy'' : ↑f (↑(extChartAt I x).symm y) ∈ c'.source
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑((c.symm ≫ₕ f) ≫ₕ c') ∘ ↑I.symm) (↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range ↑I) y

Tactic:
convert H.2.mono _

Result:
case h.e'_12
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H✝ : Type u_3
inst✝⁵ : TopologicalSpace H✝
I : ModelWithCorners 𝕜 E H✝
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H✝ M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H✝ M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : PartialHomeomorph M H✝ := chartAt H✝ x
c' : PartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (↑f x)) ∘ ↑f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I) (↑(extChartAt I x) (↑(extChartAt I x).symm y))
hy' : ↑(extChartAt I x).symm y ∈ c.source
hy'' : ↑f (↑(extChartAt I x).symm y) ∈ c'.source
⊢ y = ↑(extChartAt I x) (↑(extChartAt I x).symm y)

case mpr.intro.refine_1.convert_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H✝ : Type u_3
inst✝⁵ : TopologicalSpace H✝
I : ModelWithCorners 𝕜 E H✝
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H✝ M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H✝ M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : PartialHomeomorph M H✝ := chartAt H✝ x
c' : PartialHomeomorph M' H✝ := chartAt H✝ (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I (↑f x)) ∘ ↑f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I) (↑(extChartAt I x) (↑(extChartAt I x).symm y))
hy' : ↑(extChartAt I x).symm y ∈ c.source
hy'' : ↑f (↑(extChartAt I x).symm y) ∈ c'.source
⊢ ↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').source ∩ range ↑I ⊆ ↑(extChartAt I x).symm ⁻¹' (f ≫ₕ c').source ∩ range ↑I

Proof state:
case mp
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Tactic:
have hx : x ∈ f.source := f.symm.mapsTo hX

Result:
case mp
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : WithTop ℕ∞
inst✝² : IsManifold I n M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : PartialHomeomorph M M'
h : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
X : M'
hX : X ∈ f.symm.source
x : M := ↑f.symm X
hx : x ∈ f.source
c : PartialHomeomorph M H := chartAt H x
c' : PartialHomeomorph M' H := chartAt H X
hxf :
  (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
e : PartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
h2e : e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source
hef : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source
hex : ↑c x ∈ e.source
⊢ ↑f.symm X ∈ c.source

Tactic:
simp only [c, x, hX, mfld_simps]

Result:
no goals