mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (i : ℕ), ∫⁻ (a : E) in s ∩ u i, ENNReal.ofReal |(f' a).det| ∂μ

pp: case hm
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ ∀ (i : ℕ), MeasurableSet (s ∩ u i)

pp: case hd
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ Pairwise (Disjoint on fun n ↦ s ∩ u n)

Tactic:
]

Goal state after:
case hm
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ ∀ (i : ℕ), MeasurableSet (s ∩ u i)

case hd
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ Pairwise (Disjoint on fun n ↦ s ∩ u n)
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ interior s

Tactic:
hs.interior_eq

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ s
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ s

Tactic:
]

Goal state after:
H : Type u_1
inst✝ : TopologicalSpace H
e : OpenPartialHomeomorph H H
h : ∀ x ∈ e.source, ∃ s, IsOpen[inst✝] s ∧ x ∈ s ∧ e.restr s ∈ {e | ∃ s, ∃ (h : IsOpen[inst✝] s), e ≈ ofSet s h}
x : H
hx : x ∈ e.source
s : Set H
hs : IsOpen[inst✝] s
hxs : x ∈ s
s' : Set H
hs' : IsOpen[inst✝] s'
hes' : e.restr s ≈ ofSet s' hs'
⊢ x ∈ s
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ e ∈ idRestrGroupoid, e ∈ G

Tactic:
]

Goal state after:
case mp
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
_i : ClosedUnderRestriction G
⊢ ∀ e ∈ idRestrGroupoid, e ∈ G
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ dist B.det A.det ≤ ↑ε

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ dist B.det A.det ≤ ↑ε
Module: Mathlib.Geometry.Manifold.StructureGroupoid

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ ofSet s hs ≫ₕ e ∈ G

Tactic:
]

Goal state after:
case mpr
H : Type u_1
inst✝ : TopologicalSpace H
G : StructureGroupoid H
h : idRestrGroupoid ≤ G
e : OpenPartialHomeomorph H H
he : e ∈ G
s : Set H
hs : IsOpen[inst✝] s
⊢ ofSet s hs ≫ₕ e ∈ G
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ ‖B - A‖ < δ'

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < ↑ε
δ'' : ℝ≥0 := ⟨δ' / 2, ⋯⟩
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ ↑δ''
⊢ ‖B - A‖ < δ'
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
H : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ ↑I.toPartialEquiv '' univ = ↑I.toPartialEquiv '' univ

Tactic:
]

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ f.source = f.source

Tactic:
]

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst✝] f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst✝] f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ IsOpen[inst✝] (f.extend I).source

Tactic:
rw [extend_source]
  exact f.open_source

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I '' f.target = ↑I '' f.target

Tactic:
]

Goal state after:
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
φ : PartialEquiv H E
hsource : φ.source = univ
htarget : φ.target = univ
hcont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑φ
hcont_inv : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝] ↑φ.symm
⊢ ↑φ '' univ = ↑φ '' univ

Tactic:
]

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑I ∘ ↑f '' f.source = ↑I ∘ ↑f '' f.source

Tactic:
]

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' f.target)

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' f.target)
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ (OpenPartialHomeomorph.refl H).subtypeRestr this ∈
    maximalAtlas (↥s) G

Tactic:
]

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ (OpenPartialHomeomorph.refl H).subtypeRestr this ∈
    maximalAtlas (↥s) G
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G

Tactic:
]

Goal state after:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
G : StructureGroupoid H
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
hs : Nonempty ↑e.source
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
s : Opens M := { carrier := e.source, is_open' := ⋯ }
t : Opens H := { carrier := e.target, is_open' := ⋯ }
c' : OpenPartialHomeomorph (↥t) H
hc'✝ : c' ∈ atlas H ↥t
this : Nonempty ↥t
x : ↥t
hc' : c' = (chartAt H ↑x).subtypeRestr this
⊢ e.toHomeomorphSourceTarget.toOpenPartialHomeomorph ≫ₕ t.openPartialHomeomorphSubtypeCoe this ∈ maximalAtlas (↥s) G
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑f.symm ⁻¹' s) ⊆ ↑I '' ↑f.symm ⁻¹' s

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑f.symm ⁻¹' s) ⊆ ↑I '' ↑f.symm ⁻¹' s
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
⊢ x ∈ f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hxf : x ∈ f.source
⊢ x ∈ f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ x ∈ f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ x ∈ f.source
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
⊢ I.target = ↑I '' I.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
⊢ I.target = ↑I '' I.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) f.source
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : ∀ (x : H), x ∈ s ∩ o ↔ x ∈ t ∩ o
⊢ P f s x ↔ P f t x

Tactic:
← Set.ext_iff

Goal state after:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f s x ↔ P f t x
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen[inst✝¹] o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f t x ↔ P f t x

Tactic:
]

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

Goal state before:
pp: H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f g : H → H'
hu : s =ᶠ[𝓝 x] t
h : f =ᶠ[𝓝 x] g
⊢ P g t x ↔ P g t x

Tactic:
]

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

Goal state before:
pp: case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P (↑e' ∘ f) (s ∩ ↑e' ∘ f ⁻¹' e'.symm.source) x
⊢ P f s x

Tactic:
]

Goal state after:
case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P (↑e' ∘ f) (s ∩ ↑e' ∘ f ⁻¹' e'.symm.source) x
⊢ P f s 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ map (↑I ∘ ↑f) (𝓝 x) = map (↑I ∘ ↑f) (𝓝 x)

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ x ∈ f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
⊢ x ∈ f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
⊢ range ↑I ∈ 𝓝 (↑(f.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
⊢ range ↑I ∈ 𝓝 (↑(f.extend I) x)
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P (↑e' ∘ f) (s ∩ ↑e' ∘ f ⁻¹' e'.symm.source) x
h2 : P (↑e'.symm ∘ ↑e' ∘ f) s x
⊢ P f s x

Tactic:
]

Goal state after:
case mp
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ G'
hfs : ContinuousWithinAt f s x
hxe' : f x ∈ e'.source
h2f : f ⁻¹' e'.source ∈ 𝓝[s] x
h3f : ↑e' ∘ f ⁻¹' e'.symm.source ∈ 𝓝[s] x
h : P (↑e' ∘ f) (s ∩ ↑e' ∘ f ⁻¹' e'.symm.source) x
h2 : P (↑e'.symm ∘ ↑e' ∘ f) s x
⊢ P f s 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
⊢ 𝓝 (↑(f.extend I) x) = 𝓝 (↑(f.extend I) x)

Tactic:
]

Goal state after:
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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I) '' (f.extend I).source ∈ map (↑(f.extend I)) (𝓝 y)

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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I) '' (f.extend I).source ∈ map (↑(f.extend I)) (𝓝 y)