mathlib-initiative/mathlib-tactics huggingface dataset:
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
e e' : OpenPartialHomeomorph M H
⊢ (extendCoordChange e e').target = ↑I '' (e.symm ≫ₕ e').target

Tactic:
by

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 f' : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ↑(f.extend I) '' (f.source ∩ f'.source) = (extendCoordChange f f').source

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
f : OpenPartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
hf : f ∈ maximalAtlas M' G'
h : LiftPropOn P g s
y : H
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y

Tactic:
by

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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ (extendCoordChange e e').source ∈ 𝓝[range ↑I] x

Tactic:
by

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
I : ModelWithCorners 𝕜 E H
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x) ↔ ContinuousWithinAt f s x

Tactic:
by

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
I : ModelWithCorners 𝕜 E H
X : Type u_4
inst✝ : TopologicalSpace X
f : H → X
s : Set H
x : H
⊢ ContinuousWithinAt (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x) ↔ ContinuousWithinAt f s x

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
    simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range,
      inter_univ] at this
    rwa [Function.comp_assoc, I.symm_comp_self] at this
  · rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm inter_subset_left

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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ (extendCoordChange e e').source ∈ 𝓝[range ↑I] ↑(e.extend I) x

Tactic:
by

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
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s ↦ ↑I.symm '' (s ∩ range ↑I)

Tactic:
rw [← I.symm_map_nhdsWithin_range]

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
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (map (↑I.symm) (𝓝[range ↑I] ↑I x)).HasBasis (fun s ↦ s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s ↦ ↑I.symm '' (s ∩ 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
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn 𝕜 (extendCoordChange e e').source

Tactic:
by

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
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
x : H
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (↑I x) ∧ IsCompact s) fun s ↦ ↑I.symm '' (s ∩ range ↑I)

Tactic:
by

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
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ UniqueDiffOn 𝕜 (extendCoordChange e e').target

Tactic:
by

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
inst✝ : LocallyCompactSpace E
I : ModelWithCorners 𝕜 E H
⊢ LocallyCompactSpace H

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x

Tactic:
by

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
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ T1Space M

Tactic:
by

Goal state after:
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
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ {x | x.1 ∈ I.source ∧ x.2 ∈ I'.source} = univ

Tactic:
by

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(extendCoordChange e e')) (extendCoordChange e e').source

Tactic:
by

Goal state after:
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),
    ∃ δ,
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑δ → |B.det - A.det| ≤ ↑ε) ∧
          ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
hu : s =ᶠ[𝓝 x] t
⊢ LiftPropWithinAt P g s x ↔ LiftPropWithinAt P g t x

Tactic:
by

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : E
hx : x ∈ (extendCoordChange e e').source
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange e e')) (range ↑I) x

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropWithinAt P g s x
hs : s ∈ 𝓝 x
⊢ LiftPropAt P g x

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
h : LiftPropAt P g x
hs : s ∈ 𝓝 x
⊢ LiftPropWithinAt P g s x

Tactic:
by

Goal state after:
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
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range fun x ↦ (↑I x.1, ↑I' x.2))
  else (range fun x ↦ (↑I x.1, ↑I' x.2)) = univ

Tactic:
by

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
n : WithTop ℕ∞
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
inst✝ : ChartedSpace H M
he : e ∈ maximalAtlas I n M
he' : e' ∈ maximalAtlas I n M
x : M
hxe : x ∈ e.source
hxe' : x ∈ e'.source
⊢ ContDiffWithinAt 𝕜 n (↑(extendCoordChange e e')) (range ↑I) (↑(e.extend I) x)

Tactic:
by

Goal state after:
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 < ε
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) → ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ↑ε * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ s = ⋃ n, s ∩ t n

Tactic:
by

Goal state after:
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
E' : Type v'
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type w'
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
⊢ (interior (range fun x ↦ (↑I x.1, ↑I' x.2))).Nonempty

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ (PartialEquiv.pi fun i ↦ (I i).toPartialEquiv).source = univ

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
hG : G.LocalInvariantProp G' P
h : ∀ x ∈ s, ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ LiftPropOn P g (s ∩ u)
⊢ LiftPropOn P g s

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftProp P g

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ if h : IsRCLikeNormedField 𝕜 then Convex ℝ (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))
  else range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv) = univ

Tactic:
by

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'
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
⊢ (↑(chartAt H' (g' x)) ∘ g' ∘ ↑(chartAt H x).symm) (↑(chartAt H x) x) =
    (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x) x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
ι : Type v
inst✝³ : Fintype ι
E : ι → Type w
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
H : ι → Type u'
inst✝ : (i : ι) → TopologicalSpace (H i)
I : (i : ι) → ModelWithCorners 𝕜 (E i) (H i)
⊢ (interior (range ↑(PartialEquiv.pi fun i ↦ (I i).toPartialEquiv))).Nonempty

Tactic:
by

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'
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:
by

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'
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
⊢ LiftPropWithinAt P g' s x

Tactic:
by

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'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
x : M
hG : G.LocalInvariantProp G' P
h₁ : g' =ᶠ[𝓝 x] g
⊢ g' =ᶠ[𝓝[univ] x] g

Tactic:
by

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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ 𝓘(𝕜, E × F) = 𝓘(𝕜, E).prod 𝓘(𝕜, F)

Tactic:
by

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 t : Set M
x : M
mono_of_mem_nhdsWithin : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x
h : LiftPropWithinAt P g s x
hst : s ∈ 𝓝[t] x
⊢ LiftPropWithinAt P g t x

Tactic:
by

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
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹ : TopologicalSpace H
G : Type u_7
inst✝ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ range ↑(I.prod J) = range ↑I ×ˢ range ↑J

Tactic:
by

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 t : 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 s x
hts : t ⊆ s
⊢ LiftPropWithinAt P g t x

Tactic:
by

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
⊢ range ↑𝓘(𝕜, E) = univ

Tactic:
by

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 : LiftPropAt P g x
⊢ LiftPropWithinAt P g s x

Tactic:
by

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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftProp P g
⊢ LiftPropOn P g s

Tactic:
by

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
x : M
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ ContinuousWithinAt (↑e) univ x ∧ Q (↑(OpenPartialHomeomorph.refl H) ∘ ↑e ∘ ↑e.symm) (↑e.symm ⁻¹' univ) (↑e x)

Tactic:
(e.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
x : M
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ True ∧ Q (↑(OpenPartialHomeomorph.refl H) ∘ ↑e ∘ ↑e.symm) (↑e.symm ⁻¹' univ) (↑e 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
x : M
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
hx : x ∈ e.source
⊢ LiftPropAt Q (↑e) x

Tactic:
by

Goal state after:
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
⊢ (I.prod I').Boundaryless

Tactic:
by

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
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
he : e ∈ maximalAtlas M G
⊢ LiftPropOn Q (↑e) e.source

Tactic:
by

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
⊢ ↑e.symm x ∈ e.source

Tactic:
by

Goal state after: