-- 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:
𝕜 : 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
⊢ ↑c' X = ↑c' (↑f (↑c.symm (↑c x)))

Tactic:
have hfX : f.symm X ∈ c.source := by simp only [c, x, hX, mfld_simps]

Result:
𝕜 : 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
hfX : ↑f.symm X ∈ c.source
⊢ ↑c' X = ↑c' (↑f (↑c.symm (↑c x)))

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
⊢ (contDiffPregroupoid n I).property (↑((c.symm ≫ₕ f) ≫ₕ c').symm) ((c.symm ≫ₕ f) ≫ₕ c').target

Tactic:
intro y hy

Result:
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 : y ∈ ↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑((c.symm ≫ₕ f) ≫ₕ c').symm ∘ ↑I.symm)
    (↑I.symm ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range ↑I) y

Proof state:
case mpr.intro
𝕜 : 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
⊢ (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) x)

Tactic:
let c' := chartAt H (f x)

Result:
case mpr.intro
𝕜 : 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)
⊢ (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑(chartAt H (↑f x)) ∘ ↑f ∘ ↑(chartAt H x).symm)
    (↑(chartAt H x).symm ⁻¹' f.source) (↑(chartAt H x) 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
h2X : ↑c' X = ↑e (↑c (↑f.symm X))
h1 : EqOn (↑(c.symm ≫ₕ f ≫ₕ c').symm) (↑e.symm) (e.target ∩ e.target)
x : H
hx : x ∈ e.target
⊢ (↑c' ∘ ↑f ∘ ↑c.symm) (↑e.symm x) ∈ (c.symm ≫ₕ f ≫ₕ c').target

Tactic:
exact PartialHomeomorph.mapsTo _ (h2e <| e.symm.mapsTo hx)

Result:
no goals