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

Goal state before:
pp: case hs
𝕜 : 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 (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
this :
  ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 (↑(extChartAt I x₀) x₀)]
    ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' u)

Tactic:
]

Goal state after:
case hs
𝕜 : 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 (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
this :
  ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 (↑(extChartAt I x₀) x₀)]
    ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' u)
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ √⟪v, v⟫ = √⟪v, v⟫

Tactic:
]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) t) 1‖ₑ =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) t) 1‖ₑ =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : z ∈ Icc 0 1
⊢ ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) z) 1‖ₑ =
    ‖(fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y)) z) 1‖ₑ

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : z ∈ Icc 0 1
⊢ ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) z) 1‖ₑ =
    ‖(fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y)) z) 1‖ₑ
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ edist x y ≤ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] (⇑γ ∘ projIcc 0 1 ⋯) t) 1‖ₑ

Tactic:
]

Goal state after:
case refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ edist x y ≤ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] (⇑γ ∘ projIcc 0 1 ⋯) t) 1‖ₑ
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 f (inclusion hUV x)

Tactic:
]

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 (inclusion hUV x)
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
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
x : ↥V
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ ⇑i)
x' : ↥U := ⟨↑x, hxU⟩
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x'

Tactic:
]

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
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
x : ↥V
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ ⇑i)
x' : ↥U := ⟨↑x, hxU⟩
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x'
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
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ ContDiffOn ℝ 1 (⇑γ) (Icc 0 1)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ ContDiffOn ℝ 1 (⇑γ) (Icc 0 1)
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (⇑γ) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] ⇑γ t) 1‖ₑ = edist x y

Tactic:
]

Goal state after:
case refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (⇑γ) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] ⇑γ t) 1‖ₑ = edist x y
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
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens ↑(TopCat.of P))ᵒᵖ
g : (smoothSheaf IP I P N).obj.obj U
⊢ ContMDiff IM IP ∞ (Subtype.val ∘ (unop U).1.restrictPreimage f)

Tactic:
]

Goal state after:
𝕜 : 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
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens ↑(TopCat.of P))ᵒᵖ
g : (smoothSheaf IP I P N).obj.obj U
⊢ ContMDiff IM IP ∞ (Subtype.val ∘ (unop U).1.restrictPreimage f)
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
F₁ : Type u_4
inst✝¹ : NormedAddCommGroup F₁
inst✝ : InnerProductSpace ℝ F₁
⊢ ∀ (x : B), ContinuousAt (fun x ↦ TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)) x

Tactic:
]

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
F₁ : Type u_4
inst✝¹ : NormedAddCommGroup F₁
inst✝ : InnerProductSpace ℝ F₁
⊢ ∀ (x : B), ContinuousAt (fun x ↦ TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)) 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✝¹ : Group G
inst✝ : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G) (CategoryTheory.forget GrpCat))

Tactic:
]

Goal state after:
𝕜 : 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✝¹ : Group G
inst✝ : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G) (CategoryTheory.forget GrpCat))
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✝³ : CommGroup A
inst✝² : CommGroup A'
inst✝¹ : LieGroup I ∞ A
inst✝ : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A) (CategoryTheory.forget CommGrpCat))

Tactic:
]

Goal state after:
𝕜 : 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✝³ : CommGroup A
inst✝² : CommGroup A'
inst✝¹ : LieGroup I ∞ A
inst✝ : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A) (CategoryTheory.forget CommGrpCat))
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
F₁ : Type u_4
inst✝¹ : NormedAddCommGroup F₁
inst✝ : InnerProductSpace ℝ F₁
x : B
⊢ ContinuousAt (fun x ↦ (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)).proj) x ∧
    ContinuousAt
      (fun x_1 ↦
        (↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun x ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)).proj)
            (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1 ((fun x ↦ innerSL ℝ) x_1))).2)
      x

Tactic:
]

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
F₁ : Type u_4
inst✝¹ : NormedAddCommGroup F₁
inst✝ : InnerProductSpace ℝ F₁
x : B
⊢ ContinuousAt (fun x ↦ (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)).proj) x ∧
    ContinuousAt
      (fun x_1 ↦
        (↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun x ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) x)).proj)
            (TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1 ((fun x ↦ innerSL ℝ) x_1))).2)
      x
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
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
⊢ y ∈ (chartAt H x).source → ‖mfderiv% ↑(extChartAt I x) y‖ < C

Tactic:
h'y

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
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
h'y : y ∈ (chartAt H x).source
⊢ ‖mfderiv% ↑(extChartAt I x) y‖ < C
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✝¹ : Ring R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R) (CategoryTheory.forget RingCat))

Tactic:
]

Goal state after:
𝕜 : 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✝¹ : Ring R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R) (CategoryTheory.forget RingCat))