mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent

Goal state before:
pp: case hg
𝕜 : 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'
this : IsManifold I (0 + 1) M
i j k : ↑(atlas H M)
x : M
hxk : x ∈ (↑k).source
hxi : x ∈ (↑i).source
hxj : x ∈ (↑j).source
v : E
⊢ DifferentiableWithinAt 𝕜 (↑((↑k).extend I) ∘ ↑((↑j).extend I).symm) (range ↑I) (↑((↑j).extend I) x)

Tactic:
exact (I.contDiffWithinAt_extendCoordChange' (subset_maximalAtlas j.2)
        (subset_maximalAtlas k.2) hxj hxk).differentiableWithinAt one_ne_zero

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
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'
x₀ : M
y₀ : M'
⊢ (mfderiv% fun y ↦ (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_
  rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]

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
⊢ mfderiv% ↑(extChartAt I x) y ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) y))

Tactic:
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm

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% ↑(extChartAt I x) y ∘SL mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) 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'
p : M ⊕ M'
⊢ HasMFDerivAt% Sum.swap p (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
by
  refine ⟨by fun_prop, ?_⟩
  apply (hasFDerivWithinAt_id _ (range I)).congr_of_eventuallyEq
  · exact writtenInExtChartAt_sumSwap_eventuallyEq_id
  · simp only [mfld_simps]
    cases p <;> simp

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

Goal state before:
pp: case mp
𝕜 : 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 : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
x : M
hm : m ≤ n
⊢ ContMDiffWithinAt I I' m (f ∘ ⇑h) s x → ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h x)

Tactic:
intro Hfh
    rw [← h.symm_apply_apply x] at Hfh
    simpa only [Function.comp_def, h.apply_symm_apply] using
      Hfh.comp (h x) (h.symm.contMDiffWithinAt.of_le hm) (mapsTo_preimage _ _)

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
⊢ mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y =
    ContinuousLinearMap.id 𝕜 (TangentSpace I y)

Tactic:
have : y = (extChartAt I x).symm (extChartAt I x y) := ((extChartAt I x).left_inv hy).symm

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)
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 : ℕ∞ω
h : ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, (E →L[𝕜] E) × E) n id
⊢ ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n fun p ↦ p.1 • p.2

Tactic:
exact isBoundedBilinearMap_apply.contDiff.contMDiff.comp h

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case pos
ι : 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)
i : ι
ne : c.Nonempty
h : ∃ v ∈ c, i ∈ v.carrier
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c

Tactic:
have := h.choose_spec

Goal state after:
case pos
ι : 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)
i : ι
ne : c.Nonempty
h : ∃ v ∈ c, i ∈ v.carrier
this : h.choose ∈ c ∧ i ∈ h.choose.carrier
⊢ i ∈ h.choose.carrier ↔ i ∈ chainSupCarrier c
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
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
intro i

Goal state after:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
⊢ i ∈ v.carrier
Module: Mathlib.Topology.MetricSpace.PartitionOfUnity

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i

Tactic:
intro i

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
⊢ x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedEBall p.2 p.1 ⊆ U i
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case h.refine_2
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst✝²] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
⊢ ∀ (i : Fin n) (x : X), (f i) x ∈ Icc 0 1

Tactic:
intro i

Goal state after:
case h.refine_2
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen[inst✝²] (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
i : Fin n
⊢ ∀ (x : X), (f i) x ∈ Icc 0 1
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝¹ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this✝ :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∀ (i : ι), IsCompact (closure (v.toFun i))

Tactic:
intro i

Goal state after:
case refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝¹ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this✝ :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
this : ∀ (i : ι), i ∈ v.carrier
i : ι
⊢ IsCompact (closure (v.toFun i))
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
intro i

Goal state after:
case refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
i : ι
⊢ i ∈ v.carrier
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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
i x : M
hx : x ∈ {x | (ρ i) x • s_loc i x ≠ 0}
⊢ x ∈ {x | (ρ i) x ≠ 0}

Tactic:
mem_ofPred_eq

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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
i x : M
hx : (ρ i) x • s_loc i x ≠ 0
⊢ (ρ i) x ≠ 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:

Tactic:
b * μ.real s < 0 := mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne
    _ ≤ ∫ x in s, f x ∂μ := by
      rw [← μ.restrict_toMeasurable mus.ne]
      exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])

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
⊢ ∀ (c : M),
    ∃ g, support g = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) g ∧ range g ⊆ Icc 0 1

Tactic:
intro 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
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
i : M
⊢ ∃ g, support g = (chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s ∧ ContMDiff I 𝓘(ℝ, ℝ) (↑n) g ∧ range g ⊆ Icc 0 1
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝¹ : FiniteDimensional 𝕜 E
this✝ : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I
L'_cont : Continuous ⇑L'
x : E
y : ↥S
z : ↥T
hyz : M.symm x = (y, z)
this : x = M (y, z)
⊢ L x = (↑L' ∘ₗ P ∘ₗ ↑M.symm) x

Tactic:
simp [L', P, M, this]

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

Goal state before:
pp: case iUnion
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
β : Type u_3
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst✝²] s → ∫ (x : β) in s, f x ∂μ = 0
A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0 → ∫ (x : β) in tᶜ, f x ∂μ = 0
s : Set β
g : ℕ → Set β
g_disj : Pairwise (Function.onFun Disjoint g)
g_meas : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), ∫ (x : β) in g i, f x ∂μ = 0
⊢ ∫ (x : β) in ⋃ i, g i, f x ∂μ = 0

Tactic:
| iUnion g g_disj g_meas hg =>

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
⊢ ∫ (x : E), f (x + t • v) * g x ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ

Tactic:
rw [← integral_add_right_eq_self _ (t • (-v))]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C D : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : LipschitzWith D g
h'g : HasCompactSupport g
v : E
A :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
B :
  Tendsto (fun t ↦ ∫ (x : E), t⁻¹ • (g (x + t • -v) - g x) * f x ∂μ) (𝓝[>] 0)
    (𝓝 (∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ))
t : ℝ
⊢ ∫ (x : E), f (x + t • -v + t • v) * g (x + t • -v) ∂μ = ∫ (x : E), f x * g (x + t • -v) ∂μ
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
⊢ ∀ i ∈ s, Integrable (fun x ↦ a i * ((fderiv ℝ g x) (v i) * f x)) μ

Tactic:
intro i

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
i : ι
⊢ i ∈ s → Integrable (fun x ↦ a i * ((fderiv ℝ g x) (v i) * f x)) μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ≤ x
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y

Tactic:
suffices -((y - x)⁻¹ • ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ • ∫ (t : ℝ) in Icc y x, f t by
      simpa [slope, average, intervalIntegral.integral_interval_sub_left, hg,
        intervalIntegral.integral_of_ge, hy, h]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ≤ x
⊢ -((y - x)⁻¹ • ∫ (t : ℝ) in Icc y x, f t) = (x - y)⁻¹ • ∫ (t : ℝ) in Icc y x, f t
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
⊢ (comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {p | dist p.1 p.2 < ε}

Tactic:
convert! hasBasis_totalLengthFilter.comap _

Goal state after:
case e'_5
X : Type u_1
inst✝ : PseudoMetricSpace X
x✝ : ℝ
⊢ {p | dist p.1 p.2 < x✝} = (fun x ↦ (1, fun x_1 ↦ x)) ⁻¹' {E | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < x✝}
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
⊢ ∀ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2

Tactic:
intro i

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
ε : ℝ
hε : ε > 0
x✝ : ℕ × (ℕ → ℝ × ℝ)
n : ℕ
I : ℕ → ℝ × ℝ
hnI₁ : (n, I) ∈ disjWithin a b
hnI₂ : ∑ i ∈ Finset.range (n, I).1, dist ((n, I).2 i).1 ((n, I).2 i).2 < ε / (↑K + 1)
i : ℕ
⊢ i ∈ Finset.range (n, I).1 → dist (f ((n, I).2 i).1) (f ((n, I).2 i).2) ≤ ↑K * dist (I i).1 (I i).2