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

Goal state before:
pp: case inr
𝕜 : 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 ≠ ∞
this : ∀ {s : Set M}, x ∈ s → (ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u)
hxs : x ∉ s
⊢ ContMDiffWithinAt I I' n f (insert x s) x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u

Tactic:
this (mem_insert _ _),

Goal state after:
case inr
𝕜 : 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 ≠ ∞
this : ∀ {s : Set M}, x ∈ s → (ContMDiffWithinAt I I' n f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u)
hxs : x ∉ s
⊢ (∃ u ∈ 𝓝[insert x (insert x s)] x, ContMDiffOn I I' n f u) ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' n f u
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
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
this✝ : IsManifold I ∞ M
this : IsManifold I' ∞ M'
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)

Tactic:
rcases (contMDiffWithinAt_iff_contMDiffOn_nhds (by simp [h'])).1 h with ⟨t, ht, h't⟩

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
m n : ℕ∞ω
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
h : ContMDiffWithinAt I I' n f s x
hm : ∞ ≤ n
h' : ∞ = ∞ → n = ω
this✝ : IsManifold I ∞ M
this : IsManifold I' ∞ M'
t : Set M
ht : t ∈ 𝓝[insert x s] x
h't : ContMDiffOn I I' n f t
⊢ ∃ u, IsOpen[inst✝⁸] u ∧ x ∈ u ∧ ContMDiffOn I I' ∞ f (insert x s ∩ u)
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
⊢ mfderiv[univ] f x = mfderiv% f x

Tactic:
simp only [mfderivWithin, mfderiv, mfld_simps]

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
⊢ (if MDiffAt[univ] f x then
      fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I)
        (↑I (↑(chartAt H x) x))
    else 0) =
    if MDiffAt f x then
      fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I)
        (↑I (↑(chartAt H x) x))
    else 0
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 f₁ : M → M'
x : M
hL : f₁ =ᶠ[𝓝 x] f
A : f₁ x = f x
⊢ mfderiv[univ] f₁ x = mfderiv[univ] f x

Tactic:
← nhdsWithin_univ

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 f₁ : M → M'
x : M
hL : f₁ =ᶠ[𝓝[univ] x] f
A : f₁ x = f x
⊢ mfderiv[univ] f₁ x = mfderiv[univ] f 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
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 : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt% f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt% g p.2 dg
⊢ HasMFDerivAt% (Prod.map f g) p ((mfderiv% f p.1).prodMap (mfderiv% g p.2))

Tactic:
simp_rw [← hasMFDerivWithinAt_univ, ← mfderivWithin_univ, ← univ_prod_univ]

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 : Type u_11
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_12
inst✝⁷ : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_13
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace G N
F' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
p : M × M'
f : M → N
g : M' → N'
df : TangentSpace I p.1 →L[𝕜] TangentSpace J (f p.1)
hf : HasMFDerivAt% f p.1 df
dg : TangentSpace I' p.2 →L[𝕜] TangentSpace J' (g p.2)
hg : HasMFDerivAt% g p.2 dg
⊢ HasMFDerivAt[univ ×ˢ univ] (Prod.map f g) p ((mfderiv[univ] f p.1).prodMap (mfderiv[univ] g p.2))
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 ∈ (tangentBundleCore I M).baseSet (achart H x)

Tactic:
rw [tangentBundleCore_baseSet, coe_achart, ← 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.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
v : TangentSpace I x
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))).inverse v = v

Tactic:
ContinuousLinearMap.inverse_id

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
v : TangentSpace I x
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))) v = v
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
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivAt% (f i) z (f' i)
⊢ HasMFDerivAt% (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)

Tactic:
simp_all only [← hasMFDerivWithinAt_univ]
  exact HasMFDerivWithinAt.prod hf

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

Goal state before:
pp: case refine_1
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
a : X → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst✝] (t b)
ht : ⋃ b, t b = univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ x, t b ⊆ s x (f x)
⊢ ⋃ b, ↑b = univ

Tactic:
rwa [iUnion_subtype, biUnion_range]

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
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι), i_1 ≠ i → x ∈ (v.toFun i_1)ᶜ
j : ι
hj : x ∈ v.toFun j
⊢ x ∈ v.toFun i

Tactic:
exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1.inl
ι : 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
vi : Set X
ovi : IsOpen vi
j : ι
hi : j ∉ v.carrier
I : s ∩ ⋂ j_1, ⋂ (_ : j_1 ≠ j), (v.toFun j_1)ᶜ ⊆ v.toFun j
C : IsClosed (s ∩ ⋂ j_1, ⋂ (_ : j_1 ≠ j), (v.toFun j_1)ᶜ)
hvi : s ∩ ⋂ j_1, ⋂ (_ : j_1 ≠ j), (v.toFun j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun j
⊢ IsOpen (update v.toFun j vi j)

Tactic:
simp [*, v.isOpen]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1.inr
ι : 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 : ι
hne : j ≠ i
⊢ IsOpen (update v.toFun i vi j)

Tactic:
simp [*, v.isOpen]

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
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module ℝ M
φ : ι → X → M
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ • φ i x₀ = ∑ᶠ (i : ι), (ρ i) x₀ • φ i x₀

Tactic:
apply (finsum_eq_sum_of_support_subset _ _).symm
  have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
    funext fun _ => (Pi.smul_apply' _ _ _).symm
  rw [ρ.coe_finsupport x₀, this, support_smul]
  exact inter_subset_left

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1.inl
ι : 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
vi : Set X
j : ι
hi : j ∉ v.carrier
si : Set X := s ∩ (⋃ j_1, ⋃ (_ : j_1 ≠ j), v.toFun j_1)ᶜ
hsi : si = s ∩ ⋂ i, ⋂ (_ : ¬i = j), (v.toFun i)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun j
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun j ∧ IsCompact (closure vi)
⊢ IsOpen (update v.toFun j vi j)

Tactic:
simp [*, v.isOpen]

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1.inr
ι : 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 : ι
hne : j ≠ i
⊢ IsOpen (update v.toFun i vi j)

Tactic:
simp [*, v.isOpen]

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i ↦ 1 - (f i) x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)

Tactic:
let : LinearOrder ι := linearOrderOfSTO WellOrderingRel

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
B : (mulSupport fun i ↦ 1 - (f i) x) ⊆ ↑s
this : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
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
⊢ f =ᵐ[μ] 0

Tactic:
by
  let s := denseSeq E
  have hs : DenseRange s := denseRange_denseSeq E
  have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, ⟪s n, f x⟫_𝕜 = 0 := ae_all_iff.mpr fun n => hf (s n)
  refine hf'.mono fun x hx => ?_
  rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]
  have h_closed : IsClosed {c : E | ⟪c, f x⟫_𝕜 = 0} :=
    isClosed_eq (by fun_prop) (by fun_prop)
  exact @isClosed_property ℕ E _ s (fun c => ⟪c, f x⟫_𝕜 = 0) hs h_closed hx _

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
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
have h''g : ∀ c x, 0 ≤ f c x * g c (chartAt H c x) :=
    fun c x ↦ mul_nonneg (f.nonneg c x) (h'g c _)

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case pos
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
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ tsupport ⇑(f c)
⊢ g c (↑(chartAt H c) x) = 0

Tactic:
rw [← notMem_support, g_supp, ← mem_preimage, preimage_inter]

Goal state after:
case pos
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
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∈ tsupport ⇑(f c)
⊢ x ∉ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' ↑(chartAt H c).symm ⁻¹' s
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommGroup (E i)
inst✝³ : (i : ι) → Module 𝕜 (E i)
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure[inst✝² i] (s i)
⊢ closure[Pi.topologicalSpace] (univ.pi fun i ↦ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i)))) ⊆
    closure[Pi.topologicalSpace] ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))

Tactic:
simp only [closure_pi_set, ← Submodule.closure_coe_iSup_map_single, Submodule.map_span]

Goal state after:
𝕜 : Type u_1
inst✝⁵ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommGroup (E i)
inst✝³ : (i : ι) → Module 𝕜 (E i)
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ (i : ι), Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (s i) (x i))) ∧ x i ∈ closure[inst✝² i] (s i)
⊢ closure[Pi.topologicalSpace] ↑(⨆ i, Submodule.span 𝕜 (⇑(LinearMap.single 𝕜 E i) '' tangentConeAt 𝕜 (s i) (x i))) ⊆
    closure[Pi.topologicalSpace] ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (univ.pi s) x))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval f b a

Tactic:
simp_all [AbsolutelyContinuousOnInterval, disjWithin_comm]

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
⊢ ∃ q ⊆ s, q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ

Tactic:
have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
      apply hs.trans (fun z hz ↦ ?_)
      obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
      exact mem_biUnion ys hy
    exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this

Goal state after: