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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
this : MapsTo (fun x ↦ (x, g x)) t (t ×ˢ u)
x : N
hx : ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) (id x, g x)
h'x : x ∈ t
⊢ ContMDiffWithinAt I I' 1 (f x) u (g x)

Tactic:
apply hx.comp (g x) (contMDiffWithinAt_const.prodMk contMDiffWithinAt_id)

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := ⋯
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
this : MapsTo (fun x ↦ (x, g x)) t (t ×ˢ u)
x : N
hx : ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) (id x, g x)
h'x : x ∈ t
⊢ MapsTo (Prod.mk (id x)) u (t ×ˢ u)
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'
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
E'' : Type u_9
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
g : M' → M''
f : M → M'
V : (x : M'') → TangentSpace I'' x
s : Set M
t : Set M'
x₀ : M
hg : MDiffAt[t] g (f x₀)
h : MapsTo f s t
hu : UniqueMDiffAt[s] x₀
hf' : (mfderiv[s] f x₀).IsInvertible
⊢ mpullbackWithin I I'' (g ∘ f) V s x₀ = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀

Tactic:
by
  simp only [mpullbackWithin]
  have hf : MDifferentiableWithinAt I I' f s x₀ :=
    mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf'
  rw [mfderivWithin_comp _ hg hf h hu, IsInvertible.inverse_comp_apply_of_right hf',
    Function.comp_apply]

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

Goal state before:
pp: case hV
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
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)

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: 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)

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: case hV
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField u x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: case hV₁
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: 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
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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

Goal state before:
pp: 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
u v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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
c : 𝕜
v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1

Tactic:
exact mdifferentiableAt_mulInvariantVectorField _

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'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderiv[u] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : (mfderiv[s] f x₀).IsInvertible
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullbackWithin I I' f V u x⟩) s x₀

Tactic:
apply (hV.mpullbackWithin_vectorField_of_mem (hf.mono hu) hh hx₀ hs hmn
    hst).congr_of_eventuallyEq_of_mem _ hx₀

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
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'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderiv[u] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
hh : (mfderiv[s] f x₀).IsInvertible
⊢ (fun x ↦ ⟨x, mpullbackWithin I I' f V u x⟩) =ᶠ[𝓝[s] x₀] fun x ↦ ⟨x, mpullbackWithin I I' f V s x⟩
Module: Mathlib.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
e✝ : α ≃ β
inst✝³ : TopologicalSpace β
inst✝² : AddCommMonoid β
inst✝¹ : Semiring R
inst✝ : Module R β
e : α ≃ β
this✝¹ : TopologicalSpace α := e.topologicalSpace
this✝ : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (linearEquiv R e).invFun

Tactic:
simp +instances only [Equiv.topologicalSpace, toFun_as_coe, ← coinduced_symm]
      exact continuous_coinduced_rng

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
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'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

Tactic:
have A' : x₀ = (extChartAt I x₀).symm (extChartAt I x₀ x₀) := by simp

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
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'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ closure (f ⁻¹' Ici a) = f ⁻¹' Ici a

Tactic:
rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ici]

Goal state after:
case hfc
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (PiLp p fun x ↦ ℝ) → ℝ := fun x ↦ x.ofLp i
⊢ Continuous fun f ↦ f.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ closure {y | a ≤ y.ofLp i} = {y | a ≤ y.ofLp i}

Tactic:
let f : PiLp p (fun _ : Fin n ↦ ℝ) → ℝ := fun x ↦ x i
  change closure (f ⁻¹' Ici a) = f ⁻¹' Ici a
  rw [← (PiLp.isOpenMap_apply p _ i).preimage_closure_eq_closure_preimage, closure_Ici]
  fun_prop

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
⊢ (fderivWithin ℝ id (Icc x y) ↑z) 1 = 1

Tactic:
fderivWithin_id (uniqueDiffOn_Icc h.out _ z.2)

Goal state after:
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
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

Goal state before:
pp: 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₀ : ℝ
h : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
Filter.eventually_iff_exists_mem

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₀ : ℝ
h : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt% γ y (ContinuousLinearMap.smulRight 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

Goal state before:
pp: 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 : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ ∀ᶠ (t : ℝ) in 𝓝 t₀, HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
Filter.eventually_iff_exists_mem

Goal state after:
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 : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt% γ y (ContinuousLinearMap.smulRight 1 (v (γ y)))
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0

Tactic:
convert! stereographic_apply_neg (-v)
  ext1
  simp

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : ↥V → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (fun x ↦ f (i x)) x

Tactic:
change ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x

Goal state after:
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : ↥V → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁶ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁵ : NormedAddCommGroup EM
inst✝²⁴ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace 𝕜 E
H : Type u_5
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M)) (smoothPresheafCommRing IM I M R)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _
      (CategoryTheory.forget CommRingCat)]
    exact (smoothSheaf IM I M R).property

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.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
inst✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
⊢ ∃ u ∈ 𝓝 x, IsClosed[inst✝⁵] u ∧ u ⊆ s ∧ u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C} ∧ u ⊆ (extChartAt I x).source

Tactic:
have := Filter.inter_mem (Filter.inter_mem hs hC) (extChartAt_source_mem_nhds (I := I) x)

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✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
this : s ∩ {x_1 | (fun y ↦ ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C) x_1} ∩ (extChartAt I x).source ∈ 𝓝 x
⊢ ∃ u ∈ 𝓝 x, IsClosed[inst✝⁵] u ∧ u ⊆ s ∧ u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C} ∧ u ⊆ (extChartAt I x).source
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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_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 : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hu'u : u' ⊆ u
⊢ ∀ {x : M}, x ∈ u' → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ s x_1 x)

Tactic:
intro x hx
    exact hs.generating (hu'u hx)

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

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_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
inst✝⁵ : VectorBundle 𝕜 F V
inst✝⁴ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
t : Set M
k : ℕ∞ω
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
ht : IsOpen[inst✝¹⁴] t
ht' : t ⊆ e.baseSet
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) t ↔
    ∀ (i : ι), ContMDiffOn I 𝓘(𝕜, 𝕜) k ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) t

Tactic:
refine ⟨fun h i ↦ contMDiffOn_localFrameCoeff b ht ht' h _, fun h x hx ↦ ?_⟩
  exact (contMDiffAt_iff_localFrameCoeff b (ht' hx)).mpr
    (fun i ↦ (h i x hx).contMDiffAt (ht.mem_nhds hx)) |>.contMDiffWithinAt

Goal state after: