mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
hFφ : IsLocalMax (⇑F ∘ f) x
h : fderiv ℝ (⇑F ∘ f) x = 0
⊢ DifferentiableAt ℝ (⇑F) (f x)

Tactic:
by fun_prop

Goal state after:
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
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : 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
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
by
  -- Choose a right inverse `g` of `f`.
  choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'
  -- Choose diffeomorphisms φ_x which coincide with `f` near `x`.
  choose Φ hyp using (fun x ↦ hf x)
  -- Two such diffeomorphisms (and their inverses!) coincide on their sources:
  -- they're both inverses to g. In fact, the latter suffices for our proof.
  -- have (x y) : EqOn (Φ x).symm (Φ y).symm ((Φ x).target ∩ (Φ y).target) := sorry
  have aux (x) : EqOn g (Φ x).symm (Φ x).target :=
    eqOn_of_leftInvOn_of_rightInvOn (fun x' _ ↦ hgInverse.1 x')
      (LeftInvOn.congr_left ((Φ x).toOpenPartialHomeomorph).rightInvOn
        ((Φ x).toOpenPartialHomeomorph).mapsTo_symm (hyp x).2.symm)
      (fun _y hy ↦ (Φ x).map_target hy)
  exact {
    toFun := f
    invFun := g
    left_inv := hgInverse.1
    right_inv := hgInverse.2
    contMDiff_toFun := hf.contMDiff
    contMDiff_invFun := by
      intro y
      let x := g y
      obtain ⟨hx, hfx⟩ := hyp x
      apply ((Φ x).symm.contMDiffOn.congr (aux x)).contMDiffAt (((Φ x).open_target).mem_nhds ?_)
      have : y = (Φ x) x := ((hgInverse.2 y).congr (hfx hx)).mp rfl
      exact this ▸ (Φ x).map_source hx }

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

Goal state before:
pp: case refine_1
𝕜 : 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
h : MDiff[a] (T% s)
x : B
hx : x ∈ a
this : MDiffAt (T% s) x
⊢ (MDiffAt[a] fun x ↦ (↑e ⟨x, s x⟩).2) x

Tactic:
exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mp this).mdifferentiableWithinAt

Goal state after:
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: case e'_4
𝕜₁ : 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 σ
b : B
L₁ : E₁ b ≃L[𝕜₁] F₁ := Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F₁ E₁ b) b ⋯
L₂ : E₂ b ≃L[𝕜₂] F₂ := Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F₂ E₂ b) b ⋯
φ : (E₁ b →SL[σ] E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this : IsInducing fun x ↦ (b, φ x)
x✝ : E₁ b →SL[σ] E₂ b
f : F₁
⊢ (Trivialization.linearMapAt 𝕜₂ (trivializationAt F₂ E₂ b) b)
      (x✝ ((Trivialization.symmL 𝕜₁ (trivializationAt F₁ E₁ b) b) f)) =
    (φ x✝) f

Tactic:
simp only [Trivialization.symmL_apply, mem_baseSet_trivializationAt,
      Trivialization.linearMapAt_def_of_mem]

Goal state after:
case e'_4
𝕜₁ : 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 σ
b : B
L₁ : E₁ b ≃L[𝕜₁] F₁ := Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F₁ E₁ b) b ⋯
L₂ : E₂ b ≃L[𝕜₂] F₂ := Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F₂ E₂ b) b ⋯
φ : (E₁ b →SL[σ] E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this : IsInducing fun x ↦ (b, φ x)
x✝ : E₁ b →SL[σ] E₂ b
f : F₁
⊢ ↑(Trivialization.linearEquivAt 𝕜₂ (trivializationAt F₂ E₂ b) b ⋯) (x✝ ((trivializationAt F₁ E₁ b).symm b f)) =
    (φ x✝) f
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
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)
EB₁ : Type u_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
inst✝⁶ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ : (MDiffAt fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : (MDiffAt fun m ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : MDiffAt b₂ m₀
⊢ (MDiffAt fun m ↦ ⟨b₂ m, (ϕ m) (v m)⟩) m₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hϕ hv hb₂ ⊢
  exact MDifferentiableWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

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 : (x : M) → TangentSpace I x
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)) =
    (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
        (↑(extChartAt I x) x))

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : 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
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
      (↑(extChartAt I x) x)
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)) =
    (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x))

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
y : TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x | V₁ x = V x}
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm y).inverse (V₁ (↑(extChartAt I x).symm y)) =
    (mfderiv[range ↑I] ↑(extChartAt I x).symm y).inverse (V (↑(extChartAt I x).symm y))

Tactic:
congr 1

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

Goal state before:
pp: case hxV
𝕜 : 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse
      (V₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) x)))

Tactic:
congr 1

Goal state after:
case hxV.e_6
𝕜 : 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ V₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x)) = V (↑(extChartAt I x).symm (↑(extChartAt I x) x))
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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
y : TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x | W₁ x = W x}
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm y).inverse (W₁ (↑(extChartAt I x).symm y)) =
    (mfderiv[range ↑I] ↑(extChartAt I x).symm y).inverse (W (↑(extChartAt I x).symm y))

Tactic:
congr 1

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

Goal state before:
pp: case hxW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse
      (W₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse
      (W (↑(extChartAt I x).symm (↑(extChartAt I x) x)))

Tactic:
congr 1

Goal state after:
case hxW.e_6
𝕜 : 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ W₁ (↑(extChartAt I x).symm (↑(extChartAt I x) x)) = W (↑(extChartAt I x).symm (↑(extChartAt I x) x))
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 : (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
⊢ (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)) =
    (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
        (↑(extChartAt I x) x))

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : 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
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
      (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ toLp 2 (update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0)) = xval

Tactic:
← WithLp.equiv_symm_apply,

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)).symm
      (update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0)) =
    xval
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ toLp 2 (update x✝.ofLp 0 (max (x✝.ofLp 0) 0)) = x✝

Tactic:
← WithLp.equiv_symm_apply,

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝ : EuclideanSpace ℝ (Fin n)
hx : x✝ ∈ {x | 0 ≤ x.ofLp 0}
⊢ (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)).symm (update x✝.ofLp 0 (max (x✝.ofLp 0) 0)) = x✝
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
y : ↥s
⊢ ContinuousAt Subtype.val y

Tactic:
by fun_prop

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn (fun z ↦ ⟨toLp 2 fun x_1 ↦ ↑z - x, ⋯⟩) {z | ↑z < y}

Tactic:
by fun_prop

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
⊢ ContinuousOn (fun z ↦ ⟨min ((↑z).ofLp 0 + x) y, ⋯⟩) {z | (↑z).ofLp 0 < y - x}

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_7
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
y : ↥s
x : E
hx : x ∈ ((chartAt H y).extend I).target
this : ↑I (↑(chartAt H y) (↑(chartAt H y).symm (↑I.symm x))) = x
⊢ (↑((chartAt H ↑y).extend I) ∘ Subtype.val ∘ ↑((chartAt H y).extend I).symm) x =
    (⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}) ∘ fun x ↦ (x, 0)) x

Tactic:
simpa +contextual

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)
⊢ ContinuousOn (fun z ↦ ⟨toLp 2 fun x_1 ↦ y - ↑z, ⋯⟩) {z | x < ↑z}

Tactic:
by fun_prop

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)
⊢ ContinuousOn (fun z ↦ ⟨max (y - (↑z).ofLp 0) x, ⋯⟩) {z | (↑z).ofLp 0 < y - x}

Tactic:
by fun_prop

Goal state after: