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

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : M) in 𝓝[s] x, ↑(chartAt H' (g' x)) (g' x_1) = ↑(chartAt H' (g x)) (g x_1)

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
⊢ ∀ᶠ (x_1 : M) in 𝓝[s] x, ↑(chartAt H' (g' x)) (g' x_1) = ↑(chartAt H' (g x)) (g x_1)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
h₁ : g' =ᶠ[𝓝[s] x] g
hx : g' x = g x
y : M
hy : g' y = g y
⊢ ↑(chartAt H' (g x)) (g y) = ↑(chartAt H' (g x)) (g y)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g univ x
⊢ LiftPropWithinAt P g s x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type w
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝⁴ : I.Boundaryless
E' : Type v'
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
H' : Type w'
inst✝¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
inst✝ : I'.Boundaryless
⊢ univ = univ

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm) univ x ∧
    Q (↑e ∘ ↑e.symm ∘ ↑(OpenPartialHomeomorph.refl H).symm) (↑(OpenPartialHomeomorph.refl H).symm ⁻¹' univ)
      (↑(OpenPartialHomeomorph.refl H) x)

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm) univ x ∧
    Q (↑e ∘ ↑e.symm ∘ ↑(OpenPartialHomeomorph.refl H).symm) (↑(OpenPartialHomeomorph.refl H).symm ⁻¹' univ)
      (↑(OpenPartialHomeomorph.refl H) x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ ContinuousWithinAt (↑e.symm) univ x ∧
    Q (↑e ∘ ↑e.symm ∘ ↑(OpenPartialHomeomorph.refl H).symm) (↑(OpenPartialHomeomorph.refl H).symm ⁻¹' univ)
      (↑(OpenPartialHomeomorph.refl H) x)

Tactic:
refine ⟨(e.symm.continuousAt hx).continuousWithinAt, ?_⟩

Goal state after:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
Q : (H → H) → Set H → H → Prop
x : H
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.target
h : Q (↑e ∘ ↑e.symm) univ x
this : ↑e.symm x ∈ e.source
⊢ Q (↑e ∘ ↑e.symm ∘ ↑(OpenPartialHomeomorph.refl H).symm) (↑(OpenPartialHomeomorph.refl H).symm ⁻¹' univ)
    (↑(OpenPartialHomeomorph.refl H) x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
x : E
left✝ : x ∈ ↑I.symm ⁻¹' univ
hx2 : x ∈ range ↑I
y : H
hy : ↑I y = x
⊢ (↑I ∘ id ∘ ↑I.symm) (↑I y) = id (↑I y)

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
x : E
left✝ : x ∈ ↑I.symm ⁻¹' univ
hx2 : x ∈ range ↑I
y : H
hy : ↑I y = x
⊢ (↑I ∘ id ∘ ↑I.symm) (↑I y) = id (↑I y)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      ↑I x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      ↑I x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
⊢ ↑I.symm ⁻¹' u ∩ (↑I.symm ⁻¹' v ∩ range ↑I) = ↑I.symm ⁻¹' u ∩ (range ↑I ∩ ↑I.symm ⁻¹' v)

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
⊢ ↑I.symm ⁻¹' u ∩ (↑I.symm ⁻¹' v ∩ range ↑I) = ↑I.symm ⁻¹' u ∩ (range ↑I ∩ ↑I.symm ⁻¹' v)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case e_a
m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
⊢ range ↑I ∩ ↑I.symm ⁻¹' v = range ↑I ∩ ↑I.symm ⁻¹' v

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v)
this : ↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I = ↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      ↑I x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
f : H✝ → H✝
u : Set H✝
x✝ : IsOpen[inst✝¹] u
H : ∀ x ∈ u, ∃ v, IsOpen[inst✝¹] v ∧ x ∈ v ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H✝
hx : ↑I x = y
hy1 : x ∈ u
v : Set H✝
v_open : IsOpen[inst✝¹] v
xv : x ∈ v
hv : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v)
this : ↑I.symm ⁻¹' (u ∩ v) ∩ range ↑I = ↑I.symm ⁻¹' u ∩ range ↑I ∩ ↑I.symm ⁻¹' v
⊢ ∃ u_1,
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u_1 ∧
      ↑I x ∈ u_1 ∧ ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I ∩ u_1)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f g : H → H
u : Set H
x✝ : IsOpen[inst✝¹] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ (↑I ∘ g ∘ ↑I.symm) (↑I x) = (↑I ∘ f ∘ ↑I.symm) (↑I x)

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
f g : H → H
u : Set H
x✝ : IsOpen[inst✝¹] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H
hy1 : ↑I x ∈ ↑I.symm ⁻¹' u
hx : ↑I x = y
⊢ (↑I ∘ g ∘ ↑I.symm) (↑I x) = (↑I ∘ f ∘ ↑I.symm) (↑I x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
f g : H → H
u : Set H
x✝ : IsOpen[inst✝¹] u
fg : ∀ x ∈ u, g x = f x
hf : ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' u ∩ range ↑I)
y : E
hy2 : y ∈ range ↑I
x : H
hx : ↑I x = y
hy1 : x ∈ u
⊢ ↑I (f x) = ↑I (f x)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: m n : ℕ∞ω
𝕜 : 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
h : m ≤ n
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid

Tactic:
]

Goal state after:
m n : ℕ∞ω
𝕜 : 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
h : m ≤ n
⊢ (contDiffPregroupoid n I).groupoid ≤ (contDiffPregroupoid m I).groupoid
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (extChartAt I x).target

Tactic:
rw [extChartAt_target]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ UniqueDiffOn 𝕜 (↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q id ↑x

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q id ↑x
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

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
u : OpenPartialHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ { property := fun f s ↦ ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯,
          locality := ⋯, congr := ⋯ }.property
      (↑u) u.source ∧
    { property := fun f s ↦ ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯,
          locality := ⋯, congr := ⋯ }.property
      (↑u.symm) u.target

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
u : OpenPartialHomeomorph H H
a✝ : u ∈ ⊤.members
⊢ { property := fun f s ↦ ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯,
          locality := ⋯, congr := ⋯ }.property
      (↑u) u.source ∧
    { property := fun f s ↦ ContDiffOn 𝕜 0 (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I), comp := ⋯, id_mem := ⋯,
          locality := ⋯, congr := ⋯ }.property
      (↑u.symm) u.target
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q id (inclusion hUV x)

Tactic:
]

Goal state after:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U V : Opens M
hUV : U ≤ V
x : ↥U
⊢ LiftPropAt Q id (inclusion hUV x)
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
⊢ x' ∈ (extChartAt I x).source

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
⊢ x' ∈ (extChartAt I x).source
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case left
n : ℕ∞ω
𝕜 : 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : ↑I.symm x ∈ f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x

Tactic:
]

Goal state after:
case left
n : ℕ∞ω
𝕜 : 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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
x : E
hx : ↑I.symm x ∈ f.source
right✝ : x ∈ range ↑I
⊢ ContDiffWithinAt 𝕜 n (↑I ∘ ↑f ∘ ↑I.symm) (↑I.symm ⁻¹' f.source ∩ range ↑I) x
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (extChartAt I x).source

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (extChartAt I x).source
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ map (↑((chartAt H x).extend I)) (𝓝 x) = 𝓝 (↑((chartAt H x).extend I) x)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ map (↑((chartAt H x).extend I)) (𝓝 x) = 𝓝 (↑((chartAt H x).extend I) x)
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I

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
f : OpenPartialHomeomorph H H
hf : f.source = ∅
⊢ f ∈ contDiffGroupoid 0 I
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : 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
s : Set H
hs : IsOpen[inst✝] s
⊢ (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs)) (OpenPartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs).symm)
      (OpenPartialHomeomorph.ofSet s hs).target

Tactic:
]

Goal state after:
n : ℕ∞ω
𝕜 : 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
s : Set H
hs : IsOpen[inst✝] s
⊢ (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs)) (OpenPartialHomeomorph.ofSet s hs).source ∧
    (contDiffPregroupoid n I).property (↑(OpenPartialHomeomorph.ofSet s hs).symm)
      (OpenPartialHomeomorph.ofSet s hs).target