mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
⊢ (setToL1 ⋯) f = (setToL1 hT) f + (setToL1 hT') f

Tactic:
by
  apply setToL1_unique (hT.add hT') (A := setToL1 hT + setToL1 hT') _ f
  simp [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left hT hT']

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rw [h₀, closedBall_zero']

Goal state after:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x} ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case refine_1
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ (↑‖x₀‖)⁻¹ • x₀ ∉ F

Tactic:
Submodule.smul_mem_iff

Goal state after:
case refine_1
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ x₀ ∉ F

case refine_1.s0
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ (↑‖x₀‖)⁻¹ ≠ 0
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
⊢ ∀ y ∈ F, r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖

Tactic:
intro y hy

Goal state after:
case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: m : Type u_4
R : Type u_8
inst✝³ : TopologicalSpace R
α : Type u_11
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Zero R
inst✝ : T2Space R
⊢ IsClosed {M | M.BlockTriangular b}

Tactic:
by
  simp only [BlockTriangular, Set.ofPred_forall]
  refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun _ => ?_
  exact isClosed_eq (continuous_id.matrix_elem i j) continuous_const

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ ∃ ν, ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ (∑ i ∈ s, μ i + Measure.sum fun i ↦ μ ↑i) = Measure.sum μ
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
⊢ ∫ (x : X) in s, f x ∂μ = ∑' (x : ↑s), μ.real {↑x} • f ↑x

Tactic:
by
  have hi : Countable { x // x ∈ s } := Iff.mpr countable_coe_iff hs
  have hf' : Integrable (fun (x : s) ↦ f x) (Measure.comap Subtype.val μ) := by
    rw [IntegrableOn, ← map_comap_subtype_coe, integrable_map_measure] at hf
    · apply hf
    · exact Integrable.aestronglyMeasurable hf
    · exact Measurable.aemeasurable measurable_subtype_coe
    · exact Countable.measurableSet hs
  rw [← integral_subtype_comap hs.measurableSet, integral_countable hf']
  congr 1 with a : 1
  rw [measureReal_def, Measure.comap_apply Subtype.val Subtype.coe_injective
    (fun s' hs' ↦ MeasurableSet.subtype_image (Countable.measurableSet hs) hs') _
    (MeasurableSet.singleton a)]
  simp [measureReal_def]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded ((fun x_1 ↦ x_1 + x) ⁻¹' sᶜ)

Tactic:
convert! isBounded_sub hs (t := { x }) isBounded_singleton using 1

Goal state after:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ (fun x_1 ↦ x_1 + x) ⁻¹' sᶜ = sᶜ - {x}
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

Tactic:
refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ f x ∈ range ⇑f ∪ range ⇑g

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
x : α
⊢ g x ∈ range ⇑f ∪ range ⇑g
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:

Tactic:
ε * μ.real { x | ε ≤ f x } = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
      _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
        integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
          ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
      _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ Integrable f μ

Tactic:
convert h'i.sub this

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ f = fs i - (fs i - f)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) =
    (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)

Tactic:
ENNReal.toReal_ofReal hpq.nonneg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = (∫⁻ (x : α), ‖f x‖ₑ ^ p ∂μ) ^ (1 / p)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
⊢ ∀ y ∈ F, 1 ≤ ‖y - x‖

Tactic:
intro y hy

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖y - x‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ interior K ∪ frontier K

Tactic:
rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
⊢ ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖

Tactic:
intro N

Goal state after:
α : Type u_1
N : ℕ
⊢ ∀ {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist ((mkOfCompact f) x) ((mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (f x) (g x) < C
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p ↦ ↑p.1 - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [show (fun x : α => (1 : ℝ≥0∞) - infEDist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p ↦ ↑p.1 - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
⊢ ∀ (a : ↥(Lp G 1 μ)), dist a f < ε / 2 / c'.toReal → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑f ⋯) < ε

Tactic:
intro g hfg

Goal state after:
case h
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : dist g f < ε / 2 / c'.toReal
⊢ dist (Integrable.toL1 ↑↑g ⋯) (Integrable.toL1 ↑↑f ⋯) < ε
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ (thickenedIndicatorAux δ E x).toNNReal = 0

Tactic:
thickenedIndicatorAux_zero δ_pos E x_out,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ ENNReal.toNNReal 0 = 0
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ Integrable f (μ + μ')

Tactic:
apply hf.add_measure hf'

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
h' : 𝓝[<] a = ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
simp [h']

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : 𝓝[<] a = ⊥
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
simp [h']

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ

Tactic:
eq_sub_iff_add_eq,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ + ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))

Tactic:
obtain ⟨i, is, bcd⟩ : ∃ i ∈ s, b ∈ Iotop (c i) (d i) := by
    simpa only [SetLike.mem_coe, mem_iUnion, exists_prop] using cv ⟨ab, le_rfl⟩

Goal state after:
case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
i : ℕ
is : i ∈ s
bcd : b ∈ Iotop (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in s \ k ∪ t \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ

Tactic:
union_comm

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∫ (x : X) in t \ k ∪ s \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
g : G
x : α
⊢ f.symm (f ((fun x ↦ e (e.symm g) • x) x)) = (fun x ↦ g • x) (f.symm (f x))

Tactic:
f.symm_apply_apply,

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
g : G
x : α
⊢ (fun x ↦ e (e.symm g) • x) x = (fun x ↦ g • x) (f.symm (f x))
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
g : G
x : α
⊢ (fun x ↦ e (e.symm g) • x) x = (fun x ↦ g • x) (f.symm (f x))

Tactic:
f.symm_apply_apply,

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Group H
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
inst✝¹ : MulAction H β
inst✝ : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm) ν μ
e : H ≃ G
hef : ∀ (g : H), Semiconj (⇑f) (fun x ↦ e g • x) fun x ↦ g • x
g : G
x : α
⊢ (fun x ↦ e (e.symm g) • x) x = (fun x ↦ g • x) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
let f' := h.1.mk f

Goal state after:
case pos
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case e'_3.e'_4
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
A : Set α
hA₀ : MeasurableSet A
hA : ∀ (g : G), (fun x ↦ g • x) ⁻¹' A = A
g : G
x : α
⊢ A = (fun x ↦ g • x) ⁻¹' A

Tactic:
rw [hA g]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
⊢ μ { carrier := closure ↑K, isCompact' := ⋯ } ≤ μ.outerMeasure (closure ↑K)

Tactic:
exact μ.le_outerMeasure_compacts _

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ (⋂ i, {x | x ∉ i⁻¹ • fundamentalInterior G s}) = 0

Tactic:
← compl_ofPred,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ (⋂ i, {a | a ∈ i⁻¹ • fundamentalInterior G s}ᶜ) = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ 0 < ∫ (x : X) in {x | R < f x}, f x ∂μ - ∫ (x : X) in {x | R < f x}, R ∂μ

Tactic:
← integral_sub hfint this,

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ 0 < ∫ (a : X) in {x | R < f x}, f a - R ∂μ