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

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'
f : M → M'
x : M
y : M'
n : ℕ∞ω
inst✝ : IsManifold I' n M'
hy : f x ∈ (chartAt H' y).source
⊢ ContMDiffWithinAt I I' n f univ x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x

Tactic:
contMDiffWithinAt_iff_target_of_mem_source hy,

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'
f : M → M'
x : M
y : M'
n : ℕ∞ω
inst✝ : IsManifold I' n M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f univ x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) = μ.restrict (u '' s)
⊢ Measure.map (s.domRestrict f) (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)

Tactic:
rw [uf.image_eq] at A

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A : Measure.map F (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) = μ.restrict (f '' s)
⊢ Measure.map (s.domRestrict f) (Measure.comap Subtype.val (μ.withDensity fun x ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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'
f : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
z : E
hz :
  z ∈ (extChartAt I x).target ∧ ↑(extChartAt I x).symm z ∈ s ∧ f (↑(extChartAt I x).symm z) ∈ (extChartAt I' y).source
⊢ ↑(extChartAt I x).symm z ∈ s

Tactic:
exact hz.2.1

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)
⊢ HasFDerivWithinAt f f' Set.univ x ↔ HasFDerivAt f f' x

Tactic:
hasFDerivWithinAt_univ

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)
⊢ HasFDerivAt f f' x ↔ HasFDerivAt f f' x
Module: Mathlib.Geometry.Manifold.ContMDiff.Defs

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'
f f₁ : M → M'
n : ℕ∞ω
h₁ : ∀ (y : M), f₁ y = f y
⊢ ContMDiff I I' n f₁ ↔ ContMDiff I I' n f

Tactic:
simp_rw [← contMDiffOn_univ]
  exact contMDiffOn_congr fun y _ ↦ h₁ y

Goal state after:
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'
f : M → M'
s : Set M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f s x →
    (LiftPropWithinAt (DifferentiableWithinAtProp I I') (↑(chartAt H' y) ∘ f) s x ↔
      LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) (↑(extChartAt I' y) ∘ f) s x)

Tactic:
intro hf

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'
f : M → M'
s : Set M
inst✝ : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
hf : ContinuousWithinAt f s x
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') (↑(chartAt H' y) ∘ f) s x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) (↑(extChartAt I' y) ∘ f) s x
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'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
⊢ mfderiv[s ∩ t] f x = mfderiv[s] f x

Tactic:
by
  rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
n : ℕ∞ω
⊢ ∀ (e e' : OpenPartialHomeomorph (B × F) (B × F)),
    e ∈
        ⋃ φ,
          ⋃ U,
            ⋃ (hU : IsOpen[inst✝⁷] U),
              ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                  {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)} →
      e' ≈ e →
        e' ∈
          ⋃ φ,
            ⋃ U,
              ⋃ (hU : IsOpen[inst✝⁷] U),
                ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x)) U),
                  ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x ↦ ↑(φ x).symm) U),
                    {e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU ⋯ ⋯)}

Tactic:
simp only [mem_aux]
    rintro e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ hee'
    exact ⟨φ, U, hU, hφ, h2φ, Setoid.trans hee' heφ⟩

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
⊢ ContinuousWithinAt f s x₀ →
    (ContMDiffWithinAt IM 𝓘(𝕜, EB × F) n (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) s x₀ ↔
      ContMDiffWithinAt IM 𝓘(𝕜, EB) n (↑(extChartAt IB (f x₀).proj) ∘ fun x ↦ (f x).proj) s x₀ ∧
        ContMDiffWithinAt IM 𝓘(𝕜, F) n
          (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x ↦
            (↑(trivializationAt F E (f x₀).proj) (f x)).2)
          s x₀)

Tactic:
intro hf

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ ContMDiffWithinAt IM 𝓘(𝕜, EB × F) n (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) s x₀ ↔
    ContMDiffWithinAt IM 𝓘(𝕜, EB) n (↑(extChartAt IB (f x₀).proj) ∘ fun x ↦ (f x).proj) s x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n
        (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x ↦
          (↑(trivializationAt F E (f x₀).proj) (f x)).2)
        s x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case hs
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ (chartAt (ModelProd H E) p).source = (TotalSpace.toProd H E).toPartialEquiv.source

Tactic:
TangentBundle.chartAt,

Goal state after:
case hs
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ (((tangentBundleCore I H).toFiberBundleCore.localTriv (achart H p.proj)).toOpenPartialHomeomorph ≫ₕ
        (chartAt H p.proj).prod (OpenPartialHomeomorph.refl E)).source =
    (TotalSpace.toProd H E).toPartialEquiv.source
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case right
𝕜 : 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
⊢ ∃ y, Prod.map (↑I) id y = (z, w)

Tactic:
· rcases hz.2 with ⟨u, rfl⟩
    exact ⟨(u, w), rfl⟩

Goal state after:
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 y : M
hy : y ∈ (extChartAt I x).source
this : y = ↑(extChartAt I x).symm (↑(extChartAt I x) y)
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)

Tactic:
convert! mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt ((extChartAt I x).map_source hy)

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

Tactic:
rw [mfderiv_extChartAt_self, ContinuousLinearMap.comp_id] at hcomp

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
inst✝ : IsManifold I 1 M
x : M
hcomp : mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst✝²] (s a)
hu : ⋃ a, s a = univ
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
choose U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)
    simp only [← hU] at hu ⊢
    have heU : range e ⊆ ⋃ i, U i := by
      simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using! hu
    rcases precise_refinement_set he.isClosed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩
    refine ⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_,
      hVf.preimage_continuous he.continuous, fun a ↦ ⟨a, preimage_mono (hVU a)⟩⟩
    simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using! heV

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
i : ι
hi : i ∈ chainSupCarrier c
⊢ p ((find c ne i).toFun i)

Tactic:
obtain ⟨v, hv⟩ := Set.mem_iUnion.mp hi
    simp only [mem_iUnion, exists_prop] at hv
    rw [find_apply_of_mem hc ne hv.1 hv.2]
    exact v.pred_of_mem hv.2

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
⊢ j ∉ insert i v.carrier → update v.toFun i vi j = u j

Tactic:
hj

Goal state after:
case refine_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
hj : j ∉ insert i v.carrier
⊢ update v.toFun i vi j = u j
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
⊢ IsOpen (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)

Tactic:
apply isOpen_biUnion

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := ⋯
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
⊢ ∀ i_1 ∈ fun i_2 ↦ i_2 = i → False, IsOpen (v.toFun i_1)
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : {i | ((fun i ↦ support ⇑(f i)) i ∩ U).Nonempty}.Finite
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
⊢ (f j) y ≠ 0 → j ∈ hf.toFinset

Tactic:
hj

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : {i | ((fun i ↦ support ⇑(f i)) i ∩ U).Nonempty}.Finite
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
hj : (f j) y ≠ 0
⊢ j ∈ hf.toFinset
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_4
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
⊢ j ∈ insert i v.carrier → IsCompact (closure (update v.toFun i vi j))

Tactic:
hj

Goal state after:
case refine_4
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j ∈ insert i v.carrier
⊢ IsCompact (closure (update v.toFun i vi j))
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_5
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
⊢ j ∉ insert i v.carrier → update v.toFun i vi j = u j

Tactic:
hj

Goal state after:
case refine_5
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j ∉ insert i v.carrier
⊢ update v.toFun i vi j = u j
Module: Mathlib.Order.Filter.Germ.OrderedMonoid

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f g : l.Germ β
x✝³ x✝² : α → β
H✝ : ↑x✝³ ≤ ↑x✝²
h : l.Germ β
x✝¹ : α → β
x✝ : α
H : x✝³ x✝ ≤ x✝² x✝
⊢ (fun f g x ↦ (fun x1 x2 ↦ x1 * x2) (f x) (g x)) x✝³ x✝¹ x✝ ≤
    (fun f g x ↦ (fun x1 x2 ↦ x1 * x2) (f x) (g x)) x✝² x✝¹ x✝

Tactic:
by dsimp; gcongr

Goal state after: