mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
g g' : M → F
x : M
hg : MDiffAt[s] g x
hg' : MDiffAt[s] g' x
hs : UniqueMDiffAt[s] x
⊢ ↑(NormedSpace.fromTangentSpace (g x + g' x)) ∘SL (mfderiv[s] g x + mfderiv[s] g' x) =
    ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv[s] g x +
      ↑(NormedSpace.fromTangentSpace (g' x)) ∘SL mfderiv[s] g' x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
g g' : M → F
x : M
hg : MDiffAt[s] g x
hg' : MDiffAt[s] g' x
hs : UniqueMDiffAt[s] x
⊢ ↑(NormedSpace.fromTangentSpace (g x - g' x)) ∘SL (mfderiv[s] g x - mfderiv[s] g' x) =
    ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv[s] g x -
      ↑(NormedSpace.fromTangentSpace (g' x)) ∘SL mfderiv[s] g' x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
g : M → F
x : M
hs : UniqueMDiffAt[s] x
⊢ ↑(NormedSpace.fromTangentSpace (-g x)) ∘SL (-mfderiv[s] g x) =
    -↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv[s] g x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
x : M
a : M → 𝕜
ha : MDiffAt[s] a x
g : M → F
hg : MDiffAt[s] g x
hs : UniqueMDiffAt[s] x
⊢ HasFDerivWithinAt (↑(chartAt F (a x • g x)) ∘ (a • g) ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (a x • d[s] g x + (d[s] a x).smulRight (g x)) =
    HasFDerivWithinAt
      (↑(chartAt 𝕜 (a x)) ∘ a ∘ ↑(chartAt H x).symm ∘ ↑I.symm • ↑(chartAt F (g x)) ∘ g ∘ ↑(chartAt H x).symm ∘ ↑I.symm)
      (↑(chartAt 𝕜 (a x)) (a x) • mfderiv[s] g x + (mfderiv[s] a x).smulRight (↑(chartAt F (g x)) (g x)))

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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
s : Set M
f g : M → 𝕜
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
hs : UniqueMDiffAt[s] x
⊢ d[s] (f * g) x = f x • d[s] g x + g x • d[s] f x

Tactic:
by
  convert! mvfderivWithin_smul hf hg hs
  ext v
  simp [mul_comm]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ ↑(NormedSpace.fromTangentSpace (g x + g' x)) ∘SL (mfderiv% g x + mfderiv% g' x) =
    ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x + ↑(NormedSpace.fromTangentSpace (g' x)) ∘SL mfderiv% g' x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ ↑(NormedSpace.fromTangentSpace (g x - g' x)) ∘SL (mfderiv% g x - mfderiv% g' x) =
    ↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x - ↑(NormedSpace.fromTangentSpace (g' x)) ∘SL mfderiv% g' x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : M → F
x : M
⊢ ↑(NormedSpace.fromTangentSpace (-g x)) ∘SL (-mfderiv% g x) = -↑(NormedSpace.fromTangentSpace (g x)) ∘SL mfderiv% g x

Tactic:
rfl

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
⊢ (-mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I))
            (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
            (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)))
      x =
    -mlieBracketWithin I W V s x

Tactic:
rfl

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
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hV : MDiffAt[t] (T% V) (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨f x, v x⟩) x₀
this✝ : (MDiffAt[s] fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) x₀
this :
  MDiffAt[s]
      (inverse ∘ fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x))
    x₀
A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀
B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (trivializationAt E (TangentSpace I) x₀).baseSet
h'x : x ∈ f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet
⊢ ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx) ∘SL
      (mfderiv[s] f x).inverse ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x)
              h'x).symm =
    (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx) ∘SL
        (mfderiv[s] f x).inverse) ∘SL
      ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x).symm

Tactic:
rfl

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✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆

Tactic:
simp only [AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul]
    rw [mlieBracket_const_smul_right]
    exact mdifferentiableAt_addInvariantVectorField _

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
x : M
inst✝ : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := extChartAt I x
⊢ ((mfderiv% ↑φ x).inverse ∘SL (mfderiv[range ↑I] ↑φ.symm (↑φ x)).inverse) Y = Y

Tactic:
trans (ContinuousLinearMap.id 𝕜 _) Y

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
x : M
inst✝ : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := ⋯
⊢ ((mfderiv% ↑φ x).inverse ∘SL (mfderiv[range ↑I] ↑φ.symm (↑φ x)).inverse) Y =
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) Y

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁵ : TopologicalSpace H
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
x : M
inst✝ : IsManifold I 2 M
Y : TangentSpace I x
φ : PartialEquiv M E := ⋯
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) Y = Y
Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ x ∈ (domChart.restr s).source

Tactic:
grind

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ (domChart.restr s).source ⊆ f ⁻¹' codChart.source

Tactic:
grind

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'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
hv : ContMDiffWithinAt I I'.tangent m (fun x ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀
this✝ :
  ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) s x₀
this :
  ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
    (inverse ∘ fun x ↦ inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x (f x₀) (f x) (mfderiv[s] f x)) s x₀
A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀
B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀
x : M
hx : x ∈ (trivializationAt E (TangentSpace I) x₀).baseSet
h'x : x ∈ f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet
⊢ ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) (b₂ x₀)) (b₂ x) hx) ∘SL
      (mfderiv[s] f x).inverse ∘SL
        ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (b₁ x₀)) (b₁ x)
              h'x).symm =
    (↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x hx) ∘SL
        (mfderiv[s] f x).inverse) ∘SL
      ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt E' (TangentSpace I') (f x₀)) (f x) h'x).symm

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ (hf.domChart.restr s).source ⊆ s

Tactic:
grind

Goal state after:
Module: Mathlib.Topology.Homeomorph.TransferInstance

Goal state before:
pp: case e'_4
R : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
e : α ≃ β
this : TopologicalSpace α := e.topologicalSpace
⊢ e.topologicalSpace = TopologicalSpace.induced (⇑e) inst✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : Group β
inst✝² : IsTopologicalGroup β
inst✝¹ : TopologicalSpace α
inst✝ : Group α
e : α ≃ₜ* β
⊢ Continuous fun a ↦ a⁻¹

Tactic:
have : Continuous (e.symm ∘ (fun q ↦ q⁻¹) ∘ e) := by fun_prop
    exact this.congr (fun p ↦ by simp)

Goal state after:
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 : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst✝¹] s
x✝ : ImmersionAtProp F I J M N f φ ψ
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
⊢ range ↑I ∩ (↑I.symm ⁻¹' φ.target ∩ ↑I.symm ⁻¹' ↑φ.symm ⁻¹' interior s) ⊆ ↑I.symm ⁻¹' φ.target

Tactic:
grind

Goal state after:
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
x : E
hx : x ∈ (φ.extend I).target
this : ↑(φ.extend I).symm x ∈ φ.source
⊢ (↑(ψ.extend J) ∘ g ∘ ↑(φ.extend I).symm) x = (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) x

Tactic:
grind

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

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
x✝ : PiLp p fun x ↦ ℝ
⊢ (∀ (i : Fin n), a ≤ x✝.ofLp i) ↔ ∀ (i : Fin n), a ≤ f i x✝

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
h : {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a
x✝ : PiLp p fun x ↦ ℝ
⊢ (∀ (i : Fin n), a < x✝.ofLp i) ↔ ∀ (i : Fin n), a < f i x✝

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ 0 ∈ {y | 0 = y.ofLp 0}

Tactic:
mem_ofPred,

Goal state after:
x y : ℝ
hxy : Fact (x < y)
⊢ 0 = ofLp 0 0
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
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
simp only [h', if_false]
      apply lt_of_lt_of_le h.out
      simpa only [not_lt] using h'

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

Goal state before:
pp: case neg
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
⊢ 0 1 = 0 1

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
A : (mfderiv[Icc x y] (Subtype.val ∘ projIcc x y ⋯) ↑z) 1 = (mfderiv[Icc x y] id ↑z) 1
⊢ (ContinuousLinearMap.id ℝ ℝ) 1 = 1

Tactic:
rfl

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
⊢ ⟪v, ↑x⟫_ℝ • v + (ℝ ∙ v)ᗮ.starProjection ↑x = a • v + ↑y

Tactic:
rfl

Goal state after:
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
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
rfl

Goal state after:
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
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
rfl

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

Goal state before:
pp: case e'_11
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v v' : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
U' : ↥(ℝ ∙ ↑v')ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
H₁ : ContDiffOn ℝ ω (⇑U' ∘ stereoToFun ↑v') {x | ((innerSL ℝ) ↑v') x ≠ 1}
H₂ : ContDiff ℝ ω ((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm)
⊢ {a | ¬⟪↑v', ↑(↑(stereographic' n v).symm a)⟫_ℝ = 1} =
    {a | ¬⟪↑v', stereoInvFunAux (↑v) ((ℝ ∙ ↑v)ᗮ.subtypeL (U.symm a))⟫_ℝ = 1}

Tactic:
rfl

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

Goal state before:
pp: case e'_3.ht
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ -↑v ∈ ℝ ∙ ↑v

Tactic:
Submodule.neg_mem_iff

Goal state after:
case e'_3.ht
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ ↑v ∈ ℝ ∙ ↑v