-- 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 : ContMDiffWithinAt I I n (↑f.symm) (f.symm ≫ₕ c).source (↑(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:
rw [contMDiffWithinAt_iff_of_mem_source hy' hy''] at H

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 :
  (↑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

Proof state:
case hx
𝕜 : 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 x) x ∈ (c.symm ≫ₕ f ≫ₕ c').source ∪ (↑(chartAt H x).symm ⁻¹' f.source)ᶜ

Tactic:
apply Or.inl

Result:
case hx.h
𝕜 : 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 x) x ∈ (c.symm ≫ₕ f ≫ₕ c').source

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
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Tactic:
let x := f.symm X

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
⊢ LiftPropWithinAt (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f.symm) f.symm.source X

Proof state:
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 ⁻¹' (chartAt H✝ (↑f x)).target ∩
        (↑I.symm ⁻¹' (↑(chartAt H✝ (↑f x)).symm ⁻¹' f.target) ∩
          ↑I.symm ⁻¹' (↑(chartAt H✝ (↑f x)).symm ⁻¹' (↑f.symm ⁻¹' (chartAt H✝ x).source))) ∩
      range ↑I ⊆
    ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' f.target ∩
        ↑(chartAt H✝ (↑f x)).symm ∘ ↑I.symm ⁻¹' (↑f.symm ⁻¹' (chartAt H✝ x).source) ∩
      range ↑I

Tactic:
mfld_set_tac

Result:
no goals