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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : TangentSpace I x →L[𝕜] 𝕜
hs : HasMFDerivAt% f x (↑(fromTangentSpace (f x)).symm ∘SL f')
g' : TangentSpace I x →L[𝕜] V
hg : HasMFDerivAt% g x (↑(fromTangentSpace (g x)).symm ∘SL g')
⊢ HasMFDerivAt% (f • g) x
    (f x • ↑(fromTangentSpace ((f • g) x)).symm ∘SL g' +
      toSpanSingleton 𝕜 ((fromTangentSpace ((f • g) x)).symm (g x)) ∘SL f')

Tactic:
constructor

Goal state after:
case left
𝕜 : 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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : TangentSpace I x →L[𝕜] 𝕜
hs : HasMFDerivAt% f x (↑(fromTangentSpace (f x)).symm ∘SL f')
g' : TangentSpace I x →L[𝕜] V
hg : HasMFDerivAt% g x (↑(fromTangentSpace (g x)).symm ∘SL g')
⊢ ContinuousAt (f • g) x

case right
𝕜 : 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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : TangentSpace I x →L[𝕜] 𝕜
hs : HasMFDerivAt% f x (↑(fromTangentSpace (f x)).symm ∘SL f')
g' : TangentSpace I x →L[𝕜] V
hg : HasMFDerivAt% g x (↑(fromTangentSpace (g x)).symm ∘SL g')
⊢ HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, V) x (f • g))
    (f x • ↑(fromTangentSpace ((f • g) x)).symm ∘SL g' +
      toSpanSingleton 𝕜 ((fromTangentSpace ((f • g) x)).symm (g x)) ∘SL f')
    (range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

Goal state before:
pp: case right
𝕜 : 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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : TangentSpace I x →L[𝕜] 𝕜
hs : HasMFDerivAt% f x (↑(fromTangentSpace (f x)).symm ∘SL f')
g' : TangentSpace I x →L[𝕜] V
hg : HasMFDerivAt% g x (↑(fromTangentSpace (g x)).symm ∘SL g')
⊢ HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, V) x (f • g))
    (f x • ↑(fromTangentSpace ((f • g) x)).symm ∘SL g' +
      toSpanSingleton 𝕜 ((fromTangentSpace ((f • g) x)).symm (g x)) ∘SL f')
    (range ↑I) (↑(extChartAt I x) x)

Tactic:
simpa using! hs.2.smul hg.2

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
h : s ∈ 𝓝 x
⊢ mlieBracketWithin I V W (univ ∩ s) x = mlieBracketWithin I V W univ x

Tactic:
mlieBracketWithin_inter h

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
V W : (x : M) → TangentSpace I x
h : s ∈ 𝓝 x
⊢ mlieBracketWithin I V W univ x = mlieBracketWithin I V W univ x
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
v w : GroupLieAlgebra I G
g : G
⊢ mpullback I I (fun x ↦ g⁻¹ * x) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g

Tactic:
mpullback_mlieBracket (n := minSmoothness 𝕜 3),

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
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ mlieBracket I (mpullback I I (fun x ↦ g⁻¹ * x) (mulInvariantVectorField v))
      (mpullback I I (fun x ↦ g⁻¹ * x) (mulInvariantVectorField w)) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g

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
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)

case hW
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

case hf
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (minSmoothness 𝕜 3) (fun x ↦ g⁻¹ * x) g

case hn
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3
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
v w : GroupLieAlgebra I G
g : G
⊢ 2 ≤ 3

Tactic:
by norm_cast

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 := ⋯
⊢ ((mfderiv% ↑φ x).inverse ∘SL (mfderiv[range ↑I] ↑φ.symm (↑φ x)).inverse) Y =
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) Y

Tactic:
extChartAt_to_inv x,

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 := extChartAt I x
⊢ ((mfderiv% ↑φ x).inverse ∘SL (mfderiv[range ↑I] ↑φ.symm (↑φ x)).inverse) Y =
    (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) Y
Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Goal state before:
pp: case refine_4
𝕜 : 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 ⊆ g ⁻¹' hf.codChart.source

pp: case refine_5
𝕜 : 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
⊢ P g (hf.domChart.restr s) hf.codChart

Tactic:
· trans s' ∩ f ⁻¹' hf.codChart.source
    · apply subset_inter
      · exact Subset.trans (by simp [interior_eq_iff_isOpen.mpr hs]) hss'
      · exact Subset.trans (by simp) hf.source_subset_preimage_source
    · rw [hfg.inter_preimage_eq]; exact inter_subset_right

Goal state after:
case refine_5
𝕜 : 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
⊢ P g (hf.domChart.restr s) hf.codChart
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
⊢ {y | ∀ (i : Fin n), a ≤ y.ofLp i} = ⋂ i, f i ⁻¹' Ici a

Tactic:
ext

Goal state after:
n : ℕ
p : ℝ≥0∞
a : ℝ
f : Fin n → (PiLp p fun x ↦ ℝ) → ℝ := fun i x ↦ x.ofLp i
x✝ : PiLp p fun x ↦ ℝ
⊢ x✝ ∈ {y | ∀ (i : Fin n), a ≤ y.ofLp i} ↔ x✝ ∈ ⋂ i, f i ⁻¹' Ici a
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
⊢ {y | ∀ (i : Fin n), a < y.ofLp i} = ⋂ i, f i ⁻¹' Ioi a

Tactic:
ext

Goal state after:
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 ↦ ℝ
⊢ x✝ ∈ {y | ∀ (i : Fin n), a < y.ofLp i} ↔ x✝ ∈ ⋂ i, f i ⁻¹' Ioi a
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
x : EuclideanQuadrant n
x✝ : x ∈ univ
⊢ ⟨toLp 2 fun i ↦ max ((↑x).ofLp i) 0, ⋯⟩ = x

Tactic:
by ext i; simp only [x.2 i, sup_of_le_left]

Goal state after:
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
⊢ ↑(IccLeftChart x y).symm z = ⟨(↑z).ofLp 0 + x, ⋯⟩

Tactic:
ext

Goal state after:
x y : ℝ
hxy : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z).ofLp 0 ≤ y - x
⊢ ↑(↑(IccLeftChart x y).symm z) = ↑⟨(↑z).ofLp 0 + x, ⋯⟩
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
⊢ IsOpen {z | (↑z).ofLp 0 < y - x}

Tactic:
have : IsOpen { z : ℝ | z < y - x } := isOpen_Iio
    have : IsOpen { z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x } :=
      this.preimage (@PiLp.continuous_apply 2 (Fin 1) (fun _ ↦ ℝ) _ 0)
    exact this.preimage continuous_subtype_val

Goal state after:
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
⊢ ↑(IccRightChart x y).symm z = ⟨y - (↑z).ofLp 0, ⋯⟩

Tactic:
ext

Goal state after:
x y : ℝ
hxy : Fact (x < y)
z : EuclideanHalfSpace 1
hz : (↑z).ofLp 0 ≤ y - x
⊢ ↑(↑(IccRightChart x y).symm z) = ↑⟨y - (↑z).ofLp 0, ⋯⟩
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
⊢ MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) ↑w ↔ MDiffAt f w

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
  · have A := (contMDiff_subtypeVal_Icc (x := x) (y := y) w).mdifferentiableAt one_ne_zero
    rw [← mdifferentiableWithinAt_univ] at A ⊢
    convert! hf.comp _ A (fun z hz ↦ z.2)
    ext z
    simp
  · have := (contMDiffOn_projIcc (x := x) (y := y) w w.2).mdifferentiableWithinAt one_ne_zero
    exact MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq (w : ℝ) hf this (by simp)

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = 1

Tactic:
by
  change _ = oneTangentSpaceIcc (Set.projIcc x y h.out.le z)
  simp only [oneTangentSpaceIcc]
  congr
  simp [projIcc_of_mem h.out.le hz]

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
⊢ stereoInvFun hv (stereoToFun v ↑x) = x

Tactic:
ext

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
⊢ ↑(stereoInvFun hv (stereoToFun v ↑x)) = ↑x
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ (val ∘ fun x ↦ x.1 * x.2) = (fun x ↦ x.1 * x.2) ∘ fun x ↦ (↑x.1, ↑x.2)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ × Rˣ
⊢ (val ∘ fun x ↦ x.1 * x.2) x✝ = ((fun x ↦ x.1 * x.2) ∘ fun x ↦ (↑x.1, ↑x.2)) x✝
Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ (val ∘ fun x ↦ x⁻¹) = Ring.inverse ∘ val

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁸ : NormedRing R
inst✝⁷ : CompleteSpace R
n : ℕ∞ω
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra 𝕜 R
H : Type u_3
inst✝⁴ : TopologicalSpace H
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x✝ : Rˣ
⊢ (val ∘ fun x ↦ x⁻¹) x✝ = (Ring.inverse ∘ val) x✝
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₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
constructor

Goal state after:
case mp
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₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

case mpr
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₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀
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₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
constructor

Goal state after:
case mp
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₀ : ℝ
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

case mpr
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₀ : ℝ
⊢ (∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
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 ∈ (extChartAt I (γ t₀)).source
⊢ HasDerivWithinAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) s t

Tactic:
by
  -- turn `HasDerivWithinAt` into comp of `HasMFDerivWithinAt`
  replace hsrc := extChartAt_source I (γ t₀) ▸ hsrc
  rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← hasMFDerivWithinAt_iff_hasFDerivWithinAt]
  apply (HasMFDerivWithinAt.comp t (hasMFDerivWithinAt_extChartAt (I := I) hsrc) (hγ _ ht)
    (Set.subset_preimage_image _ _)).congr_mfderiv
  rw [ContinuousLinearMap.ext_iff]
  intro a
  rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
    ← one_apply_eq_self (F := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, ℝ) t) a,
    ← ContinuousLinearMap.smulRight_apply,
    mfderiv_chartAt_eq_tangentCoordChange hsrc]
  rfl

Goal state after:
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)
x : EuclideanSpace ℝ (Fin n)
⊢ ↑(↑(stereographic' n v).symm x) =
    let U := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr;
    (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • 4 • ↑(U.symm x) + (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • (‖↑(U.symm x)‖ ^ 2 - 4) • ↑v

Tactic:
simp [stereographic, stereographic', ← Submodule.coe_norm]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ Continuous Subtype.val ∧
    ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
      ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
        ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)

Tactic:
constructor

Goal state after:
case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ Continuous Subtype.val

case right
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ∀ (x : { x // x ∈ sphere 0 1 }) (y : E),
    ContDiffOn ℝ m (↑(extChartAt 𝓘(ℝ, E) y) ∘ Subtype.val ∘ ↑(extChartAt (𝓡 n) x).symm)
      ((extChartAt (𝓡 n) x).target ∩ ↑(extChartAt (𝓡 n) x).symm ⁻¹' Subtype.val ⁻¹' (extChartAt 𝓘(ℝ, E) y).source)
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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 ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
this :
  ContinuousLinearMap.smulRight 1 (a • v (γ (t * a))) =
    ContinuousLinearMap.smulRight 1 (v (γ (t * a))) ∘SL ContinuousLinearMap.smulRight 1 a
⊢ HasMFDerivAt[{t | t * a ∈ s}] (γ ∘ fun x ↦ x * a) t
    (ContinuousLinearMap.smulRight 1 (v (γ (t * a))) ∘SL ContinuousLinearMap.smulRight 1 a)

Tactic:
refine HasMFDerivWithinAt.comp t (hγ (t * a) ht)
    ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl

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 ℝ
hγ : IsMIntegralCurveOn γ v s
a t : ℝ
ht : t ∈ {t | t * a ∈ s}
this :
  ContinuousLinearMap.smulRight 1 (a • v (γ (t * a))) =
    ContinuousLinearMap.smulRight 1 (v (γ (t * a))) ∘SL ContinuousLinearMap.smulRight 1 a
⊢ HasFDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) t fun x ↦ x * a) (ContinuousLinearMap.smulRight 1 a)
    (↑(extChartAt 𝓘(ℝ, ℝ) t).symm ⁻¹' {t | t * a ∈ s} ∩ range ↑𝓘(ℝ, ℝ)) (↑(extChartAt 𝓘(ℝ, ℝ) t) t)