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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ∑ u ∈ Finset.image f a, m u = ∑ i ∈ a, m (f i)

pp: case h_ss
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ↑(Finset.image f a) ⊆ C

pp: case h_dis
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ (↑(Finset.image f a)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ⋃₀ ↑(Finset.image f a) ∈ C

Tactic:
rotate_left

Goal state after:
case h_ss
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ↑(Finset.image f a) ⊆ C

case h_dis
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ (↑(Finset.image f a)).PairwiseDisjoint id

case h_mem
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ⋃₀ ↑(Finset.image f a) ∈ C

α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
A : ⋃ i ∈ a, f i = ⋃₀ ↑(Finset.image f a)
⊢ ∑ u ∈ Finset.image f a, m u = ∑ i ∈ a, m (f i)
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl
α : 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
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
have := finite_coe_iff.2 A_fin

Goal state after:
case compl
α : 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
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : WithTop ι
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio a)

Tactic:
· induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : OrderTop ι
⊢ Continuous[TopologicalSpace.instWithTopOfOrderTopology, instTopologicalSpaceSum] fun x ↦
    if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA

Tactic:
by
    have h_fr : frontier ({⊤} : Set (WithTop ι)) = ∅ := by
      simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]
      suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
      rw [interior_eq_iff_isOpen]
      have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
      rw [this]
      exact isOpen_Ioi
    refine continuous_if' (by simp [h_fr]) (by simp [h_fr]) (by simp) ?_
    exact Continuous.comp_continuousOn (by fun_prop) continuousOn_untopA

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

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (insert s ↑I).PairwiseDisjoint id
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ m (⋃₀ insert s ↑I) = ∑ u ∈ insert s I, m u

Tactic:
rw [Set.pairwiseDisjoint_insert_of_notMem] at h_dis

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id ∧ ∀ j ∈ ↑I, Disjoint (id s) (id j)
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ m (⋃₀ insert s ↑I) = ∑ u ∈ insert s I, m u

case insert
α : Type u_1
C : Set (Set α)
s✝ t : Set α
I✝ : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' : AddContent G C
m : Set α → G
hC : IsSetRing C
m_empty : m ∅ = 0
m_add : ∀ {s t : Set α}, s ∈ C → t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
s : Set α
I : Finset (Set α)
hsI : s ∉ I
h : ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u
h_ss : s ∈ C ∧ ↑I ⊆ C
h_dis : (insert s ↑I).PairwiseDisjoint id
h_mem : ⋃₀ insert s ↑I ∈ C
⊢ s ∉ ↑I
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ {x | ↑n ≤ ↑‖f x‖₊}.indicator f x = 0

Tactic:
rw [Set.indicator_of_notMem]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ x ∉ {x | ↑n ≤ ↑‖f x‖₊}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)

Tactic:
by
  refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_
  rw [Set.indicator_of_notMem]
  simp only [not_le, Set.mem_ofPred_eq]
  refine lt_of_le_of_lt (Nat.le_ceil _) ?_
  refine lt_of_lt_of_le (lt_add_one _) ?_
  norm_cast

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ v (⋃ b ∈ s, f b) = ∑' (p : ↑s), v (f ↑p)

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ v (⋃ x, f ↑x) = ∑' (p : ↑s), v (f ↑p)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p)

Tactic:
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ v (⋃ b ∈ s, f b) = ∑' (b : ↥s), v (f ↑b)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v.restrict ∅) i = 0 i

Tactic:
rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case intro.refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : OrderClosedTopology M
v w : VectorMeasure α M
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
val✝ : Encodable β
⊢ ∀ (n : ℕ), v ≤[⋃ b ∈ Encodable.decode₂ β n, f b] w

Tactic:
intro n
    rcases Encodable.decode₂ β n with - | b
    · simp
    · simp [hf₂ b]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
⊢ Injective toSignedMeasure

Tactic:
intro j₁

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ : JordanDecomposition α
⊢ ∀ ⦃a₂ : JordanDecomposition α⦄, j₁.toSignedMeasure = a₂.toSignedMeasure → j₁ = a₂
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ - v₂ ≪ᵥ w

Tactic:
intro s hs
  rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : Fin (n + 1)) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨min δ₁ δ₂, lt_min hδ₁pos hδ₂pos, fun i s hs hμs => ?_⟩

Goal state after:
case succ
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case h₁
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
by_cases hxu' : x ∈ uᶜ
        · exact Or.inl ⟨hxu', hx⟩
        rcases ht hx with (hxu | hxv)
        exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s A ≤ s (B n)

Tactic:
rw [hA, ← Set.sdiff_union_of_subset (Set.subset_iUnion _ n),
      of_union Set.disjoint_sdiff_left _ (hmeas n)]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ s ((⋃ i, B i) \ B n) + s (B n) ≤ s (B n)

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
h : ∀ (x : ℝ), ∃ x_1 ∈ s.measureOfNegatives, x_1 < x
f : ℕ → ℝ
hf : ∀ (n : ℕ), f n ∈ s.measureOfNegatives ∧ f n < -↑n
B : ℕ → Set α
hmeas : ∀ (n : ℕ), MeasurableSet (B n)
hr : ∀ (n : ℕ), s ≤[B n] 0
h_lt : ∀ (n : ℕ), s (B n) < -↑n
A : Set α := ⋃ n, B n
hA : A = ⋃ n, B n
n : ℕ
⊢ MeasurableSet ((⋃ i, B i) \ B n)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ (s.toMeasureOfZeroLE i hi₁ hi) univ < ∞

Tactic:
rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]
    exact ENNReal.coe_lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ lpNorm f ∞ μ = essSup (fun x ↦ ‖f x‖) μ

Tactic:
simp only [← toReal_eLpNorm hf.aestronglyMeasurable, eLpNorm_exponent_top, eLpNormEssSup]
  refine ENNReal.toReal_essSup (by simp) ⟨lpNorm f ∞ μ, ?_⟩
  simpa [-toReal_enorm, lpNorm] using! ae_le_lpNorm_exponent_top hf

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
⊢ s =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure

Tactic:
hadd

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
⊢ t + μ.withDensityᵥ f =
    (t.toJordanDecomposition.posPart + μ.withDensity fun x ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (t.toJordanDecomposition.negPart + μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).toSignedMeasure
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:

Tactic:
eLpNorm (Set.indicator s (f i)) p μ ≤
        eLpNorm (Set.indicator (s ∩ { x | C ≤ ‖f i x‖₊ }) (f i)) p μ +
          eLpNorm (Set.indicator (s ∩ { x | ‖f i x‖₊ < C }) (f i)) p μ := by
      refine le_trans (Eq.le ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
        hp)
      congr
      change _ = fun x => (s ∩ { x : α | C ≤ ‖f i x‖₊ }).indicator (f i) x +
        (s ∩ { x : α | ‖f i x‖₊ < C }).indicator (f i) x
      rw [← Set.indicator_union_of_disjoint]
      · rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_gt] :
            { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
          Set.inter_univ]
      · refine (Disjoint.inf_right' _ ?_).inf_left' _
        rw [disjoint_iff_inf_le]
        rintro x ⟨hx₁, hx₂⟩
        rw [Set.mem_ofPred_eq] at hx₁ hx₂
        exact False.elim (hx₂.ne (eq_of_le_of_not_lt hx₁ (not_lt.2 hx₂.le)).symm)
    _ ≤ eLpNorm (Set.indicator { x | C ≤ ‖f i x‖₊ } (f i)) p μ +
        (C : ℝ≥0∞) * μ s ^ (1 / ENNReal.toReal p) := by
      refine add_le_add
        (eLpNorm_mono fun x => norm_indicator_le_of_subset Set.inter_subset_right _ _) ?_
      rw [← Set.indicator_indicator]
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs]
      have : ∀ᵐ x ∂μ.restrict s, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖ ≤ C := by
        filter_upwards
        simp_rw [norm_indicator_eq_indicator_norm]
        exact Set.indicator_le' (fun x (hx : _ < _) => hx.le) fun _ _ => NNReal.coe_nonneg _
      refine le_trans (eLpNorm_le_of_ae_bound this) ?_
      rw [mul_comm, Measure.restrict_apply' hs, Set.univ_inter, ENNReal.ofReal_coe_nnreal, one_div]
    _ ≤ ENNReal.ofReal (ε / 2) + C * ENNReal.ofReal (ε / (2 * C)) := by
      grw [hC i]
      gcongr
      rwa [one_div, ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hpzero hp'),
        ENNReal.ofReal_rpow_of_pos (div_pos hε (mul_pos two_pos (NNReal.coe_pos.2 hCpos)))]
    _ ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
      gcongr
      rw [← ENNReal.ofReal_coe_nnreal, ← ENNReal.ofReal_mul (NNReal.coe_nonneg _), ← div_div,
        mul_div_cancel₀ _ (NNReal.coe_pos.2 hCpos).ne.symm]
    _ ≤ ENNReal.ofReal ε := by
      rw [← ENNReal.ofReal_add (half_pos hε).le (half_pos hε).le, add_halves]

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

Goal state before:
pp: case inr
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝² : TopologicalSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝²] s) MeasurableSet
ε : ENNReal
hε : 0 < ε
r : ENNReal := μ univ
hεr : r ≤ ε
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
exact ⟨∅, isCompact_empty, by simpa⟩

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

Goal state before:
pp: case inl
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) ⊥
⊢ limsup (fun i ↦ (μs i) Eᶜ) ⊥ ≤ μ Eᶜ

pp: case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
hne : L.NeBot
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ

Tactic:
· simp only [limsup_bot, bot_le]

Goal state after:
case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
hne : L.NeBot
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case e_μ
Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
ν : FiniteMeasure Ω'
hν : ν (range f)ᶜ = 0
⊢ (↑ν).restrict (range f) = ↑ν

Tactic:
simp only [null_iff_toMeasure_null] at hν

Goal state after:
case e_μ
Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
A : ∀ (x : Ω), g x = g' (f x)
ν : FiniteMeasure Ω'
hν : ↑ν (range f)ᶜ = 0
⊢ (↑ν).restrict (range f) = ↑ν