mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ t₁.orthocenter ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧
    t₁.points i₂ ∈ ↑(affineSpan ℝ (Set.range t₁.points)) ∧ t₁.points i₃ ∈ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
exact
        ⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
          mem_affineSpan ℝ (Set.mem_range_self _)⟩

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

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
n : ℕ∞ω
x : M
k : 𝕜
f : C^∞⟮I, M; 𝕜⟯⟨x⟩
h : 𝕜
⊢ (k • f) • h = k • f • h

Tactic:
by
    rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul,
      mul_assoc]

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

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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ v (k • ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)

Tactic:
Derivation.map_smul,

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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ k • v (ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this : ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source
⊢ f (↑hf.localInverse.toPartialEquiv y) = y

Tactic:
hf.choose_spec.2 this

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
y : N
hy : y ∈ hf.localInverse.source
this : ↑hf.localInverse.toPartialEquiv y ∈ (Exists.choose hf).source
⊢ ↑(Exists.choose hf).toPartialEquiv (↑hf.localInverse.toPartialEquiv y) = y
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ⁅X, X⁆ f✝ = 0 f✝

Tactic:
simp only [commutator_apply, sub_self]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
r : 𝕜
X✝ Y : LeftInvariantDerivation I G
f f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ 0 = 0 f✝
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 =
    (Prod.fst ∘ fun x ↦
        (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1,
          (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2))
      x

Tactic:
Function.comp,

Goal state after:
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).toPartialEquiv (f x)).1
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_2
𝕜 : 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)
e e' : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
inst✝² : MemTrivializationAtlas e'
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ e.coordChange e' (f x) (g x) = ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)

Tactic:
· exact (Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²¹ : NontriviallyNormedField 𝕜
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✝¹⁴ : (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)
HB : Type u_9
inst✝⁸ : TopologicalSpace HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
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)
y₀ y : TotalSpace (F₁ →L[𝕜] F₂) fun b ↦ E₁ b →L[𝕜] E₂ b
⊢ ↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) y =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)

Tactic:
FiberBundle.chartedSpace_chartAt,

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²¹ : NontriviallyNormedField 𝕜
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✝¹⁴ : (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)
HB : Type u_9
inst✝⁸ : TopologicalSpace HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
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)
y₀ y : TotalSpace (F₁ →L[𝕜] F₂) fun b ↦ E₁ b →L[𝕜] E₂ b
⊢ ↑((trivializationAt (F₁ →L[𝕜] F₂) (fun x ↦ E₁ x →L[𝕜] E₂ x) y₀.proj).toOpenPartialHomeomorph ≫ₕ
          (chartAt HB y₀.proj).prod (OpenPartialHomeomorph.refl (F₁ →L[𝕜] F₂)))
      y =
    (↑(chartAt HB y₀.proj) y.proj, inCoordinates F₁ E₁ F₂ E₂ y₀.proj y.proj y₀.proj y.proj y.snd)
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₁
⊢ ((continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b) L) v =
    (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v

Tactic:
continuousLinearMapCoordChange,

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).symm.arrowCongrSL (Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) L) v =
    (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hV
𝕜 : 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
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse (V x) = 0

Tactic:
hV

Goal state after:
case hV
𝕜 : 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
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse 0 = 0
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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
let F₁ : G → (TangentBundle I G × TangentBundle I G) := fun g ↦ (fg g, fv g)

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
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 := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case e_6.st.ht
𝕜 : 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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
st : t ∈ 𝓝[s] x
hs : UniqueMDiffAt[s] x
hV : MDiffAt[t] (T% V) x
hW : MDiffAt[t] (T% W) x
⊢ range ↑I ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
exact nhdsWithin_mono _ inter_subset_right self_mem_nhdsWithin

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
⊢ (Subtype.val ∘ ↑(IccLeftChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm =ᶠ[𝓝[Icc x y] z] fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this

Tactic:
filter_upwards [self_mem_nhdsWithin] with w hw

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
⊢ ((Subtype.val ∘ ↑(IccLeftChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w =
    have this := toLp 2 fun x_1 ↦ w - x;
    this
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
⊢ (Subtype.val ∘ ↑(IccRightChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm =ᶠ[𝓝[Icc x y] z] fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this

Tactic:
filter_upwards [self_mem_nhdsWithin] with w hw

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
⊢ ((Subtype.val ∘ ↑(IccRightChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w =
    have this := toLp 2 fun x ↦ y - w;
    this
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case pos.hg
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
⊢ MDiffAt f (projIcc x y ⋯ ↑w)

pp: case pos.hf
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
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) ↑w

pp: case pos.hxs
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
⊢ UniqueMDiffAt[Icc x y] ↑w

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) ∘SL mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
· simp [hw]

Goal state after:
case pos.hf
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
⊢ MDiffAt[Icc x y] (projIcc x y ⋯) ↑w

case pos.hxs
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
⊢ UniqueMDiffAt[Icc x y] ↑w

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) ∘SL mfderiv[Icc x y] (projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1
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
⊢ HasFDerivWithinAt (↑(extChartAt I (γ t₀)) ∘ γ)
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) s t

Tactic:
← hasMFDerivWithinAt_iff_hasFDerivWithinAt

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
⊢ HasMFDerivAt[s] (↑(extChartAt I (γ t₀)) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))))
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)
⊢ Injective ⇑(mfderiv% Subtype.val v)

Tactic:
by
  convert! injective_mvfderiv_subtypeVal_sphere v

Goal state after: