mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
x : M
⊢ ContinuousWithinAt (↑(extChartAt I x).symm) (extChartAt I x).target (↑(extChartAt I x) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      (↑(extChartAt I (↑(extChartAt I x).symm (↑(extChartAt I x) x))) ∘ ↑(extChartAt I x).symm) (extChartAt I x).target
      (↑(extChartAt I x) x)

Tactic:
]

Goal state after:
𝕜 : 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 : ℕ∞ω
x : M
⊢ ContinuousWithinAt (↑(extChartAt I x).symm) (extChartAt I x).target (↑(extChartAt I x) x) ∧
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E) n
      (↑(extChartAt I (↑(extChartAt I x).symm (↑(extChartAt I x) x))) ∘ ↑(extChartAt I x).symm) (extChartAt I x).target
      (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
h :
  ∀ (x : ↑e.source),
    ∃ s,
      IsOpen[instTopologicalSpaceProd] s ∧
        ↑x ∈ s ∧
          ∃ φ u,
            ∃ (hu : IsOpen[inst✝⁷] u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) u) (h2φ :
              ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) u),
              (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)
⊢ ∃ U,
    e.source = U ×ˢ univ ∧
      ∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen[inst✝⁷] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) u)
            (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) u),
            (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)

Tactic:
]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
h :
  ∀ (x : ↑e.source),
    ∃ s,
      IsOpen[instTopologicalSpaceProd] s ∧
        ↑x ∈ s ∧
          ∃ φ u,
            ∃ (hu : IsOpen[inst✝⁷] u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) u) (h2φ :
              ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) u),
              (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)
⊢ ∃ U,
    e.source = U ×ˢ univ ∧
      ∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen[inst✝⁷] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) u)
            (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) u),
            (e.restr (u ×ˢ univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
p : ↑e.source
⊢ (e.restr (s p)).source = u p ×ˢ univ

Tactic:
]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
p : ↑e.source
⊢ (e.restr (s p)).source = u p ×ˢ univ
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑f y = ↑f y

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑c'.symm (↑c' (↑f y)) = ↑c'.symm (↑c' (↑f y))

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑c'.symm (↑c' (↑f (↑c.symm (↑c y)))) = ↑c'.symm ((↑c' ∘ ↑f ∘ ↑c.symm) (↑c y))

Tactic:
]

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑c'.symm (↑c' (↑f (↑c.symm (↑c y)))) = ↑c'.symm ((↑c' ∘ ↑f ∘ ↑c.symm) (↑c y))
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑c'.symm (↑c' (↑f (↑c.symm (↑c y)))) = ↑c'.symm (↑e (↑c y))

Tactic:
rw [← he' hy₃]

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
hf : LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f 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)
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
he' : EqOn (↑c' ∘ ↑f ∘ ↑c.symm) (↑e) (↑c.symm ⁻¹' f.source ∩ e.source)
hex : ↑c x ∈ e.source
s : Set M := (f ≫ₕ c').source ∩ ((c ≫ₕ e) ≫ₕ c'.symm).source
H₁ : ContMDiffOn I I n (↑c'.symm ∘ ↑e ∘ ↑c) s
y : M
hy : (y ∈ f.source ∧ ↑f y ∈ c'.source) ∧ (y ∈ c.source ∧ ↑c y ∈ e.source) ∧ ↑e (↑c y) ∈ c'.target
hy₁ : ↑f y ∈ c'.source
hy₂ : y ∈ c.source
hy₃ : ↑c y ∈ ↑c.symm ⁻¹' f.source ∩ e.source
⊢ ↑c'.symm (↑c' (↑f (↑c.symm (↑c y)))) = ↑c'.symm ((↑c' ∘ ↑f ∘ ↑c.symm) (↑c y))
Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ
hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p
p : ↑e.source
q : B × F
hq : q.1 ∈ u p
this : q ∈ e.source ∩ s p
⊢ q ∈ e.source

Tactic:
]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
s : ↑e.source → Set (B × F)
hs : ∀ (x : ↑e.source), IsOpen[instTopologicalSpaceProd] (s x)
hsp : ∀ (x : ↑e.source), ↑x ∈ s x
φ : ↑e.source → B → F ≃L[𝕜] F
u : ↑e.source → Set B
hu : ∀ (x : ↑e.source), IsOpen[inst✝⁷] (u x)
hφ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1)) (u x)
h2φ : ∀ (x : ↑e.source), ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x_1 ↦ ↑(φ x x_1).symm) (u x)
heφ : ∀ (x : ↑e.source), (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (φ x) ⋯ ⋯ ⋯)
hesu : ∀ (p : ↑e.source), e.source ∩ s p = u p ×ˢ univ
hu' : ∀ (p : ↑e.source), (↑p).1 ∈ u p
p : ↑e.source
q : B × F
hq : q.1 ∈ u p
this : q ∈ e.source ∩ s p
⊢ q ∈ e.source
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑(c.symm ≫ₕ f ≫ₕ c')) (↑e) e.source ∧ ↑c x ∈ e.source

Tactic:
]

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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)
h2 : ↑c' ∘ ↑f ∘ ↑c.symm = ↑(c.symm ≫ₕ f ≫ₕ c')
hcx : ↑c x ∈ ↑c.symm ⁻¹' f.source
⊢ ∃ e ∈ contDiffGroupoid n I,
    e.source ⊆ (c.symm ≫ₕ f ≫ₕ c').source ∧ EqOn (↑(c.symm ≫ₕ f ≫ₕ c')) (↑e) e.source ∧ ↑c x ∈ e.source
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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 : OpenPartialHomeomorph 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:
]

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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 : OpenPartialHomeomorph 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)
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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 : OpenPartialHomeomorph 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)))

Tactic:
c.left_inv hfX,

Goal state after:
𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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 : OpenPartialHomeomorph 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 (↑f.symm X))
Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: 𝕜 : 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 : ℕ∞ω
M' : Type u_5
inst✝² : TopologicalSpace M'
inst✝¹ : IsManifold I n M
inst✝ : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph 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 : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph 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 : OpenPartialHomeomorph 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' X

Tactic:
]

Goal state after: