-- 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 hs
𝕜 : 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 (↑(c.symm ≫ₕ f ≫ₕ c')) (↑(chartAt H x).symm ⁻¹' f.source)
    (↑(chartAt H x) x)
h2x : ↑(chartAt H X) X ∈ ↑(chartAt H X).symm ⁻¹' f.symm.source
h1 : c' = chartAt H (↑f x)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ (chartAt H (↑f.symm X)).target ∩
      (↑(chartAt H (↑f.symm X)).symm ⁻¹' f.source ∩ ↑(chartAt H (↑f.symm X)).symm ⁻¹' (↑f ⁻¹' c'.source)) ⊆
    ↑(chartAt H (↑f.symm X)).symm ⁻¹' f.source

Tactic:
mfld_set_tac

Result:
no goals

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 ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source ∧ ↑c x ∈ e.source

Tactic:
have h1 : c' = chartAt H (f x) := by simp only [x, c', f.right_inv hX]

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
h1 : c' = chartAt H (↑f x)
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) e.source ∧ ↑c x ∈ e.source

Proof state:
case 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
⊢ (f.symm ≫ₕ c).source ⊆ f.target

Tactic:
mfld_set_tac

Result:
no goals

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₁ : 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
⊢ ContMDiffWithinAt I I n (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y)

Tactic:
refine (h₁ ((extChartAt I x).symm y) ?_).mono ?_

Result:
case 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
⊢ ↑(extChartAt I x).symm y ∈ f.source

case 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.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
⊢ (f ≫ₕ c').source ⊆ f.source