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

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
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
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle 1 F V I
x₀ : M
σ₀ : V x₀
⊢ ∃ s ∈ 𝓝 x₀, MDiff[s] fun x' ↦ ⟨x', extend F σ₀ x'⟩

Tactic:
obtain ⟨s, hs, hsσ⟩ := exists_contMDiffOn_extend (k := 1) I F σ₀

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
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
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle 1 F V I
x₀ : M
σ₀ : V x₀
s : Set M
hs : s ∈ 𝓝 x₀
hsσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) 1 (fun x' ↦ ⟨x', extend F σ₀ x'⟩) s
⊢ ∃ s ∈ 𝓝 x₀, MDiff[s] fun x' ↦ ⟨x', extend F σ₀ x'⟩
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

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
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
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
X X' : V x →L[𝕜] W
h : (fun A Z x_1 ↦ A (Z x)) X = (fun A Z x_1 ↦ A (Z x)) X'
⊢ X = X'

Tactic:
ext σ₀

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
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
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
X X' : V x →L[𝕜] W
h : (fun A Z x_1 ↦ A (Z x)) X = (fun A Z x_1 ↦ A (Z x)) X'
σ₀ : V x
⊢ X σ₀ = X' σ₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

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
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
n : WithTop ℕ∞
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
X X' : V x →L[𝕜] W
h : (fun A Z x_1 ↦ A (Z x)) X = (fun A Z x_1 ↦ A (Z x)) X'
⊢ X = X'

Tactic:
ext σ₀

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
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
n : WithTop ℕ∞
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
X X' : V x →L[𝕜] W
h : (fun A Z x_1 ↦ A (Z x)) X = (fun A Z x_1 ↦ A (Z x)) X'
σ₀ : V x
⊢ X σ₀ = 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
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'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
⊢ mpullbackWithin I I' f (g • V) s = g ∘ f • mpullbackWithin I I' f V s

Tactic:
by
  ext; simp [mpullbackWithin_apply]

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
V : (x : M) → TangentSpace I x
⊢ mpullback I I id V = V

Tactic:
ext x
  simp [mpullback]

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

Goal state before:
pp: case hxW
𝕜 : 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
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ y = W y

Tactic:
· exact hWy

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
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'
f : M → M'
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
y₀ : M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t y₀
hf : ContMDiffAt I I' n f x₀
hf' : (mfderiv% f x₀).IsInvertible
hmn : m + 1 ≤ n
hy₀ : y₀ = f x₀
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullback I I' f V x⟩) (f ⁻¹' t) x₀

Tactic:
subst hy₀
  exact ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn

Goal state after:
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
⊢ interior {y | ∀ (i : Fin n), a ≤ y.ofLp i} = {y | ∀ (i : Fin n), a < y.ofLp i}

Tactic:
rw [h, h', interior_iInter_of_finite]

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.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ¬↑z < y
⊢ (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph ∈ maximalAtlas 𝓘(ℝ, ℝ) n ℝ

pp: case neg
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ¬↑z < y
⊢ EqOn
    (↑((Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target

Tactic:
· apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
      · have : ContDiff ℝ n ((fun v ↦ v + y / 2) ∘ fun x ↦ y / 2 - x) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
      · have : ContDiff ℝ n ((fun v ↦ -v + y / 2) ∘ fun p' ↦ p' - y / 2) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

Goal state after:
case neg
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ¬↑z < y
⊢ EqOn
    (↑((Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.extend 𝓘(ℝ, ℝ)) ∘
      (fun z ↦ ↑z) ∘ ↑((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).symm)
    (⇑φ ∘ fun x ↦ (x, 0)) ((chartAt (EuclideanHalfSpace 1) z).extend (𝓡∂ 1)).target
Module: Mathlib.Geometry.Manifold.Immersion

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

Tactic:
rw [isOpen_iff_forall_mem_open]
  exact fun x hx ↦ ⟨{x | IsImmersionAtOfComplement hx.complement I J n f x },
    fun y hy ↦ hy.isImmersionAt, .isImmersionAtOfComplement,
    by simp [hx.isImmersionAtOfComplement_complement]⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ 1 (1 a) • (mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
← ContinuousLinearMap.smulRight_apply,

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
Module: Mathlib.Geometry.Manifold.IntegralCurve.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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ 1 (1 a) • (mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
← ContinuousLinearMap.smulRight_apply,

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
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
hγ : IsMIntegralCurveOn γ v univ
dt : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v univ

Tactic:
simpa using hγ.comp_add dt

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)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ (↑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)).range = (ℝ ∙ ↑v)ᗮ

Tactic:
convert! congr($((this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv).range)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ (ℝ ∙ ↑v)ᗮ = (↑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)).range
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
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩ = ⟨⟨⟨x, v⟩.proj, 0⟩, (⟨x, v⟩.snd, 0)⟩

Tactic:
have B : fderivWithin 𝕜 (fun x' : E ↦ (x', (0 : E))) (Set.range I) (I ((chartAt H x) x)) v
      = (v, 0) := by
    rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
    · simp
    · exact differentiableAt_fun_id
    · exact differentiableAt_const _
    · exact ModelWithCorners.uniqueDiffWithinAt_image I
    · exact differentiableAt_id.prodMk (differentiableAt_const _)

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
B : (fderivWithin 𝕜 (fun x' ↦ (x', 0)) (range ↑I) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩ = ⟨⟨⟨x, v⟩.proj, 0⟩, (⟨x, v⟩.snd, 0)⟩
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
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v

Tactic:
by
    rw [not_bddAbove_iff] at hbdd
    rw [exists_isMIntegralCurve_iff_exists_isMIntegralCurveOn_Ioo hv]
    intro a
    obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a
    exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩

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
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
heq : γ a = γ b
⊢ γ (b + (a - b)) = γ b

Tactic:
add_sub_cancel,

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
inst✝¹ : T2Space M
a b : ℝ
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
heq : γ a = γ b
⊢ γ a = γ b
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁴ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²³ : NormedAddCommGroup EM
inst✝²² : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²¹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
H : Type u_5
inst✝¹⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝¹⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁶ : TopologicalSpace M
inst✝¹⁵ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
inst✝¹² : TopologicalSpace G
inst✝¹¹ : ChartedSpace H G
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : ChartedSpace H A
inst✝⁸ : TopologicalSpace A'
inst✝⁷ : ChartedSpace H' A'
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ChartedSpace H R
EP : Type u_7
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens ↑(TopCat.of P))ᵒᵖ
g : (smoothSheaf IP I P N).obj.obj U
⊢ (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred (↑g ∘ (unop U).1.restrictPreimage f)

Tactic:
apply ContMDiff.comp (I' := IP) g.2
    rw [← ContMDiff.subtypeVal_comp_iff]
    exact hf.comp contMDiff_subtype_val

Goal state after:
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
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(mfderiv[Icc 0 t₁] γ' t') 1‖ₑ ≤ ∫⁻ (t' : ℝ) in Icc 0 t₁, ↑C * ‖(mfderiv[Icc 0 t₁] γ t') 1‖ₑ

Tactic:
apply setLIntegral_mono' measurableSet_Icc (fun t' ht' ↦ ?_)
      have : mfderiv[Icc 0 t₁] γ' t' =
          (mfderiv% (extChartAt I x) (γ t')) ∘L (mfderiv[Icc 0 t₁] γ t') := by
        apply mfderiv_comp_mfderivWithin
        · refine mdifferentiableAt_extChartAt (uc' ?_)
          apply t₁_mem ht'
        · exact (γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'
        · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
          exact uniqueDiffOn_Icc h't' _ ht'
      have : mfderiv[Icc 0 t₁] γ' t' 1 =
          (mfderiv% (extChartAt I x) (γ t')) (mfderiv[Icc 0 t₁] γ t' 1) :=
        congr($this 1)
      rw [this]
      apply (ContinuousLinearMap.le_opENorm _ _).trans
      gcongr
      refine (hu ?_).le
      apply t₁_mem ht'

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Star

Goal state before:
pp: A : Type u_1
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : A → A → Prop
hr : ∀ (a b : A), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : A
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star w✝ + Star.star y✝) (Star.star x✝ + Star.star z✝)

Tactic:
exact (h1.star hr).add (h2.star hr)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
⊢ False

Tactic:
have := h'.is_comm.comm (r 1) (sr 0)

Goal state after:
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : r 1 * sr 0 = sr 0 * r 1
⊢ False
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = fst x

Tactic:
rw [← fst_comp_toProd]

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = ((MonoidHom.fst M N).comp toProd) x
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ toProd (inl x.1 * inr x.2) = x

Tactic:
rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]

Goal state after: