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

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
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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
⊢ writtenInExtChartAt I I'' x (g ∘ f) =ᶠ[𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x]
    writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f

Tactic:
apply
    @Filter.mem_of_superset _ _ (f ∘ (extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source) _
      (extChartAt_preimage_mem_nhdsWithin
        (h.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds _)))

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
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'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
s : Set M
g : M' → M''
h : ContinuousWithinAt f s x
⊢ f ∘ ↑(extChartAt I x).symm ⁻¹' (extChartAt I' (f x)).source ⊆
    {x_1 |
      (fun x_2 ↦
          writtenInExtChartAt I I'' x (g ∘ f) x_2 =
            (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) x_2)
        x_1}
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ↑e' (↑e.symm (b, v)) = (b, (coordChangeL R e e' b) v)

Tactic:
by
  rw [e.mk_coordChangeL e' hb, e.mk_symm hb.1]

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

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝² b] (e.symm b)

Tactic:
convert (e.symmL R b).continuous; ext; simp [hb]

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

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜₁
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝¹³ : TopologicalSpace B'
inst✝¹² : NormedSpace 𝕜₁ F
inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
x✝ : F
⊢ (⇑(Trivialization.continuousLinearMapAt 𝕜₂ (trivializationAt F' E' y₀) y) ∘
        ⇑ϕ ∘ ⇑(Trivialization.symmL 𝕜₁ (trivializationAt F E x₀) x))
      x✝ =
    (⇑(Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy) ∘
        ⇑ϕ ∘ ⇑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)
      x✝

Tactic:
Trivialization.coe_continuousLinearEquivAt_eq,

Goal state after:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁹ : (x : B) → AddCommMonoid (E x)
inst✝¹⁸ : NormedAddCommGroup F
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜₁
inst✝¹⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝¹³ : TopologicalSpace B'
inst✝¹² : NormedSpace 𝕜₁ F
inst✝¹¹ : (x : B) → Module 𝕜₁ (E x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst✝⁹ : NormedAddCommGroup F'
inst✝⁸ : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst✝⁷ : (x : B') → AddCommMonoid (E' x)
inst✝⁶ : (x : B') → Module 𝕜₂ (E' x)
inst✝⁵ : TopologicalSpace (TotalSpace F' E')
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜₁ F E
inst✝² : (x : B') → TopologicalSpace (E' x)
inst✝¹ : FiberBundle F' E'
inst✝ : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : E x →SL[σ] E' y
hx : x ∈ (trivializationAt F E x₀).baseSet
hy : y ∈ (trivializationAt F' E' y₀).baseSet
x✝ : F
⊢ (⇑(Trivialization.continuousLinearMapAt 𝕜₂ (trivializationAt F' E' y₀) y) ∘
        ⇑ϕ ∘ ⇑(Trivialization.symmL 𝕜₁ (trivializationAt F E x₀) x))
      x✝ =
    (⇑(Trivialization.continuousLinearMapAt 𝕜₂ (trivializationAt F' E' y₀) y) ∘
        ⇑ϕ ∘ ⇑(Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm)
      x✝
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_1
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝¹⁹ : NormedAddCommGroup EB
inst✝¹⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁶ : TopologicalSpace B
inst✝¹⁵ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
inst✝⁹ : (x : B) → AddCommMonoid (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✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
inst✝ : IsManifold IB n B
e : Trivialization F TotalSpace.proj
he : e ∈ trivializationAtlas F E
e' : Trivialization F TotalSpace.proj
he' : e' ∈ trivializationAtlas F E
this✝ : MemTrivializationAtlas e
this : MemTrivializationAtlas e'
⊢ (FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯).source =
    (((fun e ↦ e.toOpenPartialHomeomorph) e).symm ≫ₕ (fun e ↦ e.toOpenPartialHomeomorph) e').source

Tactic:
simp only [FiberwiseLinear.openPartialHomeomorph, trans_toPartialEquiv, symm_toPartialEquiv,
        e.symm_trans_source_eq e']

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (TotalSpace.toProd H E).toFun

Tactic:
let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
⊢ Continuous[_, instTopologicalSpaceModelProd H E] (TotalSpace.toProd H E).toFun
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun

Tactic:
let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩

Goal state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
p : TangentBundle I H := ⟨↑I.symm 0, 0⟩
⊢ Continuous[instTopologicalSpaceModelProd H E, _] (TotalSpace.toProd H E).invFun
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: case hy
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffAt[(extChartAt I x).source] (↑(extChartAt I x).symm y)
this :
  mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    mfderiv[(extChartAt I x).source] ↑(extChartAt I x) (↑(extChartAt I x).symm y)
⊢ ↑(extChartAt I x) (↑(extChartAt I x).symm y) = y

Tactic:
exact PartialEquiv.right_inv (extChartAt I x) hy

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        (↑((chartAt H x).prod (OpenPartialHomeomorph.refl F)).symm
          (↑(I.prod (PartialEquiv.refl F)).symm (z, w)))).proj ∈
    s

Tactic:
rw [PartialEquiv.prod_symm, PartialEquiv.refl_symm, PartialEquiv.prod_coe,
      ModelWithCorners.toPartialEquiv_coe_symm, PartialEquiv.refl_coe,
      OpenPartialHomeomorph.prod_symm, OpenPartialHomeomorph.refl_symm,
      OpenPartialHomeomorph.prod_apply, OpenPartialHomeomorph.refl_apply]

Goal state after:
case left
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
x : M
v : Z x
hs : UniqueMDiffAt[s] ⟨x, v⟩.proj
h's : s ⊆ (trivializationAt F Z ⟨x, v⟩.proj).baseSet
z : E
w : F
hz : ↑(chartAt H x).symm (↑I.symm z) ∈ s ∧ ∃ y, ↑I y = z
⊢ (↑(trivializationAt F Z x).symm
        ((fun p ↦ (↑(chartAt H x).symm p.1, id p.2)) ((fun p ↦ (↑I.symm p.1, id p.2)) (z, w)))).proj ∈
    s
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy
  have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
    rwa [← extChartAt_source (I := I)]
  have U' : UniqueMDiffAt[(extChartAt I x).source] ((extChartAt I x).symm y) :=
    (isOpen_extChartAt_source x).uniqueMDiffWithinAt h'y
  have : mfderiv% (extChartAt I x) ((extChartAt I x).symm y)
      = mfderiv[(extChartAt I x).source] (extChartAt I x) ((extChartAt I x).symm y) := by
    rw [mfderivWithin_eq_mfderiv U']
    exact mdifferentiableAt_extChartAt h''y
  rw [this, ← mfderivWithin_comp_of_eq]; rotate_left
  · exact mdifferentiableWithinAt_extChartAt_symm hy
  · exact (mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt
  · intro z hz
    apply extChartAt_target_subset_range x
    exact PartialEquiv.map_source (extChartAt I x) hz
  · exact U'
  · exact PartialEquiv.right_inv (extChartAt I x) hy
  rw [← mfderivWithin_id U']
  apply Filter.EventuallyEq.mfderivWithin_eq
  · filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz
    simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]
  · simp only [Function.comp_def, PartialEquiv.right_inv (extChartAt I x) hy, id_eq]

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

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
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) n id

Tactic:
exact contMDiff_id

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SMul

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
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) n id

Tactic:
exact contMDiff_id

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

Goal state before:
pp: case h
𝕜 : 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
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) u x₀
u' : Set M
hu' : u' ∈ nhds x₀
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}.Finite
s : Set ι := ⋯
this✝ : Fintype ↑{i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
this : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑ i ∈ s.toFinset, t i x⟩) (u ∩ u') x₀
i : ι
hi : i ∉ ↑s.toFinset
h : t i x₀ ≠ 0
⊢ x₀ ∈ {x | ¬t i x = 0} ∩ u'

Tactic:
simpa using ⟨h, mem_of_mem_nhds hu'⟩

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

Goal state before:
pp: E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : IsManifold I ∞ M
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
hd : s ⊆ interior t
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
rcases exists_contMDiffMap_zero_one_nhds_of_isClosed I isOpen_interior.isClosed_compl hs
    (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) (n := n) with ⟨f, h0, h1, hf⟩
  refine ⟨f, h1, fun x hx ↦ ?_, hf⟩
  exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x ↦ ⟪c, f x⟫_𝕜) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ f x = 0

Tactic:
← @inner_self_eq_zero 𝕜

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x ↦ ⟪c, f x⟫_𝕜) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ ⟪f x, f x⟫_𝕜 = 0
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ Function.extend Subtype.val g 0 x • f x = 0

Tactic:
Function.extend_apply' _ _ _ (mt _ hx)

Goal state after:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ 0 x • f x = 0

E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : M), Function.extend Subtype.val g 0 x • f x ∂μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
x : M
hx : x ∉ ↑U
⊢ (∃ a, ↑a = x) → x ∈ ↑U