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✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (b : B) → E b
u : Set B
b₀ : B
⊢ MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun b ↦ (↑(trivializationAt F E b₀) ⟨b, s b⟩).2) b₀

Tactic:
mdifferentiableWithinAt_totalSpace

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
s : (b : B) → E b
u : Set B
b₀ : B
⊢ (MDiffAt[u] fun x ↦ ⟨x, s x⟩.proj) b₀ ∧ (MDiffAt[u] fun x ↦ (↑(trivializationAt F E ⟨b₀, s b₀⟩.proj) ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun b ↦ (↑(trivializationAt F E b₀) ⟨b, s b⟩).2) b₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : TopologicalSpace (TotalSpace F E)
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝¹² : NormedAddCommGroup EM
inst✝¹¹ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace HM M
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
s : Set M
x₀ : M
he : f x₀ ∈ e.source
⊢ MDiffAt[s] f x₀ ↔ (MDiffAt[s] fun x ↦ (f x).proj) x₀ ∧ (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀

Tactic:
mdifferentiableWithinAt_totalSpace

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : TopologicalSpace (TotalSpace F E)
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝¹² : NormedAddCommGroup EM
inst✝¹¹ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace HM M
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
s : Set M
x₀ : M
he : f x₀ ∈ e.source
⊢ (MDiffAt[s] fun x ↦ (f x).proj) x₀ ∧ (MDiffAt[s] fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀ ↔
    (MDiffAt[s] fun x ↦ (f x).proj) x₀ ∧ (MDiffAt[s] fun x ↦ (↑e (f x)).2) 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✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
⊢ ∀
    e ∈
      {e |
        ∃ e₁ e₂, ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂), e = continuousLinearMap σ e₁ e₂},
    Pretrivialization.IsLinear 𝕜₂ e

Tactic:
rintro _ ⟨e₁, he₁, e₂, he₂, rfl⟩

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✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
e₁ : Trivialization F₁ TotalSpace.proj
he₁ : Trivialization F₂ TotalSpace.proj
e₂ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas he₁
⊢ Pretrivialization.IsLinear 𝕜₂ (continuousLinearMap σ e₁ he₁)
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g : G
V : (g : G) → TangentSpace I g
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun x ↦ g⁻¹ * x) V g

Tactic:
have A : 1 = g⁻¹ * g := by simp
  simp only [mulInvariantVectorField, mpullback, inverse_mfderiv_mul_left]
  congr
  simp

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'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderiv[u] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : (mfderiv[s] f x₀).IsInvertible
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
y : M
hy : y ∈ s
h'y : ContMDiffWithinAt I I' 1 f u y
⊢ (mfderiv[u] f y).inverse (V (f y)) = (mfderiv[s] f y).inverse (V (f y))

Tactic:
MDifferentiableWithinAt.mfderivWithin_mono (h'y.mdifferentiableWithinAt one_ne_zero)
    (hs _ hy) hu

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
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
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderiv[u] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : (mfderiv[s] f x₀).IsInvertible
Y : ∀ᶠ (x' : M) in 𝓝[u] x₀, ContMDiffWithinAt I I' 1 f u x'
y : M
hy : y ∈ s
h'y : ContMDiffWithinAt I I' 1 f u y
⊢ (mfderiv[u] f y).inverse (V (f y)) = (mfderiv[u] f y).inverse (V (f y))
Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Goal state before:
pp: case property
𝕜 : Type u_1
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
H : Type u_6
H' : Type u_7
G : Type u_8
G' : Type u_9
inst✝²⁴ : NontriviallyNormedField 𝕜
inst✝²³ : NormedAddCommGroup E
inst✝²² : NormedSpace 𝕜 E
inst✝²¹ : NormedAddCommGroup E'
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
M : Type u_10
M' : Type u_11
N : Type u_12
N' : Type u_13
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
Q : (M' → N') → OpenPartialHomeomorph M' H' → OpenPartialHomeomorph N' G' → Prop
R : (M × M' → N × N') → OpenPartialHomeomorph (M × M') (H × H') → OpenPartialHomeomorph (N × N') (G × G') → Prop
hf : LiftSourceTargetPropertyAt I J n f x P
g : M' → N'
x' : M'
hg : LiftSourceTargetPropertyAt I' J' n g x' Q
h :
  ∀ {f : M → N} {φ₁ : OpenPartialHomeomorph M H} {ψ₁ : OpenPartialHomeomorph N G} {g : M' → N'}
    {φ₂ : OpenPartialHomeomorph M' H'} {ψ₂ : OpenPartialHomeomorph N' G'},
    P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂)
⊢ R (Prod.map f g) (hf.domChart.prod hg.domChart) (hf.codChart.prod hg.codChart)

Tactic:
exact h hf.property hg.property

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanHalfSpace 1
⊢ max (y - (↑z).ofLp 0) x ∈ Icc x y

Tactic:
by simp [z.prop, h.out.le, sub_eq_add_neg]

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
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y) ↔ ContMDiff (𝓡∂ 1) I n f

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffOn contMDiffOn_projIcc⟩

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
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
f : ↑(Icc x y) → M
hf : ContMDiffOn 𝓘(ℝ, ℝ) I n (f ∘ projIcc x y ⋯) (Icc x y)
⊢ ContMDiff (𝓡∂ 1) I n f
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case pos
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)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
⊢ (mfderiv% f (projIcc x y ⋯ ↑w)) ((mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1) = (mfderiv% f w) 1

Tactic:
have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]

Goal state after:
case pos
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)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : MDiffAt f w
this : w = projIcc x y ⋯ ↑w
⊢ (mfderiv% f (projIcc x y ⋯ ↑w)) ((mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1) = (mfderiv% f w) 1
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w ↦ (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w ↦ 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Tactic:
convert! h₁.smul h₂ using 1

Goal state after:
case e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
h₀ : HasFDerivAt (fun w ↦ ‖w‖ ^ 2) 0 0
h₁ : HasFDerivAt (fun w ↦ (‖w‖ ^ 2 + 4)⁻¹) 0 0
h₂ : HasFDerivAt (fun w ↦ 4 • w + (‖w‖ ^ 2 - 4) • v) (4 • ContinuousLinearMap.id ℝ E) 0
⊢ ContinuousLinearMap.id ℝ E =
    (‖0‖ ^ 2 + 4)⁻¹ • 4 • ContinuousLinearMap.id ℝ E + ContinuousLinearMap.smulRight 0 (4 • 0 + (‖0‖ ^ 2 - 4) • v)
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
⊢ ContMDiff 𝓘(𝕜, R) 𝓘(𝕜, R) n (val ∘ fun a ↦ a⁻¹)

Tactic:
rw [this, ContMDiff]

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
this : (val ∘ fun x ↦ x⁻¹) = Ring.inverse ∘ val
⊢ ∀ (x : Rˣ), ContMDiffAt 𝓘(𝕜, R) 𝓘(𝕜, R) n (Ring.inverse ∘ val) x
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 ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ Continuous[_, inst✝³] fun y ↦ γ' ↑y

Tactic:
· rw [continuous_iff_continuousAt]
      rintro ⟨_, ht⟩
      apply ContinuousAt.comp _ continuousAt_subtype_val
      rw [Subtype.coe_mk]
      exact hγ'.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
⊢ pathELength I γ a b = pathELength I γ' a b

Tactic:
simp only [pathELength_eq_lintegral_mfderiv_Ioo]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ γ' : ℝ → M
h : EqOn γ γ' (Ioo a b)
⊢ ∫⁻ (t : ℝ) in Ioo a b, ‖(mfderiv% γ t) 1‖ₑ = ∫⁻ (t : ℝ) in Ioo a b, ‖(mfderiv% γ' t) 1‖ₑ
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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
y : M
hy : ∀ᶠ (x_1 : M) in 𝓝[s] y, ↑(extChartAt I x) x_1 ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s
hyU :
  ∀ᶠ (x_1 : M) in 𝓝[s] y,
    U x_1 =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)) x_1
hyV :
  ∀ᶠ (x_1 : M) in 𝓝[s] y,
    V x_1 =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)) x_1
h'yU :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (m' + 1)
    (fun x_1 ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I) x_1⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
h'yV :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (m' + 1)
    (fun x_1 ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
hy_chart : y ∈ (chartAt H x).source
hys : y ∈ s
⊢ mlieBracketWithin I U V s y =
    mlieBracketWithin I
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)))
      (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))) s y

Tactic:
exact Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem hyU hyV hys

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (ψ • σ) x' = (ψ • σ') x'

Tactic:
dsimp [ψ]

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
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (if σ x' = σ' x' then 1 else 0) • σ x' = (if σ x' = σ' x' then 1 else 0) • σ' x'
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

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
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (ψ • σ) x' = (ψ • σ') x'

Tactic:
dsimp [ψ]

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
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (if x' ∈ s then 1 else 0) • σ x' = (if x' ∈ s then 1 else 0) • σ' x'