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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt (T% t) x₀
⊢ (MDiffAt fun x ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀

Tactic:
simp_rw [← mdifferentiableWithinAt_univ] at ht' ⊢

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun x ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (Trivialization.continuousLinearMapAt 𝕜₂ e₂' b ∘SL
        (Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Trivialization.continuousLinearMapAt 𝕜₁ e₁ b) ∘SL
          Trivialization.symmL 𝕜₁ e₁' b)
      v

Tactic:
comp_apply,

Goal state after:
𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ ↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) (L (↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm v)) =
    (Trivialization.continuousLinearMapAt 𝕜₂ e₂' b)
      ((Trivialization.symmL 𝕜₂ e₂ b)
        (L ((Trivialization.continuousLinearMapAt 𝕜₁ e₁ b) ((Trivialization.symmL 𝕜₁ e₁' b) v))))
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
inst✝²⁷ : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst✝¹⁴ : (x : B) → AddCommGroup (E₃ x)
inst✝¹³ : (x : B) → Module 𝕜 (E₃ x)
inst✝¹² : NormedAddCommGroup F₃
inst✝¹¹ : NormedSpace 𝕜 F₃
inst✝¹⁰ : TopologicalSpace (TotalSpace F₃ E₃)
inst✝⁹ : (x : B) → TopologicalSpace (E₃ x)
inst✝⁸ : TopologicalSpace B
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
x₀ x : B
ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x
v : F₁
w : F₂
h₁x : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
h₂x : x ∈ (trivializationAt F₂ E₂ x₀).baseSet
h₃x : x ∈ (trivializationAt F₃ E₃ x₀).baseSet
⊢ ((inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃) (fun x ↦ E₂ x →L[𝕜] E₃ x) x₀ x x₀ x ϕ) v) w =
    (Trivialization.linearMapAt 𝕜 (trivializationAt F₃ E₃ x₀) x)
      ((ϕ ((trivializationAt F₁ E₁ x₀).symm x v)) ((trivializationAt F₂ E₂ x₀).symm x w))

Tactic:
rw [inCoordinates_eq h₁x (by simp [h₂x, h₃x])]
  simp [hom_trivializationAt, Trivialization.continuousLinearMap_apply, h₂x]

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

Goal state before:
pp: case e'_5
𝕜 : 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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := ⋯
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := ⋯
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := ⋯
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⋯
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := ⋯
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
g : G
e_4✝ : g = (((F₃ ∘ F₂) ∘ F₁) g).proj
⊢ mulInvariantVectorField v g = (((F₃ ∘ F₂) ∘ F₁) g).snd

Tactic:
simp only [comp_apply, tangentMap, F₃, F₂, F₁, fg, fv]
    rw [mfderiv_prod_eq_add_apply ((contMDiff_mul I (minSmoothness 𝕜 3)).mdifferentiableAt M)]
    simp +instances [mulInvariantVectorField]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
⊢ V₁ y = V y →
    W₁ y = W y →
      (∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x) →
        (∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x) → mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y

Tactic:
hVy

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
⊢ W₁ y = W y →
    (∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x) →
      (∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x) → mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
⊢ V₁ =ᶠ[𝓝 y] V → W₁ =ᶠ[𝓝 y] W → mlieBracket I V₁ W₁ y = mlieBracket I V W y

Tactic:
hVy

Goal state after:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
y : M
hVy : V₁ =ᶠ[𝓝 y] V
⊢ W₁ =ᶠ[𝓝 y] W → mlieBracket I V₁ W₁ y = mlieBracket I V W y
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ (fderivWithin 𝕜 f' s' x₀) (V' x₀) • W' x₀
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (A + B) x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x

Tactic:
mpullback_add_apply

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ (fderivWithin 𝕜 f' s' x₀) (V' x₀) • W' x₀
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) A x + mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) B x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (interior (range Subtype.val)).Nonempty

Tactic:
rw [range_euclideanHalfSpace, interior_halfSpace]
    exact ⟨toLp 2 fun i ↦ 1, by 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 : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
h₂ : ⟪v, ↑w⟫ = 0
h₃ : ⟪v, v⟫ = 1
⊢ 2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1)) * ((‖↑w‖ ^ 2 + 4)⁻¹ * (4 * 1)) = 1

Tactic:
simp [field]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
h₂ : ⟪v, ↑w⟫ = 0
h₃ : ⟪v, v⟫ = 1
⊢ 2 = 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 ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ {t | t + dt ∈ s}
⊢ HasMFDerivAt[{t | t + dt ∈ s}] (γ ∘ fun x ↦ x + dt) t (ContinuousLinearMap.smulRight 1 (v ((γ ∘ fun x ↦ x + dt) t)))

Tactic:
comp_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 ℝ
hγ : IsMIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ {t | t + dt ∈ s}
⊢ HasMFDerivAt[{t | t + dt ∈ s}] (γ ∘ fun x ↦ x + dt) t (ContinuousLinearMap.smulRight 1 (v (γ (t + dt))))
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 ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
this :
  ContinuousLinearMap.smulRight 1 (a • v (γ (t * a))) =
    ContinuousLinearMap.smulRight 1 (v (γ (t * a))) ∘SL ContinuousLinearMap.smulRight 1 a
⊢ HasMFDerivAt[{t | t * a ∈ s}] (γ ∘ fun x ↦ x * a) t
    (ContinuousLinearMap.smulRight 1 ((a • v) ((γ ∘ fun x ↦ x * a) t)))

Tactic:
comp_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 ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
this :
  ContinuousLinearMap.smulRight 1 (a • v (γ (t * a))) =
    ContinuousLinearMap.smulRight 1 (v (γ (t * a))) ∘SL ContinuousLinearMap.smulRight 1 a
⊢ HasMFDerivAt[{t | t * a ∈ s}] (γ ∘ fun x ↦ x * a) t (ContinuousLinearMap.smulRight 1 ((a • v) (γ (t * a))))
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
⊢ (γ ∘ fun x ↦ x + (a - b)) b = γ b

Tactic:
comp_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
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
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
h : IsContinuousRiemannianBundle F E
x : B✝
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C))
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0, (r' ^ 2)⁻¹ < 1 - δ * C

Tactic:
apply (tendsto_order.1 B).1

Goal state after:
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
h : IsContinuousRiemannianBundle F E
x : B✝
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := ⋯
C : ℝ := ⋯
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, 0 < δ
B : Tendsto (fun δ ↦ 1 - δ * C) (𝓝[>] 0) (𝓝 (1 - 0 * C))
⊢ (r' ^ 2)⁻¹ < 1 - 0 * C
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : 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
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ IsUnit f ↔ f ∉ RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)

Tactic:
by
  constructor
  · rintro ⟨⟨f, g, hf, hg⟩, rfl⟩ (h' : smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x f = 0)
    simpa [h'] using congr_arg (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x) hf
  · let S := (smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf
    -- Suppose that `f`, in the stalk at `x`, is nonzero at `x`
    rintro (hf : _ ≠ 0)
    -- Represent `f` as the germ of some function (also called `f`) on an open neighbourhood `U` of
    -- `x`, which is nonzero at `x`
    obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.exists_germ_eq f
    have hf' : f ⟨x, hxU⟩ ≠ 0 := by
      convert! hf
      exact (smoothSheafCommRing.eval_germ U x hxU f).symm
    -- In fact, by continuity, `f` is nonzero on a neighbourhood `V` of `x`
    have H : ∀ᶠ (z : U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0 := f.2.continuous.continuousAt.eventually_ne hf'
    rw [eventually_nhds_iff] at H
    obtain ⟨V₀, hV₀f, hV₀, hxV₀⟩ := H
    let V : Opens M := ⟨Subtype.val '' V₀, U.2.isOpenMap_subtype_val V₀ hV₀⟩
    have hUV : V ≤ U := Subtype.coe_image_subset (U : Set M) V₀
    have hV : V₀ = Set.range (Set.inclusion hUV) := by
      convert! (Set.range_inclusion hUV).symm
      ext y
      change _ ↔ y ∈ Subtype.val ⁻¹' Subtype.val '' V₀
      rw [Set.preimage_image_eq _ Subtype.coe_injective]
    clear_value V
    subst hV
    have hxV : x ∈ (V : Set M) := by
      obtain ⟨x₀, hxx₀⟩ := hxV₀
      convert! x₀.2
      exact congr_arg Subtype.val hxx₀.symm
    have hVf : ∀ y : V, f (Set.inclusion hUV y) ≠ 0 :=
      fun y ↦ hV₀f (Set.inclusion hUV y) (Set.mem_range_self y)
    -- Let `g` be the pointwise inverse of `f` on `V`, which is smooth since `f` is nonzero there
    let g : C^∞⟮IM, V; 𝓘(𝕜), 𝕜⟯ := ⟨(f ∘ Set.inclusion hUV)⁻¹, ?_⟩
    -- The germ of `g` is inverse to the germ of `f`, so `f` is a unit
    · refine ⟨⟨S.germ _ x (hxV) (ContMDiffMap.restrictRingHom IM 𝓘(𝕜) 𝕜 hUV f), S.germ _ x hxV g,
        ?_, ?_⟩, S.germ_res_apply hUV.hom x hxV f⟩
      · 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
      · 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 inv_mul_cancel₀
        exact hVf y
    · intro y
      exact (((contDiffAt_inv _ (hVf y)).contMDiffAt).comp y
        (f.contMDiff.comp (contMDiff_inclusion hUV)).contMDiffAt :)

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

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
⊢ cov.torsion = 0 →
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
intro h X Y x hX hY

Goal state after:
case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h : cov.torsion = 0
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
⊢ (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
ht : t.points = ![t.points 0, t.points 1, t.points 2]
⊢ AffineIndependent R ![t.points 0, t.points 1, t.points 2]

Tactic:
simpa [← ht] using t.independent

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ {x * y, x, y, 1} = univ

Tactic:
by
  apply Finset.eq_univ_of_card
  rw [card_four']
  repeat rw [card_insert_of_notMem]
  on_goal 4 => simpa using mul_notMem_of_exponent_two (by simp) hx hy hxy
  all_goals simp_all

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

Goal state before:
pp: n : ℕ
⊢ ∀ (a : DihedralGroup n), a.inv * a = 1

Tactic:
rintro (a | a)
    · exact congr_arg r (neg_add_cancel a)
    · exact congr_arg r (sub_self a)

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n

Tactic:
cases n
  · rw [Nat.card_eq_zero_of_infinite]
  · rw [Nat.card_eq_fintype_card, card]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H : Type u_4
inst✝² : Group G✝
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
x : X
⊢ ((lift FreeGroup.of).comp (FreeGroup.lift of)) (FreeGroup.of x) = (MonoidHom.id (FreeGroup X)) (FreeGroup.of x)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply,
          FreeGroup.lift_apply_of, lift_of]

Goal state after: