-- 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_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.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑((c.symm ≫ₕ f) ≫ₕ c').symm ∘ ↑I.symm)
    (↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ 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.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ y = ↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y)

case mpr.intro.refine_2.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.target ∧ ↑f.symm (↑c'.symm (↑I.symm y)) ∈ c.source) ∧ y ∈ range ↑I
H :
  ContinuousWithinAt (↑f.symm) (f.symm ≫ₕ c).source (↑(extChartAt I (↑f x)).symm y) ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt I x) ∘ ↑f.symm ∘ ↑(extChartAt I (↑f x)).symm)
      (↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I)
      (↑(extChartAt I (↑f x)) (↑(extChartAt I (↑f x)).symm y))
hy' : ↑(extChartAt I (↑f x)).symm y ∈ c'.source
hy'' : ↑f.symm (↑(extChartAt I (↑f x)).symm y) ∈ c.source
⊢ ↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range ↑I ⊆ ↑(extChartAt I (↑f x)).symm ⁻¹' (f.symm ≫ₕ c).source ∩ range ↑I

Proof state:
case h.refine_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 : 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
h2X : ↑c' X = ↑e (↑c (↑f.symm X))
⊢ EqOn (↑e) (↑(c.symm ≫ₕ f ≫ₕ c')) (e.source ∩ e.source)

Tactic:
rw [inter_self]

Result:
case h.refine_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 : 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
h2X : ↑c' X = ↑e (↑c (↑f.symm X))
⊢ EqOn (↑e) (↑(c.symm ≫ₕ f ≫ₕ c')) e.source