mathlib-initiative/mathlib-tactics huggingface dataset:
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
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ e.prod e' ∈ contDiffGroupoid n (I.prod I')

Tactic:
constructor

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
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e')) (e.prod e').source

case right
n : ℕ∞ω
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
E' : Type u_5
H' : Type u_6
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
inst✝ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
e : OpenPartialHomeomorph H H
e' : OpenPartialHomeomorph H' H'
he : (contDiffPregroupoid n I).property (↑e) e.source
he_symm : (contDiffPregroupoid n I).property (↑e.symm) e.target
he' : (contDiffPregroupoid n I').property (↑e') e'.source
he'_symm : (contDiffPregroupoid n I').property (↑e'.symm) e'.target
⊢ (contDiffPregroupoid n (I.prod I')).property (↑(e.prod e').symm) (e.prod e').target
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
⊢ (extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
convert! extChartAt_target_mem_nhdsWithin x
  simp only [I.range_eq_univ, nhdsWithin_univ]

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

Goal state before:
pp: H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f) s x ↔
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

Tactic:
constructor

Goal state after:
case mp
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
⊢ G.IsLocalStructomorphWithinAt (↑f) s x →
    x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source

case mpr
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : OpenPartialHomeomorph H H
s : Set H
x : H
hx : x ∈ f.source ∪ sᶜ
⊢ (x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source) →
    G.IsLocalStructomorphWithinAt (↑f) s 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
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ HasGroupoid M (contDiffGroupoid 0 I)

Tactic:
constructor

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
n : ℕ∞ω
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ∀ {e e' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e' ∈ contDiffGroupoid 0 I
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
n : ℕ∞ω
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 3 M
⊢ 2 ≤ 3

Tactic:
by norm_cast

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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I') ∧
    (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod I')

Tactic:
constructor

Goal state after:
case left
𝕜 : 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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ (e.symm ≫ₕ f).prod (e'.symm ≫ₕ f') ∈ contDiffGroupoid n (I.prod I')

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
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
n : ℕ∞ω
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
e : OpenPartialHomeomorph M H
he : e ∈ maximalAtlas I n M
e' : OpenPartialHomeomorph M' H'
he' : e' ∈ maximalAtlas I' n M'
f : OpenPartialHomeomorph M H
hf : f ∈ atlas H M
f' : OpenPartialHomeomorph M' H'
hf' : f' ∈ atlas H' M'
⊢ (f.symm ≫ₕ e).prod (f'.symm ≫ₕ e') ∈ contDiffGroupoid n (I.prod 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 : ContDiffWithinAtProp I I' m f s x
⊢ ContDiffWithinAtProp I I' m (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)

Tactic:
rw [ContDiffWithinAtProp] at h ⊢

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 x)
⊢ ContDiffWithinAt 𝕜 m (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' ↑e.symm ⁻¹' s ∩ range ↑I) (↑I (↑e x))
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'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAtProp I I' m f s x
⊢ ContDiffWithinAtProp I I' m (↑e' ∘ f) s x

Tactic:
rw [ContDiffWithinAtProp] at h ⊢

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'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : ContDiffWithinAt 𝕜 m (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
⊢ ContDiffWithinAt 𝕜 m (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
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 : ContMDiff I J n (Sum.inl ∘ f)
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x ↦ default
⊢ aux ∘ Sum.inl ∘ f = f

Tactic:
ext

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 : ContMDiff I J n (Sum.inl ∘ f)
a✝ : Nontrivial N
inhabited_h : Inhabited N
aux : N ⊕ N' → N := Sum.elim id fun x ↦ default
x✝ : M
⊢ (aux ∘ Sum.inl ∘ f) x✝ = f x✝
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 : ContMDiff I J n (Sum.inr ∘ g)
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x ↦ default) id
⊢ aux ∘ Sum.inr ∘ g = g

Tactic:
ext

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 : ContMDiff I J n (Sum.inr ∘ g)
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x ↦ default) id
x✝ : M'
⊢ (aux ∘ Sum.inr ∘ g) x✝ = g x✝
Module: Mathlib.Geometry.Manifold.ContMDiff.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
e : M → H
h : IsOpenEmbedding e
n : ℕ∞ω
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm) (range e) ∧
    ∀ (x : H) (y : M),
      ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩
          ↑(extChartAt I x).symm ⁻¹'
            (range e ∩ ↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))

Tactic:
constructor

Goal state after:
case left
𝕜 : 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
⊢ ContinuousOn (↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm) (range e)

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 : H) (y : M),
    ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩
        ↑(extChartAt I x).symm ⁻¹'
          (range e ∩ ↑(IsOpenEmbedding.toOpenPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))
Module: Mathlib.Geometry.Manifold.ContMDiff.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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
n : ℕ∞ω
inst✝¹ : ChartedSpace H M
inst✝ : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
⊢ f = ↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm ∘ e' ∘ f

Tactic:
ext

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
n : ℕ∞ω
inst✝¹ : ChartedSpace H M
inst✝ : Nonempty M'
e' : M' → H'
h' : IsOpenEmbedding e'
f : M → M'
hf : ContMDiff I I' n (e' ∘ f)
x✝ : M
⊢ f x✝ = (↑(IsOpenEmbedding.toOpenPartialHomeomorph e' h').symm ∘ e' ∘ f) x✝
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
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
constructor

Goal state after:
case mp
𝕜 : 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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiffOn I I' n f s →
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

case mpr
𝕜 : 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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
s : Set M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))) →
    ContMDiffOn I I' n f s
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
G : Type u_4
inst✝⁸ : Mul G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : ContinuousMul G
⊢ ContMDiffMul I 0 G

Tactic:
constructor

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
G : Type u_4
inst✝⁸ : Mul G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : ContinuousMul G
⊢ ContMDiff (I.prod I) I 0 fun p ↦ p.1 * p.2
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h : G
⊢ 𝑳 I (g * h) = (𝑳 I g).comp (𝑳 I h)

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑳 I (g * h)) x✝ = ((𝑳 I g).comp (𝑳 I h)) x✝
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h : G
⊢ 𝑹 I (g * h) = (𝑹 I h).comp (𝑹 I g)

Tactic:
ext

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_8
inst✝³ : Semigroup G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I ∞ G
g h x✝ : G
⊢ (𝑹 I (g * h)) x✝ = ((𝑹 I h).comp (𝑹 I g)) x✝
Module: Mathlib.Geometry.Manifold.Algebra.Monoid

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiffAdd 𝓘(𝕜, E) n E

Tactic:
constructor

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n fun p ↦ p.1 + p.2
Module: Mathlib.Geometry.Manifold.Algebra.LieGroup

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : IsTopologicalGroup G
⊢ LieGroup I 0 G

Tactic:
constructor

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
n : ℕ∞ω
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : IsTopologicalGroup G
⊢ ContMDiff I I 0 fun a ↦ a⁻¹