mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝² : M✝
𝕜 : 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 e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ φ.source ∈ 𝓝 (↑(e.extend I) x)

Tactic:
simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]

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✝
n✝ : WithTop ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝² : M✝
𝕜 : 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 e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ↑(e.extend I).symm ⁻¹' e'.source ∈ 𝓝 (↑(e.extend I) x)
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
x₀ : B
hs : ∀ i ∈ s, MDiffAt (T% t) x₀
⊢ (MDiffAt fun x ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
by
  simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢
  exact MDifferentiableWithinAt.sum_section hs

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

Goal state before:
pp: 𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst✝³¹ : NontriviallyNormedField 𝕜
inst✝³⁰ : (x : B₁) → AddCommGroup (E₁ x)
inst✝²⁹ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝²⁸ : NormedAddCommGroup F₁
inst✝²⁷ : NormedSpace 𝕜 F₁
inst✝²⁶ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁵ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝²⁴ : (x : B₂) → AddCommGroup (E₂ x)
inst✝²³ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝²² : NormedAddCommGroup F₂
inst✝²¹ : NormedSpace 𝕜 F₂
inst✝²⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁹ : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
inst✝⁶ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
n : WithTop ℕ∞
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContMDiffWithinAt IM IB₁ n (fun x ↦ ⟨b₁ x, v x⟩.proj) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) n (fun x ↦ (↑(trivializationAt F₁ E₁ ⟨b₁ m₀, v m₀⟩.proj) ⟨b₁ x, v x⟩).2) (insert m₀ s)
      m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet
A' : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ (trivializationAt F₂ E₂ (b₂ m₀)).baseSet
m : M
hm : b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet
h'm : b₂ m ∈ (trivializationAt F₂ E₂ (b₂ m₀)).baseSet
⊢ (↑(trivializationAt F₂ E₂ (b₂ m₀)) ⟨b₂ m, (ϕ m) (v m)⟩).2 =
    (↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ (b₂ m₀)) (b₂ m) h'm) ∘SL
        ϕ m ∘SL ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ (b₁ m₀)) (b₁ m) hm).symm)
      (↑(trivializationAt F₁ E₁ (b₁ m₀)) ⟨b₁ m, v m⟩).2

Tactic:
simp [*]

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
W : (x : M) → TangentSpace I x
⊢ mlieBracket I 0 W = 0

Tactic:
simp [← mlieBracketWithin_univ]

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
W : (x : M) → TangentSpace I x
⊢ mlieBracket I W 0 = 0

Tactic:
simp [← mlieBracketWithin_univ]

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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
this :
  (MDiffAt[range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s] fun x_1 ↦
      ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
    (↑(extChartAt I x) x)
⊢ MDiffAt[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x) x)

Tactic:
inter_comm

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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
this :
  (MDiffAt[range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s] fun x_1 ↦
      ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
    (↑(extChartAt I x) x)
⊢ MDiffAt[range ↑I ∩ ↑(extChartAt I x).symm ⁻¹' s] (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
H : Type u_7
inst✝³ : TopologicalSpace H
G : Type u_9
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝¹ : TopologicalSpace M
N : Type u_13
inst✝ : TopologicalSpace N
f : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst✝¹] s
x✝ : ImmersionAtProp F I J M N f φ ψ
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
⊢ ((φ.restr s).extend I).target ⊆ (φ.extend I).target

Tactic:
by simp; grind

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
rw [isMIntegralCurveAt_iff]
  constructor
  · intro ⟨s, hs, h⟩
    rw [Metric.mem_nhds_iff] at hs
    obtain ⟨ε, hε, hε'⟩ := hs
    refine ⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩
  · intro ⟨ε, hε, h⟩
    exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

Goal state after:
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
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
⊢ HasMFDerivAt% (fun t ↦ γ (|t| + 1) t) t (ContinuousLinearMap.smulRight 1 (v ((fun t ↦ γ (|t| + 1) t) t)))

Tactic:
have ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1) := by
    rw [mem_Ioo, ← abs_lt]
    exact lt_add_one _

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
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ HasMFDerivAt% (fun t ↦ γ (|t| + 1) t) t (ContinuousLinearMap.smulRight 1 (v ((fun t ↦ γ (|t| + 1) t) t)))
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₀).symm ⁻¹' u ∩ (extChartAt I x₀).target)

Tactic:
inter_comm

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.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₁
⊢ IsContinuousRiemannianBundle F₁ (Trivial B F₁)

Tactic:
refine ⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩

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₁
⊢ Continuous[inst✝⁹,
      topologicalSpaceTotalSpace (RingHom.id ℝ) F₁ (Trivial B F₁) (F₁ →L[ℝ] ℝ) fun x ↦ Trivial B F₁ x →L[ℝ] ℝ]
    fun x ↦ TotalSpace.mk' (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x ((fun x ↦ innerSL ℝ) 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:
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _
      (CategoryTheory.forget CommRingCat)

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✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafCommRing IM I M R) (CategoryTheory.forget CommRingCat))
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
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ UniqueDiffOn 𝕜 (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target)

Tactic:
inter_comm

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
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' s)
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case ht
𝕜 : 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
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ UniqueDiffOn 𝕜 (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target)

Tactic:
inter_comm

Goal state after:
case ht
𝕜 : 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
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ UniqueDiffOn 𝕜 ((extChartAt I x₀).target ∩ ↑(extChartAt I x₀).symm ⁻¹' u)