mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Constructions

Goal state before:
pp: B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁶ : TopologicalSpace B'
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace B
inst✝² : ∀ (_b : B), Nonempty (E _b)
K : Type U
inst✝¹ : FunLike K B' B
inst✝ : ContinuousMapClass K B' B
e : Trivialization F TotalSpace.proj
f : K
y : B' × F
h : f y.1 ∈ e.baseSet ∧ y.2 ∈ univ
⊢ TotalSpace.mk' F y.1 (e.symm (f y.1) y.2) ∈ Pullback.lift ⇑f ⁻¹' e.source

Tactic:
simp_rw [e.source_eq, mem_preimage, Pullback.lift_proj, h.1]

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'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivAt[s] f x f'
hxs : UniqueMDiffAt[s] x
⊢ mfderiv[s] f x = f'

Tactic:
ext
  rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]

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
p : TangentBundle I M
hs : UniqueMDiffAt[s] p.proj
h : MDiffAt f p.proj
⊢ tangentMapWithin I I' f s p = tangentMap I I' f p

Tactic:
by
  rw [← mdifferentiableWithinAt_univ] at h
  rw [← tangentMapWithin_univ]
  exact tangentMapWithin_subset (subset_univ _) hs h

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

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
s : Set M
x : M
hxs : UniqueMDiffAt[s] x
⊢ mfderiv[s] id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
MDifferentiable.mfderivWithin mdifferentiableAt_id hxs

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
s : Set M
x : M
hxs : UniqueMDiffAt[s] x
⊢ mfderiv% id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
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
x₀ : M
⊢ ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔
    ContMDiffAt IM IB n (fun x ↦ (f x).proj) x₀ ∧
      ContMDiffAt IM 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Tactic:
simp_rw [← contMDiffWithinAt_univ]

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
x₀ : M
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f univ x₀ ↔
    ContMDiffWithinAt IM IB n (fun x ↦ (f x).proj) univ x₀ ∧
      ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) univ x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case h₁
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
inst✝³ : TopologicalSpace B
inst✝² : ChartedSpace HB B
inst✝¹ : FiberBundle F E
s : (x : B) → E x
u : Set B
x : B
inst✝ : Subsingleton F
⊢ ∀ y ∈ u, (↑(trivializationAt F E x) { proj := y, snd := s y }).2 = ?m.113

Tactic:
intro y

Goal state after:
case h₁
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
inst✝³ : TopologicalSpace B
inst✝² : ChartedSpace HB B
inst✝¹ : FiberBundle F E
s : (x : B) → E x
u : Set B
x : B
inst✝ : Subsingleton F
y : B
⊢ y ∈ u → (↑(trivializationAt F E x) { proj := y, snd := s y }).2 = ?m.113
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
⊢ MDiff[(extChartAt I x).target] ↑(extChartAt I x).symm

Tactic:
intro y

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
y : E
⊢ y ∈ (extChartAt I x).target → MDiffAt[(extChartAt I x).target] ↑(extChartAt I x).symm y
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
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
s : (x : B) → E x
x₀ : B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x₀ ↔
    ContMDiffAt IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) x₀

Tactic:
simp_rw [← contMDiffWithinAt_univ]

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
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
s : (x : B) → E x
x₀ : B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) univ x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) univ x₀
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ EqOn (writtenInExtChartAt I I (Sum.inl x) Sum.swap) id t

Tactic:
intro y

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
⊢ y ∈ t → writtenInExtChartAt I I (Sum.inl x) Sum.swap y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ EqOn (writtenInExtChartAt I I (Sum.inr x) Sum.swap) id t

Tactic:
intro y

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
⊢ y ∈ t → writtenInExtChartAt I I (Sum.inr x) Sum.swap y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
⊢ writtenInExtChartAt I I q' Sum.inr =ᶠ[𝓝[range ↑I] ↑(extChartAt I q') q'] id

Tactic:
by
  have hmem : I.symm ⁻¹'
      (chartAt H q').target ∩ Set.range I ∈ 𝓝[Set.range I] (extChartAt I q' q') := by
    rw [← I.image_eq (chartAt H q').target]
    exact (chartAt H q').extend_image_target_mem_nhds (mem_chart_source H q')
  filter_upwards [hmem] with y hy
  rcases hy with ⟨hyT, ⟨z, rfl⟩⟩
  simp [writtenInExtChartAt, extChartAt, ChartedSpace.sum_chartAt_inr,
    Sum.inr_injective.extend_apply <| chartAt H q',
    (chartAt H q').right_inv (by simpa [Set.mem_preimage, I.left_inv] using hyT)]

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
s : Set M
hs : s ⊆ support ↑f
⊢ ↑(extChartAt I c) '' s = closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s

Tactic:
by
  rw [support_eq_inter_preimage, subset_inter_iff, ← extChartAt_source I, ← image_subset_iff] at hs
  obtain ⟨hse, hsf⟩ := hs
  apply Subset.antisymm
  · refine subset_inter (subset_inter (hsf.trans ball_subset_closedBall) ?_) ?_
    · rintro _ ⟨x, -, rfl⟩; exact mem_range_self _
    · rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
      exact inter_subset_right
  · refine Subset.trans (inter_subset_inter_left _ f.closedBall_subset) ?_
    rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_2
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)
⊢ s ⊆ ⋃ a, B ((fun a ↦ ↑↑a.snd) a) ((fun a ↦ r a.fst ↑a.snd) a)

Tactic:
refine fun x hx ↦ mem_iUnion.2 ?_

Goal state after:
case refine_2
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
hx : x ∈ s
⊢ ∃ i, x ∈ B ((fun a ↦ ↑↑a.snd) i) ((fun a ↦ r a.fst ↑a.snd) i)
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: case refine_1.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
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, t x⟩).2) u x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun x ↦ (↑e ⟨x, (s + t) x⟩).2) x = ((fun x ↦ (↑e ⟨x, s x⟩).2) + fun x ↦ (↑e ⟨x, t x⟩).2) x

Tactic:
apply (e.linear 𝕜 hx).1

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : R1Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed[inst✝³] s
H : ∀ x ∈ s, ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v

Tactic:
choose u v hu hv hxu htv huv using SetCoe.forall'.1 H

Goal state after:
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : R1Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed[inst✝³] s
H : ∀ x ∈ s, ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen[inst✝³] (u x)
hv : ∀ (x : ↑s), IsOpen[inst✝³] (v x)
hxu : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
⊢ ∃ n, eball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)

Tactic:
rcases EMetric.isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
      have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
      rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
      refine ⟨n, Subset.trans (eball_subset_eball ?_) hε⟩
      simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ (x : X),
    {i | x ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))} →
      ρ.fintsupport x ⊆ ρ.fintsupport x₀

Tactic:
intro y

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
⊢ {i | y ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))} →
    ρ.fintsupport y ⊆ ρ.fintsupport x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

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
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
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u
⊢ ∀ y ∈ (tsupport ψ)ᶜ, ⟨y, (ψ • s) y⟩ = zeroSection F V y

Tactic:
intro y

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
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
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u
y : M
⊢ y ∈ (tsupport ψ)ᶜ → ⟨y, (ψ • s) y⟩ = zeroSection F V y
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∃ I, (∀ᶠ (x : X) in 𝓝[s] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 ↦ (ρ x_1) x) ⊆ ↑I

Tactic:
rcases ρ.locallyFinite.exists_finset_support x₀ with ⟨I, hI⟩
  refine ⟨I, eventually_nhdsWithin_iff.mpr (hI.mono fun x hx x_in ↦ ?_), hI⟩
  have : ∑ᶠ i : ι, ρ i x = ∑ i ∈ I, ρ i x := finsum_eq_sum_of_support_subset _ hx
  rwa [eq_comm, ρ.sum_eq_one x_in] at this

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

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
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₀
⊢ ⟨x₀, ∑' (i : ι), t i x₀⟩ = ⟨x₀, ∑ i ∈ s.toFinset, t i x₀⟩

Tactic:
rw [TotalSpace.mk_inj, tsum_eq_sum']
    refine support_subset_iff'.mpr fun i hi ↦ ?_
    by_contra! h
    have : i ∈ s.toFinset := by
      refine Set.mem_toFinset.mpr ?_
      simp only [s, ne_eq, Set.mem_ofPred_eq]
      use x₀
      simpa using ⟨h, mem_of_mem_nhds hu'⟩
    exact hi this

Goal state after: