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

Tactic:
(extChartAt I x).left_inv (by simpa using hy)

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) ↔
    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.BumpFunction

Goal state before:
pp: case refine_2
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
⊢ ∀ (i' : SmoothBumpFunction I c),
    True → closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I c) c

Tactic:
· exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos)
      self_mem_nhdsWithin

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

Goal state before:
pp: X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst✝²] (s a)
hu : ⋃ a, s a = univ
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
simp only [← hU] at hu ⊢

Goal state after:
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : IsClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen[inst✝²] (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen[inst✝¹] (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ a, e ⁻¹' U a = univ
⊢ ∃ β t, (∀ (b : β), IsOpen[inst✝²] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
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
s : (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₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, (-s) x⟩).2) u x₀

Tactic:
refine hs.neg.congr_of_eventuallyEq ?_ ?_

Goal state after:
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
s : (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₀
⊢ (fun x ↦ (↑e ⟨x, (-s) x⟩).2) =ᶠ[nhdsWithin x₀ u] fun x ↦ -(↑e ⟨x, s x⟩).2

case refine_2
𝕜 : 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 : (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₀
⊢ (↑e ⟨x₀, (-s) x₀⟩).2 = -(↑e ⟨x₀, s x₀⟩).2
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_6
ι : 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
⊢ (fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i) v
    { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯, closure_subset := ⋯,
      pred_of_mem := ⋯, apply_eq := ⋯ }

pp: case refine_7
ι : 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
⊢ ¬(fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i)
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
        closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }
      v

Tactic:
· refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm

Goal state after:
case refine_7
ι : 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
⊢ ¬(fun v₁ v₂ ↦ v₁.carrier ⊆ v₂.carrier ∧ ∀ i ∈ v₁.carrier, v₁.toFun i = v₂.toFun i)
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
        closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }
      v
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
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, t i x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀

Tactic:
simp_rw [← contMDiffWithinAt_univ] at ht' ⊢
  exact .sum_section_of_locallyFinite ht ht'

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝²] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
by
  -- need to switch 0 and 1 in `exists_continuous_zero_one_of_isCompact`
  simpa using
    exists_isSubordinate_of_locallyFinite_of_prop_t2space (fun _ => True)
      (fun _ _ ht hs hd =>
        (exists_continuous_zero_one_of_isCompact' hs ht hd.symm).imp fun _ hf => ⟨trivial, hf⟩)
      hs U ho hf hU

Goal state after:
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))

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
    exact v.pred_of_mem (this 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.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: case inl
𝕜 : 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
hE : Subsingleton E
⊢ ProperSpace F

Tactic:
have : Subsingleton F := Function.Surjective.subsingleton h

Goal state after:
case inl
𝕜 : 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
hE : Subsingleton E
this : Subsingleton F
⊢ ProperSpace F
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: case hf
𝕜 : 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'
A : L = ↑L' ∘ₗ P ∘ₗ ↑M.symm
⊢ Measurable ⇑P

Tactic:
exact P_cont.measurable

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

Goal state before:
pp: case refine_2
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)
⊢ ContMDiff I 𝓘(ℝ, ℝ) ↑n fun x ↦ ∑ᶠ (c : M), (f c) x * g c (↑(chartAt H c) x)

Tactic:
apply SmoothPartitionOfUnity.contMDiff_finsum_smul

Goal state after:
case refine_2
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)
⊢ ∀ (i x : M), x ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, ℝ) (↑n) (fun x ↦ g i (↑(chartAt H i) x)) x
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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Pi.single i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (univ.pi s)) x

Tactic:
apply mem_tangentConeAt_of_seq l c (fun n ↦ Pi.single i (d n))

Goal state after:
case hd₀
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ Pi.single i (d n)) l (𝓝 0)

case hds
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : ι) in l, x + Pi.single i (d n) ∈ closure[Pi.topologicalSpace] (univ.pi s)

case hcd
𝕜 : 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
inst✝ : DecidableEq ι✝
i : ι✝
hi : ∀ (j : ι✝), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
ι : Type (max u_1 u_3)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E i
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x i + d n ∈ s i
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ c n • Pi.single i (d n)) l (𝓝 (Pi.single i y))
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 g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (fun i ↦ f (i + t • v) - f i) μ

Tactic:
apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v : E
t : ℝ
⊢ AEStronglyMeasurable (fun i ↦ f (i + 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 g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := ⋯
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (fun i ↦ f (i + t • v) - f i) μ

Tactic:
apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := ⋯
K_compact : IsCompact K
t : ℝ
⊢ AEStronglyMeasurable (fun i ↦ f (i + t • v)) μ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: 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
t : Set β
t_meas : MeasurableSet t
ht : ∫ (x : β) in t, f x ∂μ = 0
⊢ ∫ (x : β), f x ∂μ = 0

Tactic:
rw [← setIntegral_univ]

Goal state after:
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
t : Set β
t_meas : MeasurableSet t
ht : ∫ (x : β) in t, f x ∂μ = 0
⊢ ∫ (x : β) in Set.univ, f x ∂μ = 0
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
⊢ ∫ (x : E), lineDeriv ℝ f x v * g x ∂μ = ∫ (x : E), lineDeriv ℝ g x (-v) * f x ∂μ

Tactic:
have A : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ f x v * g x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul
      hf (hg.continuous.integrable_of_hasCompactSupport h'g) v
  have B : Tendsto (fun (t : ℝ) ↦ ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ) (𝓝[>] 0)
              (𝓝 (∫ x, lineDeriv ℝ g x (-v) * f x ∂μ)) :=
    integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' hg h'g hf.continuous (-v)
  suffices S1 : ∀ (t : ℝ), ∫ x, (t⁻¹ • (f (x + t • v) - f x)) * g x ∂μ =
                            ∫ x, (t⁻¹ • (g (x + t • (-v)) - g x)) * f x ∂μ by
    simp only [S1] at A; exact tendsto_nhds_unique A B
  intro t
  suffices S2 : ∫ x, (f (x + t • v) - f x) * g x ∂μ = ∫ x, f x * (g (x + t • (-v)) - g x) ∂μ by
    simp only [smul_eq_mul, mul_assoc, integral_const_mul, S2, mul_comm (f _)]
  have S3 : ∫ x, f (x + t • v) * g x ∂μ = ∫ x, f x * g (x + t • (-v)) ∂μ := by
    rw [← integral_add_right_eq_self _ (t • (-v))]; simp
  simp_rw [_root_.sub_mul, _root_.mul_sub]
  rw [integral_sub, integral_sub, S3]
  · apply Continuous.integrable_of_hasCompactSupport
    · exact hf.continuous.mul (hg.continuous.comp (continuous_add_const _))
    · exact (h'g.comp_homeomorph (Homeomorph.addRight (t • (-v)))).mul_left
  · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left
  · apply Continuous.integrable_of_hasCompactSupport
    · exact (hf.continuous.comp (continuous_add_const _)).mul hg.continuous
    · exact h'g.mul_left
  · exact (hf.continuous.mul hg.continuous).integrable_of_hasCompactSupport h'g.mul_left

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 : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
⊢ ∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)

Tactic:
apply ae_eq_of_integral_contDiff_smul_eq (hf.locallyIntegrable_lineDeriv _)
    (locallyIntegrable_finsetSum _ (fun i hi ↦ (hf.locallyIntegrable_lineDeriv (v i)).smul (a i)))
    (fun g g_smooth g_comp ↦ ?_)

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
⊢ ∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ =
    ∫ (x : E), g x • ∑ i ∈ s, (a i • fun x ↦ lineDeriv ℝ f x (v i)) x ∂μ