mathlib-initiative/mathlib-tactics huggingface dataset:
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 =
    (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) y)))

Tactic:
mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' hy,

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 (↑(extChartAt I x).symm (↑(extChartAt I x) y)))
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
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
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 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
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 : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
⊢ mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) ∘SL mfderiv% ↑(extChartAt I x₀) x₀ =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)))

Tactic:
convert!
      mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt (I := I) (x := x₀) (y :=
        extChartAt I x₀ x₀) (by simp)

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
⊢ f '' h.domChart.source ⊆ h.codChart.source

Tactic:
simp [h.source_subset_preimage_source]

Goal state after:
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
⊢ closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ioi]

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.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
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp i = z.ofLp i

Tactic:
have A : x + z 0 ≤ y := by linarith

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 i = z.ofLp i
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
this✝ :
  ContDiffWithinAt 𝕜 m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
        (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x))))
    (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x)))
    t' x₀
x : N
hx : ContMDiffWithinAt I I' 1 (f x) u (g x)
h'x : x ∈ (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source
h2 : x ∈ g ⁻¹' (extChartAt I (g x₀)).source
hxt : x ∈ t
h1 : g x ∈ u
h3 : UniqueMDiffAt[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] (↑(extChartAt I (g x₀)) (g x))
A :
  mfderiv[range ↑I] ↑(extChartAt I (g x₀)).symm (↑(extChartAt I (g x₀)) (g x)) =
    mfderiv[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] ↑(extChartAt I (g x₀)).symm
      (↑(extChartAt I (g x₀)) (g x))
⊢ f x (g x) ∈ (chartAt H' (f x₀ (g x₀))).source

Tactic:
simpa using h'x

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:
refine ⟨fun hf ↦ ?_,
    fun hf ↦ hf.comp_contMDiffWithinAt_of_eq (contMDiffOn_projIcc w w.2) (by simp)⟩
  have A := contMDiff_subtypeVal_Icc (x := x) (y := y) (n := n) w
  rw [← contMDiffWithinAt_univ] at A ⊢
  convert! hf.comp _ A (fun z hz ↦ z.2)
  ext z
  simp

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
⊢ ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2

Tactic:
Submodule.mem_orthogonal_singleton_iff_inner_left

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : E
hw : ⟪w, v⟫ = 0
h₁ : 0 < ‖w‖ ^ 2 + 4
⊢ ‖4 • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2
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
this : (val ∘ fun x ↦ x⁻¹) = Ring.inverse ∘ val
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse ↑x

Tactic:
exact contDiffAt_ringInverse _ _

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

Goal state before:
pp: case mpr
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
t₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀

Tactic:
· rintro ⟨s, hs, h⟩
    rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]
    obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs
    refine ⟨s', h2.mem_nhds h3, ?_⟩
    intro t ht
    apply (h t (h1 ht)).hasMFDerivAt
    rw [mem_nhds_iff]
    exact ⟨s', h1, h2, ht⟩

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

Goal state before:
pp: case mpr
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
t₀ : ℝ
⊢ (∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
intro ⟨ε, hε, h⟩
    exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ ↑(stereographic' n (-v)) v = 0

Tactic:
dsimp [stereographic']

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr (↑(stereographic ⋯) v) = 0
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case hy
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
this✝ :
  ContDiffWithinAt 𝕜 m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
        (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x))))
    (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x)))
    t' x₀
x : N
hx : ContMDiffWithinAt I I' 1 (f x) u (g x)
h'x : x ∈ (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source
h2 : x ∈ g ⁻¹' (extChartAt I (g x₀)).source
hxt : x ∈ t
h1 : g x ∈ u
h3 : UniqueMDiffAt[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] (↑(extChartAt I (g x₀)) (g x))
A :
  mfderiv[range ↑I] ↑(extChartAt I (g x₀)).symm (↑(extChartAt I (g x₀)) (g x)) =
    mfderiv[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] ↑(extChartAt I (g x₀)).symm
      (↑(extChartAt I (g x₀)) (g x))
⊢ f x (g x) ∈ (chartAt H' (f x₀ (g x₀))).source

Tactic:
simpa using h'x

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

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ (fderivWithin 𝕜 (fun x' ↦ (x', 0)) (range ↑I) (↑I (↑(chartAt H x) x))) v = (v, 0)

Tactic:
fderivWithin_eq_fderiv,

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ (fderiv 𝕜 (fun x' ↦ (x', 0)) (↑I (↑(chartAt H x) x))) v = (v, 0)

case hs
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I (↑(chartAt H x) x))

case h
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (fun x' ↦ (x', 0)) (↑I (↑(chartAt H x) x))
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
hγ1 : IsMIntegralCurveOn (γ1_aux ∘ fun x ↦ x + (asup - ε / 2)) v {t | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
⊢ False

Tactic:
set γ1 := γ1_aux ∘ (· + (asup - ε / 2)) with γ1_def

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
⊢ False
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun t ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ riemannianEDist I y x < r

Tactic:
have : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0) := by
    apply riemannianEDist_le_pathELength h_smooth.contMDiffOn <;> simp [η, γ0, γ1]

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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun t ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ riemannianEDist I y x < r
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun x ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun x ↦ y
γ : ℝ → M := (Iic 1).piecewise γ₁ γ₂
⊢ riemannianEDist I x z < r

Tactic:
have : riemannianEDist I x z ≤ pathELength I γ 0 2 := by
    apply riemannianEDist_le_pathELength
    · apply ContMDiff.contMDiffOn
      exact ContMDiff.piecewise_Iic hγ₁_smooth hγ₂_smooth (hγ₁_const.trans hγ₂_const.symm)
    · simp [γ, hγ₁0]
    · simp [γ, hγ₂2]
    · exact zero_le_two

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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun x ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun x ↦ y
γ : ℝ → M := (Iic 1).piecewise γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ riemannianEDist I x z < r
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
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x v : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
conv_lhs => rw [show (1 : ℝ) = √1 by simp]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x v : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁸ : TopologicalSpace B
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → NormedAddCommGroup (E x)
inst✝³ : (x : B) → InnerProductSpace ℝ (E x)
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle ℝ F E
M : Type u_4
inst✝ : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
x : M
hv : ContinuousAt (fun m ↦ { proj := b m, snd := v m }) x
hw : ContinuousAt (fun m ↦ { proj := b m, snd := w m }) x
⊢ ContinuousAt (fun b_1 ↦ ⟪v b_1, w b_1⟫) x

Tactic:
simp only [← continuousWithinAt_univ] at hv hw ⊢
  exact ContinuousWithinAt.inner_bundle hv hw

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case mpr.refine_2.refine_1
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
⊢ (CategoryTheory.ConcreteCategory.hom (S.germ V x hxV)) ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f) *
      (CategoryTheory.ConcreteCategory.hom (S.germ V x hxV)) g =
    1

Tactic:
rw [← map_mul]
        -- Qualified the name to avoid Lean not finding a `OneHomClass` https://github.com/leanprover-community/mathlib4/pull/8386
        convert! RingHom.map_one _
        apply Subtype.ext
        ext y
        apply mul_inv_cancel₀
        exact hVf y

Goal state after: