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

Goal state before:
pp: case pos.h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
this : (fun f ↦ setToFun μ' T hT' ↑↑f) = fun f ↦ setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ' T hT' ↑↑f

Tactic:
this

Goal state after:
case pos.h_closed
α : 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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
this : (fun f ↦ setToFun μ' T hT' ↑↑f) = fun f ↦ setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f ⋯)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ edist ((thickenedIndicator δ_pos E) x) ((thickenedIndicator δ_pos E) y) ≤ ↑δ.toNNReal⁻¹ * edist x y
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 C' : ℝ
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f μ
h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
[

Goal state after:
case neg
α : 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 C' : ℝ
μ' : Measure α
c c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f μ
h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) ^ (ENNReal.toReal 1)⁻¹ ≤ (2 * μ univ * ↑r).toReal

Tactic:
[

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) ^ (ENNReal.toReal 1)⁻¹ ≤ (2 * μ univ * ↑r).toReal
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ (∫⋯∫⁻_∅, f ∂μ) x = f x

Tactic:
[

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ (∫⋯∫⁻_∅, f ∂μ) x = f x
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X ↑default ≃ᵐ ((i_1 : α) → X ↑i_1) := (MeasurableEquiv.piUnique fun j ↦ X ↑j).symm
x : (i : δ) → X i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (y : X ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default

Tactic:
[

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X ↑default ≃ᵐ ((i_1 : α) → X ↑i_1) := (MeasurableEquiv.piUnique fun j ↦ X ↑j).symm
x : (i : δ) → X i
⊢ (∫⋯∫⁻_{i}, f ∂μ) x = ∫⁻ (y : X ↑default), f (updateFinset x {i} (e y)) ∂μ ↑default
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X ↑i) × ((i : ↥t) → X ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → X ↑i) := MeasurableEquiv.piFinsetUnion X hst
⊢ (∫⁻ (y : (i : ↥s) → X ↑i),
      ∫⁻ (z : (j : ↥t) → X ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j ↦ μ ↑j ∂Measure.pi fun i ↦ μ ↑i) =
    (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Tactic:
[

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X ↑i) × ((i : ↥t) → X ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → X ↑i) := MeasurableEquiv.piFinsetUnion X hst
⊢ (∫⁻ (y : (i : ↥s) → X ↑i),
      ∫⁻ (z : (j : ↥t) → X ↑j),
        f (updateFinset x (s ∪ t) (e (y, z))) ∂Measure.pi fun j ↦ μ ↑j ∂Measure.pi fun i ↦ μ ↑i) =
    (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.univ, f ∂μ) x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ

Tactic:
[

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → X i) → ℝ≥0∞
e : ↥Finset.univ ≃ δ := subtypeUnivEquiv ⋯
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.univ, f ∂μ) x = ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) (update ((fun {x_1} ↦ x) ∘' e) a✝ xᵢ) ∂((fun {x} ↦ μ) ∘' e) a✝

Tactic:
[

Goal state after:
case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) (update x (e a✝) xᵢ) ∂μ (e a✝) =
    ∫⁻ (xᵢ : X (e a✝)), (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) (update ((fun {x_1} ↦ x) ∘' e) a✝ xᵢ) ∂((fun {x} ↦ μ) ∘' e) a✝
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case insert
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → X i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) (update x i' xᵢ) ∂μ i'

Tactic:
[

Goal state after:
case insert
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → X i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) (update x i' xᵢ) ∂μ i'
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
[

Goal state after:
case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
[

Goal state after:
case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ = ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
[

Goal state after:
case inl
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
h : IsEmpty ((i : δ) → X i)
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ

Tactic:
[

Goal state after:
case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ ∫⁻ (x : (i : δ) → X i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → X i), g x ∂Measure.pi μ
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : 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
⊢ ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst✝³] i → ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id i

Tactic:
rintro s ⟨s_mem, s_closed⟩

Goal state after:
α : 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
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : 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))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
⊢ ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst✝³] i → ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id i

Tactic:
rintro s ⟨s_mem, s_closed⟩

Goal state after:
α : 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))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
⊢ ∀ (i : Set β), i ∈ 𝓝 b ∧ IsClosed[inst✝⁴] i → ∀ᶠ (x : α) in atTop, g x ∈ id i

Tactic:
rintro s ⟨s_mem, s_closed⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
⊢ ∀ᶠ (x : α) in atTop, g x ∈ id s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ

Tactic:
[

Goal state after:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ
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
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
    ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ

Tactic:
[

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
    ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ
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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (fun a ↦ ‖∑' (n : ι), ‖f n a‖‖ₑ) =ᵐ[μ] fun a ↦ ∑' (n : ι), ‖f n a‖ₑ

Tactic:
[

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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (fun a ↦ ‖∑' (n : ι), ‖f n a‖‖ₑ) =ᵐ[μ] fun a ↦ ∑' (n : ι), ‖f n a‖ₑ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
⊢ MeasurableSet {x | Integrable (f x) μ}

Tactic:
[

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
⊢ MeasurableSet {x | Integrable (f x) μ}
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, μ (s i) ≠ ∞
⊢ μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * μ.real (⋂ i ∈ u, s i)

Tactic:
[

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, μ (s i) ≠ ∞
⊢ μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * μ.real (⋂ i ∈ u, s i)
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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
x : β
y : E
⊢ y ∈ (s' n x).range → y ∈ (s n).range

Tactic:
[

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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
x : β
y : E
⊢ y ∈ (s' n x).range → y ∈ (s n).range