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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
⊢ ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
⊢ f (↑hf.localInverse.toPartialEquiv y) = y

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (f x') = x'

Tactic:
by

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

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 : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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 : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ { toFun := fun g ↦ v (ContMDiffMap.comp g f), map_add' := ⋯, map_smul' := ⋯ } (g * g') =
    g • { toFun := fun g ↦ v (ContMDiffMap.comp g f), map_add' := ⋯, map_smul' := ⋯ } g' +
      g' • { toFun := fun g ↦ v (ContMDiffMap.comp g f), map_add' := ⋯, map_smul' := ⋯ } g

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
g : N → P
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
Ψ : PartialDiffeomorph J K N P n
hy : f x ∈ Ψ.source
heq' : EqOn g (↑Ψ.toPartialEquiv) Ψ.source
⊢ x ∈ (Φ.trans Ψ).source

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
g : N → P
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
Ψ : PartialDiffeomorph J K N P n
hy : f x ∈ Ψ.source
heq' : EqOn g (↑Ψ.toPartialEquiv) Ψ.source
y : M
hyl : y ∈ Φ.toOpenPartialHomeomorph.symm.target
hyr : y ∈ ↑Φ.toOpenPartialHomeomorph.symm.symm ⁻¹' Ψ.toOpenPartialHomeomorph.source
⊢ f y ∈ Ψ.source

Tactic:
heq.eq_of_mem hyl

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
g : N → P
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
Ψ : PartialDiffeomorph J K N P n
hy : f x ∈ Ψ.source
heq' : EqOn g (↑Ψ.toPartialEquiv) Ψ.source
y : M
hyl : y ∈ Φ.toOpenPartialHomeomorph.symm.target
hyr : y ∈ ↑Φ.toOpenPartialHomeomorph.symm.symm ⁻¹' Ψ.toOpenPartialHomeomorph.source
⊢ ↑Φ.toPartialEquiv y ∈ Ψ.source
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
g : N → P
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
Ψ : PartialDiffeomorph J K N P n
hy : f x ∈ Ψ.source
heq' : EqOn g (↑Ψ.toPartialEquiv) Ψ.source
y : M
hyl : y ∈ Φ.toOpenPartialHomeomorph.symm.target
hyr : y ∈ ↑Φ.toOpenPartialHomeomorph.symm.symm ⁻¹' Ψ.toOpenPartialHomeomorph.source
⊢ f y ∈ Ψ.source

Tactic:
by

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

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
x : M
⊢ I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
g : N → P
hg : IsLocalDiffeomorphAt J K n g (f x)
⊢ IsLocalDiffeomorphAt I K n (g ∘ f) x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
s : Set M
⊢ IsLocalDiffeomorphOn I J n f s ↔ ∀ (x : ↑s), IsLocalDiffeomorphAt I J n f ↑x

Tactic:
by

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

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
⊢ Disjoint (ModelWithCorners.interior M) (ModelWithCorners.boundary M)

Tactic:
by

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

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
x : M
⊢ ¬I.IsBoundaryPoint x → I.IsInteriorPoint x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
⊢ IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x

Tactic:
by

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

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
x : M
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

Tactic:
by

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

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
x : M
⊢ I.IsBoundaryPoint x ↔ ¬I.IsInteriorPoint x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
⊢ ContMDiffAt I J n f x

Tactic:
by

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

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
⊢ (ModelWithCorners.interior M)ᶜ = ModelWithCorners.boundary M

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
Φ : M ≃ₘ^n⟮I, J⟯ N
_x : M
⊢ _x ∈ Φ.toPartialDiffeomorph.source

Tactic:
by

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

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
⊢ (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M

Tactic:
by

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

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
x : M
h : I.IsInteriorPoint x
⊢ range ↑I ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
⊢ ∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t

Tactic:
by

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

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
inst✝ : I.Boundaryless
x : M
⊢ I.IsInteriorPoint x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p

Tactic:
by

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

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
inst✝ : BoundarylessManifold I M
⊢ ModelWithCorners.boundary M = ∅

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ IsLocalHomeomorphOn f s

Tactic:
by

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

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
⊢ ModelWithCorners.boundary M = ∅ ↔ BoundarylessManifold I M

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
⊢ affineSpan ℝ s = affineSpan ℝ (Set.range t.points)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorph f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
⊢ FiniteDimensional ℝ ↥(affineSpan ℝ s).direction

Tactic:
by

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

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
⊢ ¬Surjective ⇑(fderiv ℝ f x)

Tactic:
by

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

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
⊢ MapsTo (⇑F) s (Iic (F (f x)))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ affineSpan ℝ (Set.range p) = affineSpan ℝ s

Tactic:
by

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

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
hFφ : IsLocalMax (⇑F ∘ f) x
h : fderiv ℝ (⇑F ∘ f) x = 0
⊢ DifferentiableAt ℝ (⇑F) (f x)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
Φ : M → PartialDiffeomorph I J M N n
hyp : ∀ (x : M), x ∈ (Φ x).source ∧ EqOn f (↑(Φ x).toPartialEquiv) (Φ x).source
aux : ∀ (x : M), EqOn g (↑(Φ x).symm.toPartialEquiv) (Φ x).target
⊢ ContMDiff J I n ⇑{ toFun := f, invFun := g, left_inv := ⋯, right_inv := ⋯ }.symm

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
by

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

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : Surjective ⇑(fderiv ℝ f x)
⊢ f x ∈ interior s

Tactic:
by

Goal state after: