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

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun x ↦ ⟨x, V x⟩) x
⊢ mlieBracketWithin I (f • V) W univ x =
    -(↑(fromTangentSpace (f x)) ∘SL mfderiv[univ] f x) (W x) • V x + f x • mlieBracket I V W x

Tactic:
]

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[univ] f x
hV : (MDiffAt[univ] fun x ↦ ⟨x, V x⟩) x
⊢ mlieBracketWithin I (f • V) W univ x =
    -(↑(fromTangentSpace (f x)) ∘SL mfderiv[univ] f x) (W x) • V x + f x • mlieBracket I V W x
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 |
      (fun x' ↦
          ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
            (fun x_2 ↦ ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_2⟩)
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x
A :
  ↑(extChartAt I x) ⁻¹'
      {x_1 |
        (fun x' ↦
            ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
              (fun x_2 ↦ ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_2⟩)
              ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
          x_1} ∈
    𝓝[↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)] x
y : M
hy : y ∈ s
⊢ y ∈ (extChartAt I x).source → y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Tactic:
h'y

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
T :
  {x_1 |
      (fun x' ↦
          ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
            (fun x_2 ↦ ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_2⟩)
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
        x_1} ∈
    𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s] ↑(extChartAt I x) x
A :
  ↑(extChartAt I x) ⁻¹'
      {x_1 |
        (fun x' ↦
            ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
              (fun x_2 ↦ ⟨x_2, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_2⟩)
              ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x')
          x_1} ∈
    𝓝[↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)] x
y : M
hy : y ∈ s
h'y : y ∈ (extChartAt I x).source
⊢ y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

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
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
x : M
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
y : M
hy : y ∈ (extChartAt I x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
⊢ V y = (ContinuousLinearMap.id 𝕜 (TangentSpace I y)).inverse (V y)

Tactic:
]

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
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
x : M
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
y : M
hy : y ∈ (extChartAt I x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
⊢ V y = (ContinuousLinearMap.id 𝕜 (TangentSpace I y)).inverse (V y)
Module: Mathlib.Topology.Homeomorph.TransferInstance

Goal state before:
pp: case e'_4
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ e.topologicalSpace = TopologicalSpace.induced (⇑e) inst✝

Tactic:
]

Goal state after:
case e'_4
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ e.topologicalSpace = TopologicalSpace.induced (⇑e) inst✝
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x

Tactic:
]

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + -mlieBracketWithin I W₁ V s x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt (T% W) x
hW₁ : MDiffAt (T% W₁) x
⊢ mlieBracketWithin I V (W + W₁) univ x = mlieBracketWithin I V W univ x + mlieBracketWithin I V W₁ univ x

Tactic:
exact mlieBracketWithin_add_right hW hW₁ (uniqueMDiffWithinAt_univ _)

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hs : UniqueMDiffAt[s] x
hV : MDiffAt (T% V) x
hW : MDiffAt (T% W) x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢
  exact mlieBracketWithin_subset (subset_univ _) hs hV hW

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffAt[t] x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x

Tactic:
]

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hVs : EqOn V₁ V t
hVx : V₁ x = V x
hW : MDiffAt[s] (T% W) x
hWs : EqOn W₁ W t
hWx : W₁ x = W x
hxt : UniqueMDiffAt[t] x
h₁ : t ⊆ s
⊢ mlieBracketWithin I V W t x = mlieBracketWithin I V W s x
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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' h.domChart.source ⊆ ↑(h.codChart.extend J) '' (h.codChart.extend J).source

Tactic:
]

Goal state after:
𝕜 : 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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ↑(h.codChart.extend J) '' f '' h.domChart.source ⊆ ↑(h.codChart.extend J) '' (h.codChart.extend J).source
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ (fun f ↦ f.ofLp i) ⁻¹' Ioi a = f ⁻¹' Ioi a

pp: case hf₂
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i

Tactic:
]

Goal state after:
case hf₂
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ (fun f ↦ f.ofLp i) ⁻¹' Ici a = f ⁻¹' Ici a

pp: case hfc
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i

Tactic:
]

Goal state after:
case hfc
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i
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
x : M
h : IsImmersionAtOfComplement F I J n f x
this : f '' h.domChart.source ⊆ h.codChart.source
⊢ ↑(h.codChart.extend J) '' h.codChart.source ⊆ ↑(h.codChart.extend J) '' h.codChart.source

Tactic:
]

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

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ {y | a ≤ y.ofLp i} \ {y | a < y.ofLp i} = {y | a = y.ofLp i}

Tactic:
]

Goal state after:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ {y | a ≤ y.ofLp i} \ {y | a < y.ofLp i} = {y | a = y.ofLp i}
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
⊢ ⋂ i, interior (f i ⁻¹' Ici a) = ⋂ i, f i ⁻¹' Ioi a

Tactic:
]

Goal state after:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
⊢ ⋂ i, interior (f i ⁻¹' Ici a) = ⋂ i, f i ⁻¹' Ioi a
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
i : Fin n
⊢ (fun f ↦ f.ofLp i) ⁻¹' Ioi a = f i ⁻¹' Ioi a

pp: case hf₂
n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
i : Fin n
⊢ Continuous fun f ↦ f.ofLp i

Tactic:
]

Goal state after:
case hf₂
n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
h' : {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a
i : Fin n
⊢ Continuous fun f ↦ f.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)).symm
      (update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0)) =
    xval

Tactic:
Equiv.symm_apply_eq,

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0) = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ max ((↑⟨xval, xprop⟩).ofLp 0) 0 = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval 0 ∧
    ∀ (x : Fin n), x ≠ 0 → (↑⟨xval, xprop⟩).ofLp x = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval x

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ max ((↑⟨xval, xprop⟩).ofLp 0) 0 = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval 0 ∧
    ∀ (x : Fin n), x ≠ 0 → (↑⟨xval, xprop⟩).ofLp x = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)).symm (update x✝.ofLp 0 (max (x✝.ofLp 0) 0)) = x✝

Tactic:
Equiv.symm_apply_eq,

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ update x✝.ofLp 0 (max (x✝.ofLp 0) 0) = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) x✝
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ max (x✝.ofLp 0) 0 = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) x✝ 0 ∧
    ∀ (x : Fin n), x ≠ 0 → x✝.ofLp x = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) x✝ x

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ max (x✝.ofLp 0) 0 = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) x✝ 0 ∧
    ∀ (x : Fin n), x ≠ 0 → x✝.ofLp x = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) x✝ x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Convex ℝ {y | 0 ≤ y.ofLp 0}

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Convex ℝ {y | 0 ≤ y.ofLp 0}
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ {y | 0 < y.ofLp 0}.Nonempty

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ {y | 0 < y.ofLp 0}.Nonempty
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
⊢ Convex ℝ {y | ∀ (i : Fin n), 0 ≤ y.ofLp i}

Tactic:
]

Goal state after:
n : ℕ
⊢ Convex ℝ {y | ∀ (i : Fin n), 0 ≤ y.ofLp i}
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
⊢ {y | ∀ (i : Fin n), 0 < y.ofLp i}.Nonempty

Tactic:
]

Goal state after:
n : ℕ
⊢ {y | ∀ (i : Fin n), 0 < y.ofLp i}.Nonempty
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x) = z

Tactic:
]

Goal state after:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x) = z
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x + z.ofLp 0 ≤ y
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp 0 = z.ofLp 0

Tactic:
]

Goal state after:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x + z.ofLp 0 ≤ y
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp 0 = z.ofLp 0
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ 0 = 0

Tactic:
]

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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContinuousOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (h.domChart.extend I).target

Tactic:
]

Goal state after:
𝕜 : 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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContinuousOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (h.domChart.extend I).target
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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target

Tactic:
]

Goal state after:
𝕜 : 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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target
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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContDiff 𝕜 n (⇑h.equiv ∘ fun x ↦ (x, 0))

Tactic:
]

Goal state after:
𝕜 : 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
x : M
h : IsImmersionAtOfComplement F I J n f x
⊢ ContDiff 𝕜 n (⇑h.equiv ∘ fun x ↦ (x, 0))
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩) = z

Tactic:
]

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩) = z
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp 0 = z.ofLp 0

Tactic:
]

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp 0 = z.ofLp 0