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

Goal state before:
pp: case refine_1
𝕜 : 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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ ↑(extChartAt IB (f x₀).proj) (f x).proj = ↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj) (f x)).1

Tactic:
rw [Trivialization.coe_fst']

Goal state after:
case refine_1.ex
𝕜 : 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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 : (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (fun x ↦ (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet
⊢ (f x).proj ∈ (trivializationAt F E (f x₀).proj).baseSet
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
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
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ (MDiffAt[u] fun x ↦ ⟨x, s x⟩.proj) b₀ ∧ (MDiffAt[u] fun x ↦ (↑e ⟨x, s x⟩).2) b₀ ↔
    (MDiffAt[u] fun x ↦ (↑e ⟨x, s x⟩).2) b₀

pp: case he
𝕜 : 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
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
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ ⟨b₀, s b₀⟩ ∈ e.source

Tactic:
· change MDiffAt[u] (@id B) b₀ ∧ _ ↔ _
    simp [mdifferentiableWithinAt_id]

Goal state after:
case he
𝕜 : 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
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
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ ⟨b₀, s b₀⟩ ∈ e.source
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
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
ha : IsOpen[inst✝⁷] a
ha' : a ⊆ e.baseSet
⊢ MDiff[a] (T% s) ↔ MDiff[a] fun x ↦ (↑e ⟨x, s x⟩).2

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩ <;>
  have := (h x hx).mdifferentiableAt <| ha.mem_nhds hx
  · exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mp this).mdifferentiableWithinAt
  · exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mpr this).mdifferentiableWithinAt

Goal state after:
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
x : B
x✝ : x ∈ (continuousLinearMap σ e₁ e₂).baseSet
L L' : E₁ x →SL[σ] E₂ x
⊢ (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L + L' }).2 =
    (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L }).2 +
      (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L' }).2

Tactic:
simp [continuousLinearMap, Pretrivialization.toFun']

Goal state after:
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
x : B
x✝ : x ∈ (continuousLinearMap σ e₁ e₂).baseSet
L L' : E₁ x →SL[σ] E₂ x
⊢ (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L + L' }).2 =
    (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L }).2 +
      (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L' }).2

Tactic:
by simp [continuousLinearMap, Pretrivialization.toFun']

Goal state after:
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
x : B
x✝ : x ∈ (continuousLinearMap σ e₁ e₂).baseSet
c : 𝕜₂
L : E₁ x →SL[σ] E₂ x
⊢ (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := c • L }).2 =
    c • (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L }).2

Tactic:
simp [continuousLinearMap, Pretrivialization.toFun']

Goal state after:
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₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
x : B
x✝ : x ∈ (continuousLinearMap σ e₁ e₂).baseSet
c : 𝕜₂
L : E₁ x →SL[σ] E₂ x
⊢ (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := c • L }).2 =
    c • (↑(continuousLinearMap σ e₁ e₂) { proj := x, snd := L }).2

Tactic:
by simp [continuousLinearMap, Pretrivialization.toFun']

Goal state after:
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₁ : Trivialization F₁ TotalSpace.proj
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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ (continuousLinearMap σ e₁ e₂).symm b L =
    Trivialization.symmL 𝕜₂ e₂ b ∘SL L ∘SL Trivialization.continuousLinearMapAt 𝕜₁ e₁ b

Tactic:
rw [symm_apply]
  · rfl
  · exact hb

Goal state after:
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 h : G
⊢ ((mfderiv% fun b ↦ g * b) h).inverse = (mfderiv% fun b ↦ g⁻¹ * b) (g * h)

Tactic:
by
  have M : minSmoothness 𝕜 3 ≠ 0 := lt_of_lt_of_le (by simp) le_minSmoothness |>.ne'
  have A : mfderiv% ((fun x ↦ g⁻¹ * x) ∘ (fun x ↦ g * x)) h =
      ContinuousLinearMap.id _ _ := by
    have : (fun x ↦ g⁻¹ * x) ∘ (fun x ↦ g * x) = id := by ext x; simp
    rw [this, id_eq, mfderiv_id]
  rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
    (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)] at A
  have A' : mfderiv% ((fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x)) (g * h) =
      ContinuousLinearMap.id _ _ := by
    have : (fun x ↦ g * x) ∘ (fun x ↦ g⁻¹ * x) = id := by ext x; simp
    rw [this, id_eq, mfderiv_id]
  rw [mfderiv_comp (I' := I) _ (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M)
    (contMDiff_mul_left.contMDiffAt.mdifferentiableAt M), inv_mul_cancel_left g h] at A'
  exact ContinuousLinearMap.inverse_eq A' A

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 : Set M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hs : UniqueMDiffAt[s] x
⊢ mlieBracketWithin I V (c • W) s x = c • mlieBracketWithin I V W s x

Tactic:
simpa [mfderivWithin_const, mvfderivWithin] using!
    mlieBracketWithin_smul_right (mdifferentiableWithinAt_const (c := c)) (V := V) hW hs

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
s : Set M
x : M
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 = mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)) y

Tactic:
rw [mpullback_apply, mpullbackWithin_apply,
    ← (isInvertible_mfderiv_extChartAt hy).inverse_comp_apply_of_right,
    mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt' hy, A]

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 y)
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
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
⊢ ImmersionAtProp F I J M N g φ ψ

Tactic:
refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩

Goal state after:
𝕜 : 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
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
x : E
hx : x ∈ (φ.extend I).target
⊢ (↑(ψ.extend J) ∘ g ∘ ↑(φ.extend I).symm) x = (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) x
Module: Mathlib.Geometry.Manifold.Instances.Real

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

Tactic:
by simp [z.prop, sub_eq_add_neg, add_le_of_le_sub_left hz]

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

Goal state before:
pp: case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ y ≤ ↑z

Tactic:
simpa only [not_lt] using h'

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ IsManifold (𝓡∂ 1) n ↑(Icc x y)

Tactic:
apply isManifold_of_contDiffOn

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type u_3
inst✝² : TopologicalSpace M✝
inst✝¹ : ChartedSpace H M✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ∀ (e e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)),
    e ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
      e' ∈ atlas (EuclideanHalfSpace 1) ↑(Icc x y) →
        ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm)
          (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∈ Ioo a b
x✝ : ℝ
ht' : x✝ ∈ Ioo a b
⊢ (Ioo a b).piecewise γ γ' x✝ = γ x✝

Tactic:
by rw [piecewise, if_pos ht']

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p ∈ (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)).source
⊢ (Prod.fst ∘ fun x ↦
        (fderivWithin 𝕜
            (((fun p ↦ (↑I p.1, ↑I' p.2)) ∘ fun p ↦ (↑(chartAt H a.proj) p.1, ↑(chartAt H' b.proj) p.2)) ∘
              ↑((chartAt H x.1.proj).prod (chartAt H' x.2.proj).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm)
            (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H x.1.proj) x.1.proj), ↑I' (↑(chartAt H' x.2.proj) x.2.proj)))
          (x.1.snd, x.2.snd))
      p =
    (↑(trivializationAt E (TangentSpace I) a.proj) p.1).2

Tactic:
simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialHomeomorph,
      PartialEquiv.prod_source, mem_prod, TangentBundle.mem_chart_source_iff] at hp

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
⊢ (Prod.fst ∘ fun x ↦
        (fderivWithin 𝕜
            (((fun p ↦ (↑I p.1, ↑I' p.2)) ∘ fun p ↦ (↑(chartAt H a.proj) p.1, ↑(chartAt H' b.proj) p.2)) ∘
              ↑((chartAt H x.1.proj).prod (chartAt H' x.2.proj).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm)
            (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H x.1.proj) x.1.proj), ↑I' (↑(chartAt H' x.2.proj) x.2.proj)))
          (x.1.snd, x.2.snd))
      p =
    (↑(trivializationAt E (TangentSpace I) a.proj) p.1).2