mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse v = v

Tactic:
mfderivWithin_range_extChartAt_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 : M
v : TangentSpace I x
⊢ (ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x))).inverse v = v
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)ᶜ
⊢ x ∈ v.toFun i

Tactic:
rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩

Goal state after:
ι : 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
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3
ι : 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
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1

Tactic:
rintro j (rfl | hj)

Goal state after:
case refine_3.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
⊢ closure (update v.toFun j vi j) ⊆ u j

case refine_3.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 : ι
hj : j ∈ v.carrier
⊢ closure (update v.toFun i vi j) ⊆ u j
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: case refine_1
𝕜 : 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
⊢ (fun x ↦ (↑e ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u] f • fun x ↦ (↑e ⟨x, s x⟩).2

Tactic:
apply eventually_of_mem (U := e.baseSet)
    · exact mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)
    · intro x hx
      apply (e.linear 𝕜 hx).2

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_3
ι : 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)
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1

Tactic:
rintro j (rfl | hj)

Goal state after:
case refine_3.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)
⊢ closure (update v.toFun j vi j) ⊆ u j

case refine_3.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 : ι
hj : j ∈ v.carrier
⊢ closure (update v.toFun i vi j) ⊆ u j
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
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedEBall y r ⊆ U i}

Tactic:
mem_preimage,

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
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ ENNReal.ofReal r ∈ ⋂ i, ⋂ (_ : y ∈ K i), {r | closedEBall y r ⊆ U i}
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
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
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
⊢ False

Tactic:
have := f.sum_eq_one hx

Goal state after:
ι : Type uι
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
s : Set M
f : SmoothPartitionOfUnity ι I M s
x : M
hx : x ∈ s
h : ∀ (i : ι), (f i) x ≤ 0
H : ∀ (i : ι), (f i) x = 0
this : ∑ᶠ (i : ι), (f i) x = 1
⊢ False
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 : ι
hi : i ∉ v.carrier
⊢ False

Tactic:
rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩

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 : ι
hi : i ∉ v.carrier
v' : PartialRefinement u s fun w ↦ IsCompact (closure w)
hlt : v < v'
right✝ : IsCompact (closure (v'.toFun i))
⊢ False
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✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
⊢ ∃ x, (s x) a ≠ 0

Tactic:
have a_mem : a ∈ closure d := hd hat

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
⊢ ∃ x, (s x) a ≠ 0
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)
⊢ L x = (↑L' ∘ₗ P ∘ₗ ↑M.symm) x

Tactic:
have : x = M (y, z) := by
      rw [← hyz]; simp only [LinearEquiv.apply_symm_apply]

Goal state after:
𝕜 : 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
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
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < (f c) x
⊢ x ∈ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' ↑(chartAt H c).symm ⁻¹' s

Tactic:
have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)

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)
x : M
hx : x ∈ s
c : M
hc : 0 < (f c) x
Hx : x ∈ tsupport ⇑(f c)
⊢ x ∈ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' ↑(chartAt H c).symm ⁻¹' s
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs),

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SigmaFinite μ
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, f a ∂μ - ∫ (a : α) in s, g a ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, (f - g) x ∂μ = 0

Tactic:
integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs),

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hf : AEFinStronglyMeasurable f μ
hg : AEFinStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (a : α) in s, f a ∂μ - ∫ (a : α) in s, g a ∂μ = 0
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 t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ support f
⊢ x ∈ tᶜ

Tactic:
contrapose xs

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 t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∉ tᶜ
⊢ x ∈ support f
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope

Goal state before:
pp: case inr
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
⊢ c⁻¹ * (c * f (b + c) - ∫ (x : ℝ) in a..a + c, f x) ≤ f (b + c) - f a

Tactic:
← fL

Goal state after:
case inr
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 < c
hf' : IntervalIntegrable f volume a (b + c)
fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c)
fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x
⊢ c⁻¹ * (c * f (b + c) - c * f a) ≤ f (b + c) - f a
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
t : ℕ × (ℕ → ℝ × ℝ)
⊢ ∑ i ∈ Finset.range t.1, dist ((f + g) (t.2 i).1) ((f + g) (t.2 i).2) ≤
    ∑ i ∈ Finset.range t.1, dist (f (t.2 i).1) (f (t.2 i).2) + ∑ i ∈ Finset.range t.1, dist (g (t.2 i).1) (g (t.2 i).2)

Tactic:
· rw [← Finset.sum_add_distrib]
    gcongr
    exact dist_add_add_le _ _ _ _

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 : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
⊢ ‖y - w‖ < δ

Tactic:
rwa [norm_sub_rev]

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

Goal state before:
pp: case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ((iteratedFDerivWithin ℝ (n + 1) f [[x₀, x]] x') fun x ↦ 1) * (x - x₀) ^ (n + 1) / ↑(n + 1)! =
    ((iteratedFDeriv ℝ (n + 1) f x') fun x ↦ 1) * (x - x₀) ^ (n + 1) / ↑(n + 1)!

Tactic:
iteratedFDerivWithin_eq_iteratedFDeriv hu _ ⟨le_of_lt h1.1, le_of_lt h1.2⟩

Goal state after:
case right
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ((iteratedFDeriv ℝ (n + 1) f x') fun x ↦ 1) * (x - x₀) ^ (n + 1) / ↑(n + 1)! =
    ((iteratedFDeriv ℝ (n + 1) f x') fun x ↦ 1) * (x - x₀) ^ (n + 1) / ↑(n + 1)!

f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n + 1) f [[x₀, x]]
hu : UniqueDiffOn ℝ [[x₀, x]]
hd : DifferentiableOn ℝ (iteratedDerivWithin n f [[x₀, x]]) [[x₀, x]]
x' : ℝ
h1 : x' ∈ uIoo x₀ x
h2 :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    iteratedDerivWithin (n + 1) f [[x₀, x]] x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
⊢ ContDiffAt ℝ (↑(n + 1)) f x'