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'
s✝ : Set M
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert (↑(extChartAt I x) x)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))]
      ↑(extChartAt I x) x
hsub :
  v ⊆
    insert (↑(extChartAt I x) x)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) v
⊢ ↑(extChartAt I x).symm (↑(extChartAt I x) x) ∈ f ⁻¹' (extChartAt I' (f x)).source

Tactic:
rw [extChartAt_to_inv]

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
x : M
n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
s : Set M
hxs : x ∈ s
h : ContMDiffWithinAt I I' n f s x
v : Set E
hmem :
  v ∈
    𝓝[insert (↑(extChartAt I x) x)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))]
      ↑(extChartAt I x) x
hsub :
  v ⊆
    insert (↑(extChartAt I x) x)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
hv : ContDiffOn 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) v
⊢ x ∈ f ⁻¹' (extChartAt I' (f x)).source
Module: Mathlib.Geometry.Manifold.Algebra.LieGroup

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : Inv G
inst✝⁶ : Zero G
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 → G
inst✝ : ContinuousInv₀ G
this : T1Space G
⊢ ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I 0 (fun y ↦ y⁻¹) x

Tactic:
have A : CMDiff[{0}ᶜ] 0 (fun (x : G) ↦ x⁻¹) := by
    rw [contMDiffOn_zero_iff]
    exact continuousOn_inv₀

Goal state after:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : ℕ∞ω
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : Inv G
inst✝⁶ : Zero G
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 → G
inst✝ : ContinuousInv₀ G
this : T1Space G
A : ContMDiffOn I I 0 (fun x ↦ x⁻¹) {0}ᶜ
⊢ ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I 0 (fun y ↦ y⁻¹) 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 : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (chartAt H x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f s x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousWithinAt f s x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
        (↑(extChartAt I x) x')

Tactic:
← extChartAt_source I

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
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f s x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousWithinAt f s x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
        (↑(extChartAt I x) 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'
⊢ mfderiv[univ] f = mfderiv% f

Tactic:
ext x : 1

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
⊢ mfderiv[univ] f x = mfderiv% f x
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case refine_2
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'
b : B
v : F
hb : (b, v) ∈ (FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯).source
⊢ ↑(FiberwiseLinear.openPartialHomeomorph (Trivialization.coordChangeL 𝕜 e e') ⋯ ⋯ ⋯) (b, v) =
    ↑(((fun e ↦ e.toOpenPartialHomeomorph) e).symm ≫ₕ (fun e ↦ e.toOpenPartialHomeomorph) e') (b, v)

Tactic:
exact (e.apply_symm_apply_eq_coordChangeL e' hb.1 v).symm

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

Goal state before:
pp: 𝕜 : 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
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (chartAt H x).source

Tactic:
← extChartAt_source I

Goal state after:
𝕜 : 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
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (extChartAt I x).source
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: 𝕜 : 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).toPartialEquiv = (TotalSpace.toProd H E).toPartialEquiv

Tactic:
ext x : 1

Goal state after:
case h
𝕜 : 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 x : TangentBundle I H
⊢ ↑(chartAt (ModelProd H E) p).toPartialEquiv x = ↑(TotalSpace.toProd H E).toPartialEquiv x

case hsymm
𝕜 : 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
x : ModelProd H E
⊢ ↑(chartAt (ModelProd H E) p).symm x = ↑(TotalSpace.toProd H E).toPartialEquiv.symm x

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
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case sub2
𝕜 : 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'
s : Set M
x : M
hs : UniqueMDiffAt[s] x
f : M → M'
f' : E →L[𝕜] E'
hf : HasMFDerivAt[s] f x f'
hd : DenseRange ⇑f'
this : UniqueMDiffAt[s ∩ f ⁻¹' (extChartAt I' (f x)).source] x
⊢ writtenInExtChartAt I I' x f '' (↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) ∩ range ↑I) ⊆
    ↑(extChartAt I' (f x)).symm ⁻¹' f '' s ∩ range ↑I'

Tactic:
case sub2 =>
    rintro _ ⟨y, ⟨⟨hys, hfy⟩, -⟩, rfl⟩
    exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩

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

Goal state before:
pp: case neg
𝕜 : 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'
s : Set M
x : M
f : M → E'
hs : UniqueMDiffAt[s] x
hf : ¬MDiffAt[s] f x
⊢ (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)
    else 0) =
    -0

Tactic:
rw [← mdifferentiableWithinAt_neg] at hf

Goal state after:
case neg
𝕜 : 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'
s : Set M
x : M
f : M → E'
hs : UniqueMDiffAt[s] x
hf : ¬MDiffAt[s] (-f) x
⊢ (if MDiffAt[s] (-f) x then
      fderivWithin 𝕜 (writtenInExtChartAt I 𝓘(𝕜, E') x (-f)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)
    else 0) =
    -0
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
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)
z : M
hz : z ∈ (extChartAt I x).source
⊢ (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) z = id z

Tactic:
simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]

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

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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (chartAt H c).source

Tactic:
← extChartAt_source I

Goal state after:
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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (extChartAt I c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (extChartAt I c).source
Module: Mathlib.Geometry.Manifold.BumpFunction

Goal state before:
pp: case h₁.refine_1
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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s ⊆ range ↑I

Tactic:
rintro _ ⟨x, -, rfl⟩

Goal state after:
case h₁.refine_1
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
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
x : M
⊢ ↑(extChartAt I c) x ∈ range ↑I
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: X : Type v
inst✝ : TopologicalSpace X
ι : X → Sort u_1
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
hb : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h :
  ∀ (f : (x : X) → ι x),
    (∀ (x : X), p x (f x)) →
      ∃ β t, (∀ (b : β), IsOpen[inst✝] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ x, t b ⊆ s x (f x)
α : 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:
have := fun x ↦ (iUnion_eq_univ_iff.1 hu x).imp fun a ha ↦ (hb _).mem_iff.1 ((ho a).mem_nhds ha)
    choose a f hp hsub using this
    rcases h f hp with ⟨β, t, hto, ht, htf, hts⟩
    refine ⟨range t, Subtype.val, forall_subtype_range_iff.2 hto, ?_, htf.on_range,
      forall_subtype_range_iff.2 fun b ↦ ?_⟩
    · rwa [iUnion_subtype, biUnion_range]
    · rcases hts b with ⟨x, hx⟩
      exact ⟨_, hx.trans (hsub _)⟩

Goal state after:
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)
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ a, e ⁻¹' U a = univ
heU : range e ⊆ ⋃ i, U i
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a

Tactic:
rcases precise_refinement_set he.isClosed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩

Goal state after:
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)
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ a, e ⁻¹' U a = univ
heU : range e ⊆ ⋃ i, U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen[inst✝¹] (V i)
heV : range e ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case inl
ι : 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
x : X
hxs : x ∈ s
i : ι
hi : i ∉ chainSupCarrier c
hxi : x ∈ u i
⊢ ∃ i, x ∈ (find c ne i).toFun i

Tactic:
use i

Goal state after:
case h
ι : 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
x : X
hxs : x ∈ s
i : ι
hi : i ∉ chainSupCarrier c
hxi : x ∈ u i
⊢ x ∈ (find c ne i).toFun i
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_3
X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := ⋯
K : CompactExhaustion X := ⋯
Kdiff : ℕ → Set X := ⋯
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := ⋯
x : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)).Finite
⊢ {i | ((fun a ↦ B ((fun a ↦ ↑↑a.snd) a) ((fun a ↦ r a.fst ↑a.snd) a)) i ∩ interior (K (K'.find x + 3))).Nonempty} ⊆
    ⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)

Tactic:
rintro ⟨k, c, hc⟩

Goal state after:
case refine_3
X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := K'.shiftr.shiftr
Kdiff : ℕ → Set X := fun n ↦ K (n + 1) \ interior (K n)
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ ↑(T n)
x : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)).Finite
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
⊢ ⟨k, ⟨c, hc⟩⟩ ∈
      {i | ((fun a ↦ B ((fun a ↦ ↑↑a.snd) a) ((fun a ↦ r a.fst ↑a.snd) a)) i ∩ interior (K (K'.find x + 3))).Nonempty} →
    ⟨k, ⟨c, hc⟩⟩ ∈ ⋃ k, ⋃ (_ : k ≤ K'.find x + 2), range (Sigma.mk k)