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 : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x_1 : H) in 𝓝 (↑(chartAt H x) x), x_1 ∈ ↑(chartAt H x).symm ⁻¹' (s ∩ t) ↔ x_1 ∈ ↑(chartAt H x).symm ⁻¹' s

Tactic:
mem_preimage,

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 : M → M'
s t : Set M
x : M
hG : G.LocalInvariantProp G' P
ht : t ∈ 𝓝[s] x
⊢ ∀ᶠ (x_1 : H) in 𝓝 (↑(chartAt H x) x), ↑(chartAt H x).symm x_1 ∈ s ∩ t ↔ ↑(chartAt H x).symm x_1 ∈ s
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst✝¹] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source) ∧ x ∈ e.source

Tactic:
rcases h hx.1 with ⟨e, heG, hef, hex⟩

Goal state after:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
s : Set H
x : H
u : Set H
f : H → H
hu : IsOpen[inst✝¹] u
hux : x ∈ u
h : G.IsLocalStructomorphWithinAt f s x
hx : x ∈ s ∩ u
e : OpenPartialHomeomorph H H
heG : e ∈ G
hef : EqOn f (↑e.toPartialEquiv) (s ∩ e.source)
hex : x ∈ e.source
⊢ ∃ e ∈ G, EqOn f (↑e.toPartialEquiv) (s ∩ u ∩ e.source) ∧ x ∈ e.source
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case inr.inl.inl
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : f' ∈ atlas H M
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
rw [hef, he'f', f.lift_openEmbedding_trans f' IsOpenEmbedding.inl]

Goal state after:
case inr.inl.inl
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : f' ∈ atlas H M
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ f.symm ≫ₕ f' ∈ contDiffGroupoid n I
Module: Mathlib.Geometry.Manifold.IsManifold.Basic

Goal state before:
pp: case inr.inl.inr
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : f' ∈ atlas H M'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
· rw [hef, he'f']
        apply ContDiffGroupoid.mem_of_source_eq_empty
        ext x
        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩

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

Goal state before:
pp: E : Type u_8
𝕜 : Type u_9
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁴ : TopologicalSpace H
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝¹ : LocallyCompactSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
this✝ : ProperSpace E
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
exact ChartedSpace.locallyCompactSpace H M

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

Goal state before:
pp: case inr.inr.inl
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : f ∈ atlas H M'
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M H
hf' : f' ∈ atlas H M
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

pp: case inr.inr.inr
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : f ∈ atlas H M'
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : f' ∈ atlas H M'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I

Tactic:
· rw [hef, he'f']
        apply ContDiffGroupoid.mem_of_source_eq_empty
        ext x
        exact ⟨fun ⟨hx₁, hx₂⟩ ↦ by simp_all, fun hx ↦ hx.elim⟩

Goal state after:
case inr.inr.inr
𝕜 : 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
n : ℕ∞ω
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
hM : IsManifold I n M
hM' : IsManifold I n M'
e e' : OpenPartialHomeomorph (M ⊕ M') H
he : e ∈ atlas H (M ⊕ M')
he' : e' ∈ atlas H (M ⊕ M')
h : Nonempty H
f : OpenPartialHomeomorph M' H
hf : f ∈ atlas H M'
hef : e = f.lift_openEmbedding ⋯
f' : OpenPartialHomeomorph M' H
hf' : f' ∈ atlas H M'
he'f' : e' = f'.lift_openEmbedding ⋯
⊢ e.symm ≫ₕ e' ∈ contDiffGroupoid n I
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I
this : ContDiffWithinAt 𝕜 n (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))
⊢ ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target

Tactic:
mem_preimage,

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n m : ℕ∞ω
hmn : m ≤ n
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid n I
hx : x ∈ e.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))
this✝¹ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))
this✝ : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I
this : ContDiffWithinAt 𝕜 n (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I.symm ⁻¹' e.target ∩ range ↑I) (↑I (↑e x))
⊢ ↑I.symm (↑I (↑e x)) ∈ e.target
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
n : WithTop ℕ∞
f : M → F₁ × F₂
⊢ ContMDiff I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) n f ↔
    ContMDiff I 𝓘(𝕜, F₁) n (Prod.fst ∘ f) ∧ ContMDiff I 𝓘(𝕜, F₂) n (Prod.snd ∘ f)

Tactic:
exact contMDiff_prod_iff f

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
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
hf : InjOn f s
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)

Tactic:
intro n; exact hs.inter (u_meas n)

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

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 : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : x ∈ univ
⊢ x ∈ Sum.inl ∘ f ⁻¹' Sum.inl '' univ

Tactic:
mem_preimage,

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 : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
f : M → N
h : ContMDiffOn I J n (Sum.inl ∘ f) univ
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x ↦ default
this : aux ∘ Sum.inl ∘ f = f
x : M
_hx : x ∈ univ
⊢ (Sum.inl ∘ f) x ∈ Sum.inl '' univ
Module: Mathlib.Geometry.Manifold.ContMDiff.Constructions

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_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J n (Sum.inr ∘ g) univ
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : x ∈ univ
⊢ x ∈ Sum.inr ∘ g ⁻¹' Sum.inr '' univ

Tactic:
mem_preimage,

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_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J n (Sum.inr ∘ g) univ
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x ↦ default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : x ∈ univ
⊢ (Sum.inr ∘ g) x ∈ Sum.inr '' univ
Module: Mathlib.Geometry.Manifold.ContMDiff.Basic

Goal state before:
pp: case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this✝¹ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' e ⁻¹' (extChartAt I y).source
this✝ : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : z ∈ ↑I.symm ⁻¹' (chartAt H x).target
⊢ ↑I.symm z ∈ range e

Tactic:
mem_preimage,

Goal state after:
case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this✝¹ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' e ⁻¹' (extChartAt I y).source
this✝ : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : ↑I.symm z ∈ (chartAt H x).target
⊢ ↑I.symm z ∈ range e
Module: Mathlib.Geometry.Manifold.MFDeriv.Defs

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAtProp I I' f s x
⊢ DifferentiableWithinAtProp I I' (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
DifferentiableWithinAtProp

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e : OpenPartialHomeomorph H H
he : e ∈ contDiffGroupoid 1 I
hx : x ∈ e.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' ↑e.symm ⁻¹' s ∩ range ↑I) (↑I (↑e x))
Module: Mathlib.Geometry.Manifold.MFDeriv.Defs

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAtProp I I' f s x
⊢ DifferentiableWithinAtProp I I' (↑e' ∘ f) s x

Tactic:
DifferentiableWithinAtProp

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
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : OpenPartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I 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)
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
heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source
he : e.source = (Prod.fst '' e.source) ×ˢ univ
⊢ ∀ x ∈ Prod.fst '' e.source,
    ∃ φ u,
      ∃ (hu : IsOpen[inst✝⁷] u) (_ : u ⊆ Prod.fst '' e.source) (_ : 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:
rintro x ⟨p, hp, rfl⟩

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
heu : ∀ (p : ↑e.source) (q : B × F), q.1 ∈ u p → q ∈ e.source
he : e.source = (Prod.fst '' e.source) ×ˢ univ
p : B × F
hp : p ∈ e.source
⊢ ∃ φ u,
    ∃ (hu : IsOpen[inst✝⁷] u) (_ : u ⊆ Prod.fst '' e.source) (_ : p.1 ∈ 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.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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
⊢ ContMDiffWithinAt I I n (↑f) (f ≫ₕ c').source (↑(extChartAt I x).symm y)

Tactic:
refine (h₁ ((extChartAt I x).symm y) ?_).mono ?_

Goal state after:
case refine_1
𝕜 : 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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
⊢ ↑(extChartAt I x).symm y ∈ f.source

case refine_2
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
n : ℕ∞ω
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₁ : ContMDiffOn I I n (↑f) f.source
h₂ : ContMDiffOn I I n (↑f.symm) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H (↑f x)
hx' : ↑c x ∈ ↑c.symm ⁻¹' f.source
y : E
hy : ((↑I.symm y ∈ c.target ∧ ↑c.symm (↑I.symm y) ∈ f.source) ∧ ↑f (↑c.symm (↑I.symm y)) ∈ c'.source) ∧ y ∈ range ↑I
⊢ (f ≫ₕ c').source ⊆ f.source