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

Goal state before:
pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

pp: 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
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (minSmoothness 𝕜 3) (fun x ↦ g⁻¹ * x) g

pp: case hn
𝕜 : 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
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
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
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (minSmoothness 𝕜 3) (fun x ↦ g⁻¹ * x) g

case hn
𝕜 : 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
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField u x⟩) 1

pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: case 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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
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
⊢ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x

Tactic:
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)]
    with y hy 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.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace β
inst✝⁶ : AddCommGroup β
inst✝⁵ : Module R β
inst✝⁴ : TopologicalSpace R
inst✝³ : ContinuousSMul R β
inst✝² : TopologicalSpace α
inst✝¹ : AddCommGroup α
inst✝ : Module R α
e : α ≃L[R] β
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let f : R × α → α := fun p ↦ e.symm <| p.1 • (e p.2)

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : TopologicalSpace β
inst✝⁶ : AddCommGroup β
inst✝⁵ : Module R β
inst✝⁴ : TopologicalSpace R
inst✝³ : ContinuousSMul R β
inst✝² : TopologicalSpace α
inst✝¹ : AddCommGroup α
inst✝ : Module R α
e : α ≃L[R] β
f : R × α → α := fun p ↦ e.symm (p.1 • e p.2)
⊢ Continuous fun p ↦ p.1 • p.2
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)),
    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:
intro e e' he 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.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
⊢ (mfderiv% Subtype.val z) 1 = 1

Tactic:
have A : mfderiv[Icc x y] (Subtype.val ∘ (projIcc x y h.out.le)) z 1
      = mfderiv[Icc x y] (@id ℝ) z 1 := by
    congr 1
    apply mfderivWithin_congr_of_mem _ z.2
    intro z hz
    simp [projIcc_of_mem h.out.le hz]

Goal state after:
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
A : (mfderiv[Icc x y] (Subtype.val ∘ projIcc x y ⋯) ↑z) 1 = (mfderiv[Icc x y] id ↑z) 1
⊢ (mfderiv% Subtype.val z) 1 = 1
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v {t | t + dt ∈ s} ↔ IsMIntegralCurveOn γ v s

Tactic:
by
  refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
  convert! hγ.comp_add (-dt)
  · ext t
    simp
  · simp

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)

Tactic:
have h : ContDiffOn ℝ ω _ Set.univ := U.contDiff.contDiffOn

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
⊢ HasFDerivWithinAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (range ↑I)
    (↑(extChartAt I x₀) (↑(extChartAt I x₀).symm (f t)))

Tactic:
exact hasFDerivWithinAt_tangentCoordChange ⟨hft1, hft2⟩

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

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
heq : γ =ᶠ[𝓝 t₁] γ'
⊢ s ∈ 𝓝 t₁

Tactic:
apply (heq.and hmem).mono

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
heq : γ =ᶠ[𝓝 t₁] γ'
⊢ ∀ (x : ℝ), γ x = γ' x ∧ a < x ∧ x < b → ({t | γ t = γ' t} ∩ Ioo a b) x
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
⊢ ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : ↥V → M'),
    ChartedSpace.LiftProp P f → ChartedSpace.LiftProp P fun x ↦ f (i x)

Tactic:
intro U V i f h x
    have hUV : U ≤ V := CategoryTheory.leOfHom i
    change ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
    rw [← hG.liftPropAt_iff_comp_inclusion hUV]
    apply h

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
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
hy : ContMDiffAt I I' 2 f y
h'y : y ∈ s
⊢ MDiffAt f y

Tactic:
exact hy.mdifferentiableAt two_ne_zero

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ ((cov.torsion x) (X x)) (Y x) = (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x

Tactic:
unfold torsion IsCovariantDerivativeOn.torsion

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
x : M
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ ((TensorialAt.mkHom₂ (fun x1 x2 ↦ IsCovariantDerivativeOn.torsionAux (↑cov) x1 x2 x) x ⋯ ⋯) (X x)) (Y x) =
    (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ ((cov.torsion x) X₀) Y₀ =
    (↑cov (extend E Y₀) x) (extend E X₀ x) - (↑cov (extend E X₀) x) (extend E Y₀ x) -
      mlieBracket I (extend E X₀) (extend E Y₀) x

Tactic:
unfold torsion IsCovariantDerivativeOn.torsion

Goal state after:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
x : M
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X₀ Y₀ : TangentSpace I x
⊢ ((TensorialAt.mkHom₂ (fun x1 x2 ↦ IsCovariantDerivativeOn.torsionAux (↑cov) x1 x2 x) x ⋯ ⋯) X₀) Y₀ =
    (↑cov (extend E Y₀) x) (extend E X₀ x) - (↑cov (extend E X₀) x) (extend E Y₀ x) -
      mlieBracket I (extend E X₀) (extend E Y₀) x
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.mp inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
refine ⟨_, eEF ∘ f.embeddingPiTangent,
    eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩

Goal state after:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.mp inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq ⋯
x : M
⊢ Injective ⇑(mfderiv% (⇑eEF ∘ ⇑f.embeddingPiTangent) x)