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

Goal state before:
pp: case compl.refine_2.mp
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
⊢ (∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2) →
    ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1

pp: case compl.refine_2.mpr
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
⊢ (∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1) →
    ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2

Tactic:
<;>

Goal state after:
case compl.refine_2.mp
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
⊢ (∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2) →
    ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1

case compl.refine_2.mpr
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
⊢ (∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1) →
    ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_1.«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ![s, t] ((fun i ↦ i) ⟨0, ⋯⟩) ∈ C

pp: case convert_1.«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ![s, t] ((fun i ↦ i) ⟨1, ⋯⟩) ∈ C

Tactic:
<;>

Goal state after:
case convert_1.«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ![s, t] ((fun i ↦ i) ⟨0, ⋯⟩) ∈ C

case convert_1.«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ![s, t] ((fun i ↦ i) ⟨1, ⋯⟩) ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2.«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case convert_2.«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case convert_2.«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) j

case convert_2.«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
j : Fin (Nat.succ 0).succ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
hP : IsProjectiveMeasureFamily P
s : ℕ → Set ((i : ι) → α i)
hs : ∀ (n : ℕ), s n ∈ measurableCylinders α
n : ℕ
⊢ (projectiveFamilyContent hP) (⋃ i, ⋃ (_ : i ≤ n), s i) = (projectiveFamilyContent hP) (⋃ i ∈ range (n + 1), s i)

Tactic:
simp only [mem_range_succ_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
hP : IsProjectiveMeasureFamily P
s : ℕ → Set ((i : ι) → α i)
hs : ∀ (n : ℕ), s n ∈ measurableCylinders α
n : ℕ
⊢ (projectiveFamilyContent hP) (⋃ i, ⋃ (_ : i ≤ n), s i) = (projectiveFamilyContent hP) (⋃ i ∈ range (n + 1), s i)

Tactic:
by
    simp only [mem_range_succ_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.SimpleGraph

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable fun x ↦ e ∈ Sym2.diagSet

pp: case refine_2
V : Type u_1
inst✝ : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable fun x ↦ e ∉ x

Tactic:
<;>

Goal state after:
case refine_1
V : Type u_1
inst✝ : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable fun x ↦ e ∈ Sym2.diagSet

case refine_2
V : Type u_1
inst✝ : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable fun x ↦ e ∉ x
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case succ.inl
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u : α
huv : u ≤ u
h'uv : ⋃₀ ↑I = Set.Ioc u u
⊢ onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u

pp: case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
⊢ onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u

Tactic:
· have : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0 := by simp [onIocAux_empty f]
        rw [h'uv, this]
        apply Finset.sum_congr rfl fun i hi ↦ ?_
        have : i = ∅ := by grind [sUnion_eq_empty]
        grind [onIocAux_empty]

Goal state after:
case succ.inr
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
n : ℕ
ih :
  ∀ (I : Finset (Set α)),
    ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} →
      (↑I).PairwiseDisjoint id →
        ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} → #I = n → onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
hn : #I = n + 1
u v : α
huv✝ : u ≤ v
h'uv : ⋃₀ ↑I = Set.Ioc u v
huv : u < v
⊢ onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case top
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
⊢ (fun x ↦
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊤)
      ((fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA) ⊤) =
    ⊤

pp: case coe
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
a✝ : ι
⊢ (fun x ↦
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊤)
      ((fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA) ↑a✝) =
    ↑a✝

Tactic:
<;>

Goal state after:
case top
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
⊢ (fun x ↦
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊤)
      ((fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA) ⊤) =
    ⊤

case coe
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
a✝ : ι
⊢ (fun x ↦
        match x with
        | Sum.inl i => ↑i
        | Sum.inr PUnit.unit => ⊤)
      ((fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA) ↑a✝) =
    ↑a✝
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
val✝ : ι
⊢ (fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA)
      ((fun x ↦
          match x with
          | Sum.inl i => ↑i
          | Sum.inr PUnit.unit => ⊤)
        (Sum.inl val✝)) =
    Sum.inl val✝

pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
val✝ : Unit
⊢ (fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA)
      ((fun x ↦
          match x with
          | Sum.inl i => ↑i
          | Sum.inr PUnit.unit => ⊤)
        (Sum.inr val✝)) =
    Sum.inr val✝

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
val✝ : ι
⊢ (fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA)
      ((fun x ↦
          match x with
          | Sum.inl i => ↑i
          | Sum.inr PUnit.unit => ⊤)
        (Sum.inl val✝)) =
    Sum.inl val✝

case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
val✝ : Unit
⊢ (fun x ↦ if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA)
      ((fun x ↦
          match x with
          | Sum.inl i => ↑i
          | Sum.inr PUnit.unit => ⊤)
        (Sum.inr val✝)) =
    Sum.inr val✝
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
I : Finset (Set α)
h_ss : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
h_mem : ⋃₀ ↑I ∈ C
⊢ ⋃₀ ↑I ∈ C

Tactic:
exact h_mem

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case pos
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f✝ : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∈ s
⊢ (B (s.indicator (Function.const Ω c) ω)) (f ω) = s.indicator (fun ω ↦ (B c) (f ω)) ω

pp: case neg
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f✝ : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∉ s
⊢ (B (s.indicator (Function.const Ω c) ω)) (f ω) = s.indicator (fun ω ↦ (B c) (f ω)) ω

Tactic:
<;>

Goal state after:
case pos
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f✝ : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∈ s
⊢ (B (s.indicator (Function.const Ω c) ω)) (f ω) = s.indicator (fun ω ↦ (B c) (f ω)) ω

case neg
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f✝ : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∉ s
⊢ (B (s.indicator (Function.const Ω c) ω)) (f ω) = s.indicator (fun ω ↦ (B c) (f ω)) ω
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ.restrict E) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ_pos, hδε⟩ := hf hε
  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
  rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs
  calc
    eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
    _ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
      eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
    _ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
      (eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case e'_3
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0

pp: case e'_4
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0

case e'_4
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
ι : Type u_4
x : ι
B : Set ι
A : Set α
inst✝ : Decidable (x ∈ B)
h : x ∈ B
⊢ v A = B.indicator (fun x ↦ v A) x

pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
ι : Type u_4
x : ι
B : Set ι
A : Set α
inst✝ : Decidable (x ∈ B)
h : x ∉ B
⊢ v ∅ = B.indicator (fun x ↦ v A) x

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
ι : Type u_4
x : ι
B : Set ι
A : Set α
inst✝ : Decidable (x ∈ B)
h : x ∈ B
⊢ v A = B.indicator (fun x ↦ v A) x

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
ι : Type u_4
x : ι
B : Set ι
A : Set α
inst✝ : Decidable (x ∈ B)
h : x ∉ B
⊢ v ∅ = B.indicator (fun x ↦ v A) x
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : IsEmpty α
μ : VectorMeasure α M
s : Set α
⊢ μ s = 0

Tactic:
by
  simp [eq_empty_of_isEmpty s]

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

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ → re c ≪ᵥ μ ∧ im c ≪ᵥ μ

pp: case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ re c ≪ᵥ μ ∧ im c ≪ᵥ μ → c ≪ᵥ μ

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ c ≪ᵥ μ → re c ≪ᵥ μ ∧ im c ≪ᵥ μ

case mpr
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ re c ≪ᵥ μ ∧ im c ≪ᵥ μ → c ≪ᵥ μ
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: case mp.left
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ

pp: case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ im c ≪ᵥ μ

Tactic:
<;>

Goal state after:
case mp.left
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ re c ≪ᵥ μ

case mp.right
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : VectorMeasure α ℝ≥0∞
h : c ≪ᵥ μ
⊢ im c ≪ᵥ μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i

pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ i

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ s.restrictNonposSeq i 0 ⊆ i

case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ s.restrictNonposSeq i (n✝ + 1) ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
s : Set α
x : α
m : M
hs : MeasurableSet s
inst✝ : Decidable (x ∈ s)
t : Set α
ht : MeasurableSet t
has : x ∈ s
⊢ (dirac x m) (t ∩ s) = (dirac x m) t

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
s : Set α
x : α
m : M
hs : MeasurableSet s
inst✝ : Decidable (x ∈ s)
t : Set α
ht : MeasurableSet t
has : x ∉ s
⊢ (dirac x m) (t ∩ s) = 0 t

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
s : Set α
x : α
m : M
hs : MeasurableSet s
inst✝ : Decidable (x ∈ s)
t : Set α
ht : MeasurableSet t
has : x ∈ s
⊢ (dirac x m) (t ∩ s) = (dirac x m) t

case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
s : Set α
x : α
m : M
hs : MeasurableSet s
inst✝ : Decidable (x ∈ s)
t : Set α
ht : MeasurableSet t
has : x ∉ s
⊢ (dirac x m) (t ∩ s) = 0 t
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)

pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.restrictNonposSeq i 0)

case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (s.restrictNonposSeq i (n✝ + 1))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (v.restrict {a}) s = (dirac a (v {a})) s

pp: case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (v.restrict {a}) s = (dirac a (v {a})) s

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
s : Set α
hs : MeasurableSet s
ha : a ∈ s
⊢ (v.restrict {a}) s = (dirac a (v {a})) s

case neg
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
a : α
h : MeasurableSet {a}
s : Set α
hs : MeasurableSet s
ha : a ∉ s
⊢ (v.restrict {a}) s = (dirac a (v {a})) s
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ v j ≤ w j

Tactic:
rw [v.not_measurable hj₁, w.not_measurable hj₁]

Goal state after: