mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 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)
⊢ ∀ (x : ι✝), Tendsto (fun i_1 ↦ Pi.single i (d i_1) x) l (𝓝 (0 x))

Tactic:
]

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)
⊢ ∀ (x : ι✝), Tendsto (fun i_1 ↦ Pi.single i (d i_1) x) l (𝓝 (0 x))
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict t) s < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict t) s < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 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 μ
⊢ f - g =ᵐ[μ] 0

Tactic:
]

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 μ
⊢ f - g =ᵐ[μ] 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 < ∞
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 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 : ι
hn : x i + d n ∈ s i
⊢ ∀ (i_1 : ι✝), (x + Pi.single i (d n)) i_1 ∈ closure[inst✝³ i_1] (s i_1)

Tactic:
]

Goal state after:
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 : ι
hn : x i + d n ∈ s i
⊢ ∀ (i_1 : ι✝), (x + Pi.single i (d n)) i_1 ∈ closure[inst✝³ i_1] (s i_1)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.restrict t).trim hm)
⊢ SigmaFinite ((μ.restrict t).trim hm)

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.restrict t).trim hm)
⊢ SigmaFinite ((μ.restrict t).trim hm)
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:
]

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 ∉ support f
⊢ x ∈ tᶜ
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → f x = 0 x

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → f x = 0 x
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 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)
⊢ ∀ (x : ι✝), Tendsto (fun i_1 ↦ (c i_1 • Pi.single i (d i_1)) x) l (𝓝 (Pi.single i y x))

Tactic:
]

Goal state after:
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)
⊢ ∀ (x : ι✝), Tendsto (fun i_1 ↦ (c i_1 • Pi.single i (d i_1)) x) l (𝓝 (Pi.single i y x))
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : DivisionSemiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : (𝓝[≠] 0).NeBot
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi (I.piecewise s fun x ↦ univ)) x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁷ : DivisionSemiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : (𝓝[≠] 0).NeBot
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : ∀ (i : ι), ContinuousAdd (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi (I.piecewise s fun x ↦ univ)) x
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : ((μ.restrict t).trim hm) s < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 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 : ℝ≥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 := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
t_pos : 0 < t
x : E
hx : x ∈ K
⊢ ↑C * ‖v‖ * ‖g x‖ = ↑C * ‖v‖ * ‖g x‖

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α) in s ∩ t, f x ∂μ = 0

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : μ (s ∩ t) < ∞
⊢ ∫ (x : α) in s ∩ t, 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 : ℝ≥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 := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
t_pos : 0 < t
x : E
hx : x ∉ K
⊢ x ∉ Function.support f

Tactic:
]

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 := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
t : ℝ
ht : t ∈ Ioc 0 1
t_pos : 0 < t
x : E
hx : x ∉ K
⊢ x ∉ Function.support f
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 : β) in Set.univ, f x ∂μ = 0

Tactic:
]

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