mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [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.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
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ IsLocalHomeomorphOn f s

Tactic:
by
  apply IsLocalHomeomorphOn.mk
  intro x hx
  choose U hyp using hf ⟨x, hx⟩
  exact ⟨U.toOpenPartialHomeomorph, hyp⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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 : WithTop ℕ∞
inst✝ : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
hx : x ∈ e.source
⊢ I.IsInteriorPoint x ↔ ↑(e.extend I) x ∈ interior (e.extend I).target

Tactic:
rw [isInteriorPoint_iff]
  exact mem_interior_range_iff_of_mem_atlas hn (chart_mem_atlas H x) he (mem_chart_source H x) hx

Goal state after:
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 Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ⁅X + Y, Z⁆ f✝ = (⁅X, Z⁆ + ⁅Y, Z⁆) f✝

Tactic:
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]

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 Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (Z f✝) + Y (Z f✝) - (Z (X f✝) + Z (Y f✝)) = X (Z f✝) - Z (X f✝) + (Y (Z f✝) - Z (Y f✝))
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 Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ ⁅X, Y + Z⁆ f✝ = (⁅X, Y⁆ + ⁅X, Z⁆) f✝

Tactic:
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]

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 Y Z : LeftInvariantDerivation I G
f✝ : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ X (Y f✝) + X (Z f✝) - (Y (X f✝) + Z (X f✝)) = X (Y f✝) - Y (X f✝) + (X (Z f✝) - Z (X f✝))
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
⊢ mpullback 𝓘(𝕜, E) 𝓘(𝕜, E') f V = pullback 𝕜 f V

Tactic:
by
  simp only [← mpullbackWithin_univ, ← pullbackWithin_univ, mpullbackWithin_eq_pullbackWithin]

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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiffAt f x
hg : MDiffAt g x
⊢ ↑(fromTangentSpace ((f • g) x)) ∘SL mfderiv% (f • g) x =
    f x • ↑(fromTangentSpace (g x)) ∘SL mfderiv% g x +
      toSpanSingleton 𝕜 (g x) ∘SL ↑(fromTangentSpace (f x)) ∘SL mfderiv% f x

Tactic:
mfderiv_smul hf hg

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
x : M
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
hf : MDiffAt f x
hg : MDiffAt g x
⊢ ↑(fromTangentSpace ((f • g) x)) ∘SL
      (f x • ↑(fromTangentSpace ((f • g) x)).symm ∘SL ↑(fromTangentSpace (g x)) ∘SL mfderiv% g x +
        toSpanSingleton 𝕜 ((fromTangentSpace ((f • g) x)).symm (g x)) ∘SL ↑(fromTangentSpace (f x)) ∘SL mfderiv% f x) =
    f x • ↑(fromTangentSpace (g x)) ∘SL mfderiv% g x +
      toSpanSingleton 𝕜 (g x) ∘SL ↑(fromTangentSpace (f x)) ∘SL mfderiv% f 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
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)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
let S := (S₃.comp S₂).comp S₁

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)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ContMDiff.comp (ContMDiff.comp S₃ S₂) S₁
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩
Module: Mathlib.Geometry.Manifold.Instances.Real

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

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

Goal state after:
x y : ℝ
h : Fact (x < y)
this✝ : IsOpen {z | z < y - x}
this : IsOpen {z | z.ofLp 0 < y - x}
⊢ IsOpen {z | (↑z).ofLp 0 < y - x}
Module: Mathlib.Geometry.Manifold.Instances.Icc

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

Tactic:
mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)

Goal state after:
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

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)

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
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : ℕ∞ω
h₀ : ContDiff ℝ ω fun w ↦ ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w ↦ (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ ω fun w ↦ 4 • w + (‖w‖ ^ 2 - 4) • v

Tactic:
refine (contDiff_const.smul contDiff_id).add ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
m : ℕ∞ω
h₀ : ContDiff ℝ ω fun w ↦ ‖w‖ ^ 2
h₁ : ContDiff ℝ ω fun w ↦ (‖w‖ ^ 2 + 4)⁻¹
⊢ ContDiff ℝ ω fun w ↦ (‖w‖ ^ 2 - 4) • v
Module: Mathlib.Geometry.Manifold.Instances.Sphere

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

Tactic:
_

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

Goal state before:
pp: case e'_3
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))ᗮ.subtype.range

Tactic:
simp only [Submodule.range_subtype, coe_neg_sphere]

Goal state after:
case e'_3
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)ᗮ
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a : ℝ
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
obtain ⟨y, ⟨γ, hγ1, hγ2⟩, hlt⟩ := hbdd a

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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a y : ℝ
hlt : a < y
γ : ℝ → M
hγ1 : γ 0 = x
hγ2 : IsMIntegralCurveOn γ v (Ioo (-y) y)
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: x : ↑I
⊢ volume {x} = 0

Tactic:
by simp [volume_apply]

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
⊢ Path x y

Tactic:
refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩ <;>
    simp [f, η, ContinuousAffineMap.coe_lineMap_eq, ha, hb]

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

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ

Tactic:
Metric.continuousAt_iff'

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ∀ ε > 0, ∀ᶠ (x_1 : B) in 𝓝 x, dist (g' x_1) (g' x) < ε
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : E ≃L[𝕜] E'' × F
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
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
⊢ IsSubmersionAt I J n f x

Tactic:
have aux : IsSubmersionAtOfComplement F I J n f x := by
    apply IsSubmersionAtOfComplement.mk_of_continuousAt <;> assumption

Goal state after:
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : E ≃L[𝕜] E'' × F
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
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
aux : IsSubmersionAtOfComplement F I J n f x
⊢ IsSubmersionAt I J n f x
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: case pos
𝕜 : 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_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
⊢ (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)

Tactic:
simp [coeff, hxe]

Goal state after:
case pos
𝕜 : 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_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
⊢ ((hs.toBasisAt ⋯).repr (t x)) i = ((hs'.toBasisAt ⋯).repr (t x)) i
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: case neg
𝕜 : 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_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∉ u
⊢ (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)

Tactic:
simp [coeff, hxe]

Goal state after: