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

Goal state before:
pp: case refine_1
𝕜✝ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝²⁰ : NormedAddCommGroup E✝
inst✝¹⁹ : NormedSpace 𝕜✝ E✝
H✝ : Type u_3
inst✝¹⁸ : TopologicalSpace H✝
I✝ : ModelWithCorners 𝕜✝ E✝ H✝
M✝ : Type u_4
inst✝¹⁷ : TopologicalSpace M✝
inst✝¹⁶ : ChartedSpace H✝ M✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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 : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ (extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)]

Goal state after:
case refine_1
𝕜✝ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝²⁰ : NormedAddCommGroup E✝
inst✝¹⁹ : NormedSpace 𝕜✝ E✝
H✝ : Type u_3
inst✝¹⁸ : TopologicalSpace H✝
I✝ : ModelWithCorners 𝕜✝ E✝ H✝
M✝ : Type u_4
inst✝¹⁷ : TopologicalSpace M✝
inst✝¹⁶ : ChartedSpace H✝ M✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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 : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ (extChartAt I x).target ∈ 𝓝[range ↑I] ↑(extChartAt I x) x
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ ∀ y ∈ t.baseSet, (fun x_1 ↦ (↑t ⟨x_1, extend F σ₀ x_1⟩).2) y = (fun _x ↦ w) y

pp: case refine_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
· intro x hx
    simp [extend, t, hx, w]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

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_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) = ((mfderiv% fun x ↦ h * x) 1) v

Tactic:
rw [D, mfderiv_comp (I' := I)]

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_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ ((mfderiv% fun b ↦ g⁻¹ * b) (g * h)) (((mfderiv% fun x ↦ g * h * x) 1) v) =
    ((mfderiv% fun b ↦ g⁻¹ * b) (g * h * 1) ∘SL (mfderiv% fun x ↦ g * h * x) 1) v

case hg
𝕜 : 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_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun b ↦ g⁻¹ * b) (g * h * 1)

case hf
𝕜 : 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_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
h : G
D : (fun x ↦ h * x) = (fun b ↦ g⁻¹ * b) ∘ fun x ↦ g * h * x
⊢ (MDiffAt fun x ↦ g * h * x) 1
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hs
𝕜 : 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 V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffAt[s] x
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
· exact uniqueMDiffWithinAt_iff_inter_range.1 hs

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 V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffAt[s] x
⊢ mlieBracketWithin I (V + V₁) W s x = mlieBracketWithin I V W s x + mlieBracketWithin I V₁ W s x

Tactic:
by
  simp only [mlieBracketWithin_apply]
  rw [← map_add, mpullbackWithin_add, lieBracketWithin_add_left]
  · exact hV.differentiableWithinAt_mpullbackWithin_vectorField
  · exact hV₁.differentiableWithinAt_mpullbackWithin_vectorField
  · exact uniqueMDiffWithinAt_iff_inter_range.1 hs

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

Goal state before:
pp: case e_6.hs
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

pp: case e_6.hV
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

pp: case e_6.hW
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
· exact uniqueMDiffWithinAt_iff_inter_range.1 hs

Goal state after:
case e_6.hV
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)

case e_6.hW
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) 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
F' : Type u_6
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup E''
inst✝¹⁰ : NormedSpace 𝕜 E''
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
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
e : F ≃L[𝕜] F'
⊢ IsImmersionAtOfComplement F' I J n f x

Tactic:
refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
    h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
F' : Type u_6
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
inst✝¹¹ : NormedAddCommGroup E''
inst✝¹⁰ : NormedSpace 𝕜 E''
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
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
e : F ≃L[𝕜] F'
⊢ ImmersionAtProp F' I J M N f h.domChart h.codChart
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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 : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
e e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he : e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y)
⊢ e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
    ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))

Tactic:
he'

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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 : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
e e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he : e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y)
he' : e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R) n (val ∘ fun p ↦ p.1 * p.2)

Tactic:
have : (val : Rˣ → R) ∘ (fun x : Rˣ × Rˣ => x.1 * x.2) =
      (fun x : R × R => x.1 * x.2) ∘ (fun x : Rˣ × Rˣ => (x.1, x.2)) := by ext; simp

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : (val ∘ fun x ↦ x.1 * x.2) = (fun x ↦ x.1 * x.2) ∘ fun x ↦ (↑x.1, ↑x.2)
⊢ ContMDiff (𝓘(𝕜, R).prod 𝓘(𝕜, R)) 𝓘(𝕜, R) n (val ∘ fun p ↦ p.1 * p.2)
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
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ ((|2| / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ * (((|2| / (1 - a) * ‖y‖) ^ 2 - 4) * 1) = a * 1

Tactic:
field_simp
    linear_combination 4 * (a - 1) * pythag

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: case neg
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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
hmem : t ∉ Ioo a b
⊢ (Ioo a b).piecewise γ γ' t = γ' t

Tactic:
· rw [piecewise, if_neg hmem]

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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
inst✝ : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ Disjoint (Icc a b) (Ioc b c)

Tactic:
exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ mfderiv[Icc a b] (γ ∘ f) t = mfderiv[Icc (f a) (f b)] γ (f t) ∘SL mfderiv[Icc a b] f t

Tactic:
← f_im

Goal state after:
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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ mfderiv[Icc a b] (γ ∘ f) t = mfderiv[f '' Icc a b] γ (f t) ∘SL mfderiv[Icc a b] f t
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ mfderiv[Icc a b] (γ ∘ f) t = mfderiv[Icc (f b) (f a)] γ (f t) ∘SL mfderiv[Icc a b] f t

Tactic:
← f_im

Goal state after:
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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ mfderiv[Icc a b] (γ ∘ f) t = mfderiv[f '' Icc a b] γ (f t) ∘SL mfderiv[Icc a b] f t
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
⊢ ∃ C > 0, ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C

Tactic:
rcases eventually_norm_mfderivWithin_symm_extChartAt_lt I x with ⟨C, C_pos, hC⟩

Goal state after:
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
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < C
⊢ ∃ C > 0, ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C