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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : Nonempty M
inhabited_h : Inhabited M
x : M := default
⊢ NormedAddCommGroup ⋯.smallComplement

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
i : Fin 1
⊢ ContDiff ℝ n fun x ↦ (toLp 2 fun x_1 ↦ y - x).ofLp i

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
hM : Nonempty M
inhabited_h : Inhabited M
x : M := default
⊢ NormedSpace 𝕜 ⋯.smallComplement

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
⊢ ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersionOfComplement F I J n f
⊢ IsImmersion I J n f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this✝ :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
this : y - max x (min y w) = y - w
⊢ (((Subtype.val ∘ ↑(IccRightChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w).ofLp i =
    (have this := toLp 2 fun x ↦ y - w;
        this).ofLp
      i

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (𝓡∂ 1) n (projIcc x y ⋯) (Icc x y)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↔ ContMDiff (𝓡∂ 1) I n f

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I (↑(chartAt H x) (↑(chartAt H x).symm (↑I.symm y))) = y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : ContMDiffAt (𝓡∂ 1) I n f w
⊢ projIcc x y ⋯ ↑w = w

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ IsImmersionOfComplement PUnit.{u_15 + 1} I I n id

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
⊢ ContinuousAt Sum.inl x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
w : ↑(Icc x y)
⊢ ContMDiffWithinAt 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↑w ↔ ContMDiffAt (𝓡∂ 1) I n f w

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I (↑(chartAt H x) (↑(chartAt H x).symm (↑I.symm y))) = y

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
⊢ IsImmersionOfComplement Unit I I n Sum.inl

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M'
⊢ ContinuousAt Sum.inr x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hf : MDiffAt f w
this : MDiffAt[Icc x y] (projIcc x y ⋯) ↑w
⊢ projIcc x y ⋯ ↑w = w

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M'
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) ↑w ↔ MDiffAt f w

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M'
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
x : M'
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I (↑(chartAt H x) (↑(chartAt H x).symm (↑I.symm y))) = y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
⊢ IsImmersionOfComplement Unit I I n Sum.inr

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
⊢ ContMDiff I J n f ↔ Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersion I J n f
x : M
⊢ NormedAddCommGroup h.complement

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersion I J n f
x : M
⊢ NormedSpace 𝕜 h.complement

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsImmersion I J n f
x : M
⊢ IsImmersionAt I J n f x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ NormedAddCommGroup PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ NormedSpace 𝕜 PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ IsImmersion I I n id

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ NormedAddCommGroup PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ NormedSpace 𝕜 PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsImmersion I I n Subtype.val

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
⊢ IsImmersion I I n Subtype.val

Tactic:
by
  use PUnit, by infer_instance, by infer_instance
  exact IsImmersionOfComplement.of_opens s

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_7
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ
⊢ NormedAddCommGroup PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_7
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ
⊢ NormedSpace 𝕜 PUnit.{u_2 + 1}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_7
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : ℕ
⊢ IsImmersion I 𝓘(𝕜, E) ↑n ↑I

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
inst✝¹⁰ : NormedAddCommGroup E'''
inst✝⁹ : NormedSpace 𝕜 E'''
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersion J J' n φ
⊢ ContMDiff I J n f ↔ Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ w = projIcc x y ⋯ ↑w

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ContDiffOn ℝ n (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : E
hw : w ∈ (ℝ ∙ v)ᗮ
⊢ 0 < ‖w‖ ^ 2 + 4

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : E
hw : w ∈ (ℝ ∙ v)ᗮ
h₁ : 0 < ‖w‖ ^ 2 + 4
this : ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4
⊢ stereoInvFunAux v w ∈ sphere 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : E
hw : w ∈ (ℝ ∙ v)ᗮ
h₁ : 0 < ‖w‖ ^ 2 + 4
this : ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2
⊢ ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : E
hw : w ∈ (ℝ ∙ v)ᗮ
⊢ stereoInvFunAux v w ∈ sphere 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0

Tactic:
convert! (hasStrictFDerivAt_norm_sq (0 : E)).hasFDerivAt

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ 0 = 2 • (innerSL ℝ) 0
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0
⊢ HasFDerivAt (fun w ↦ (‖w‖ ^ 2 + 4)⁻¹) 0 0

Tactic:
by

Goal state after: