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

Goal state before:
pp: case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ⨅ (_ : ∀ (i : ℕ), P (t i)), ⨅ (_ : s ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) ≤ ∑' (n : ℕ), m (t n)

Tactic:
simp only [ht, not_false_eq_true, iInf_neg, top_le_iff]

Goal state after:
case neg
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
P : Set α → Prop
m_top : ∀ (s : Set α), ¬P s → m s = ∞
s : Set α
t : ℕ → Set α
ht_subset : s ⊆ iUnion t
ht : ¬∀ (i : ℕ), P (t i)
⊢ ∑' (i : ℕ), m (t i) = ∞
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (OuterMeasure.ofFunction m m_empty) s = m s

Tactic:
ofFunction_eq s m_mono m_subadd

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)
⊢ m s = m s
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ι : Type u_4
s : Set ι
hs : s.Countable
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Tactic:
by
  classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i ↦ ↑(w i)) i * ↑(δ i) < ε

Tactic:
refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∑' (i : ι), (fun i ↦ ↑(w i)) i * ↑((fun i ↦ δ' i / max 1 (w i)) i) < ε
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
⊢ IsPiSystem (⋃ n, p n)

Tactic:
intro t1 ht1 t2 ht2 h

Goal state after:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 ↦ x1 ⊆ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
ht2 : t2 ∈ ⋃ n, p n
h : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ ⋃ n, p n
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

Tactic:
by_cases hs : a ∈ s

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∈ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)

case neg
α : Type u_1
a : α
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : a ∈ t
hs : a ∉ s
⊢ (dirac a) t = (dirac a) (t ∩ s) + (dirac a) (t \ s)
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] s

Tactic:
convert! ae_eq_set_inter (ae_eq_refl s) h

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∩ t =ᵐ[μ] s ↔ s ∩ t =ᵐ[μ] s ∩ univ
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅

Tactic:
convert! ae_eq_set_inter (ae_eq_refl s) h

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅ ↔ s ∩ t =ᵐ[μ] s ∩ ∅
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ ∃ t ∈ f ⊓ g, MeasurableSet t ∧ t ⊆ sf ∩ sg

Tactic:
refine ⟨s'f ∩ s'g, inter_mem_inf hs'f hs'g, hmf.inter hmg, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝² : MeasurableSpace α
f g : Filter α
inst✝¹ : f.IsMeasurablyGenerated
inst✝ : g.IsMeasurablyGenerated
sf : Set α
hsf : sf ∈ f
sg : Set α
hsg : sg ∈ g
s'f : Set α
hs'f : s'f ∈ f
hmf : MeasurableSet s'f
hs'sf : s'f ⊆ sf
s'g : Set α
hs'g : s'g ∈ g
hmg : MeasurableSet s'g
hs'sg : s'g ⊆ sg
⊢ s'f ∩ s'g ⊆ sf ∩ sg
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ s \ t

Tactic:
simpa using ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
  calc
    μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (.countable_iUnion ht_eq)
    _ = ∑' i, μ (t i) := measure_iUnion htd htm
    _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ μ (⇑e.symm '' s) = μ (⇑e ⁻¹' s)

pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)

Tactic:
image_symm

Goal state after:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ μ (⇑e ⁻¹' s) = μ (⇑e ⁻¹' s)

α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
s : Set β
hs : MeasurableSet s
⊢ ∀ (s : Set β), MeasurableSet s → MeasurableSet (⇑e.symm '' s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₃ = μ (s₃ \ s₁ ∪ s₁)

Tactic:
sdiff_union_of_subset (h12.trans h23)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nullsdiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₃ = μ s₃
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : μ s ≠ ∞
⊢ μ sᶜ = μ univ - μ s

Tactic:
← measure_add_measure_compl₀ h,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : μ s ≠ ∞
⊢ μ sᶜ = μ s + μ sᶜ - μ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ μ (⋂ n, s (x n)) ≤ μ (⋂ i, s i)

Tactic:
refine measure_mono <| iInter_mono' fun i ↦ ?_

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsCodirectedOrder ι
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
⊢ ∃ i_1, s (x i_1) ⊆ s i
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝² : Countable ι
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
hfin : ∃ i, μ (f i) ≠ ∞
⊢ μ (⋂ i, f i) = μ (⋂ i', ⋂ i, ⋂ (_ : i' ≤ i), f i')

Tactic:
exact congrArg μ <| iInter_congr fun i ↦ (biInf_const nonempty_Ici).symm

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
h'T : ¬T.Nonempty
⊢ False

Tactic:
not_nonempty_iff_eq_empty.1 h'T,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ ∅ = univ
h'T : ¬T.Nonempty
⊢ False
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
h'T : ¬T.Nonempty
⊢ False

Tactic:
rw [not_nonempty_iff_eq_empty.1 h'T, sUnion_empty] at hT

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s | IsOpen[inst✝²] s ∧ μ s < ∞}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ∅ = univ
h'T : ¬T.Nonempty
⊢ False
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case inr
α : Type u_1
l : Filter α
inst✝² : CountableInterFilter l
inst✝¹ : Nonempty α
p : Set α → Prop
s : Set α
inst✝ : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
hne : s.Nonempty
⊢ ∃ a, {a} ∈ l

Tactic:
· exact (exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating p hs hne hl).imp fun _ ↦
      And.right

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ) s = (Measure.comap f μ) (f ⁻¹' f '' s)

Tactic:
by rw [hf.injective.preimage_image]

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

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), min (μ (t' n)) (ν (t' n)) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
        ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero]

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) + min (μ (t' 1)) (ν (t' 1)) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∀ (x : ℕ), (if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
⊢ ⋃ i, f ⁻¹' spanningSets (Measure.map f μ) i = univ

Tactic:
by rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
⊢ AEMeasurable f 0

Tactic:
nontriviality α; inhabit α
  exact ⟨fun _ => f default, measurable_const, rfl⟩

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ (sum fun n ↦ sum (μ n)) = sum fun p ↦ μ p.1 p.2

Tactic:
ext1 s hs
  simp [sum_apply _ hs, ENNReal.tsum_prod']

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
⊢ ∑ i, μ ↑i = ∑ i ∈ s, μ i

Tactic:
Finset.sum_coe_sort s μ

Goal state after:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
⊢ ∑ i ∈ s, μ i = ∑ i ∈ s, μ i
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hc : MeasurableSpace.CountablyGenerated β
h : NullMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
classical
  nontriviality β; inhabit β
  rcases hc.1 with ⟨S, hSc, rfl⟩
  choose! T hTf hTm hTeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_subset_ae_eq
  choose! U hUf hUm hUeq using fun s hs ↦ (h <| .basic s hs).exists_measurable_superset_ae_eq
  set v := ⋃ s ∈ S, U s \ T s
  have hvm : MeasurableSet v := .biUnion hSc fun s hs ↦ (hUm s hs).diff (hTm s hs)
  have hvμ : μ v = 0 := (measure_biUnion_null_iff hSc).2 fun s hs ↦ ae_le_set.1 <|
    ((hUeq s hs).trans (hTeq s hs).symm).le
  refine ⟨v.piecewise (fun _ ↦ default) f, ?_, measure_mono_null (fun x ↦
    not_imp_comm.2 fun hxv ↦ (piecewise_eq_of_notMem _ _ _ hxv).symm) hvμ⟩
  refine measurable_of_restrict_of_restrict_compl hvm ?_ ?_
  · rw [domRestrict_piecewise]
    apply measurable_const
  · rw [domRestrict_piecewise_compl, domRestrict_eq]
    refine measurable_generateFrom fun s hs ↦ .of_subtype_image ?_
    rw [preimage_comp, Subtype.image_preimage_coe]
    convert! (hTm s hs).diff hvm using 1
    rw [inter_comm]
    refine Set.ext fun x ↦ and_congr_left fun hxv ↦ ⟨fun hx ↦ ?_, fun hx ↦ hTf s hs hx⟩
    exact by_contra fun hx' ↦ hxv <| mem_biUnion hs ⟨hUf s hs hx, hx'⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ⊆ s

Tactic:
· rwa [compl_mem_cofinite, measure_toMeasurable]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ⊆ s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x ↦ μ (Ioc x a)) atBot (𝓝 (μ (Iic a)))

Tactic:
by
  rw [← iUnion_Ioc_left]
  exact tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : OpensMeasurableSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : OpensMeasurableSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : TopologicalSpace γ₂
inst✝³ : MeasurableSpace γ₂
inst✝² : BorelSpace γ₂
inst✝¹ : MeasurableSpace δ
inst✝ : T0Space α
⊢ MeasurableSpace.SeparatesPoints α

Tactic:
rw [separatesPoints_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹³ : TopologicalSpace α
inst✝¹² : MeasurableSpace α
inst✝¹¹ : OpensMeasurableSpace α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : OpensMeasurableSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : TopologicalSpace γ₂
inst✝³ : MeasurableSpace γ₂
inst✝² : BorelSpace γ₂
inst✝¹ : MeasurableSpace δ
inst✝ : T0Space α
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (Iio a)

Tactic:
convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u < a), Icc l u)

Goal state after:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ Iio a = ⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u

case pos
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
hd : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s
S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Icc l u = S}
this : MeasurableSpace α := MeasurableSpace.generateFrom S
a : α
t : Set α
hts : t ⊆ s
hc : t.Countable
htd : Dense t
htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t
ha : ∀ b < a, (Ioo b a).Nonempty
⊢ MeasurableSet (⋃ l ∈ t, ⋃ u ∈ t, ⋃ (_ : l < u), ⋃ (_ : u < a), Icc l u)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
by
  rw [infEDist_closure, infEDist_pos_iff_notMem_closure]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ Measurable f

Tactic:
apply measurable_of_measurable_on_compl_countable _ hs

Goal state after:
α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSingletonClass α
f : α → γ
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
⊢ Measurable (sᶜᶜ.domRestrict f)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (infEDist y s + ediam s) ≤ ↑ε + ↑δ + (↑ε + ediam s)

Tactic:
grw [hy]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : IsCompact s
hne : s.Nonempty
x y : α
hys : y ∈ s
hy : infEDist x s = edist x y
⊢ infDist x s = dist x y

Tactic:
by rw [infDist, dist_edist, hy]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Tactic:
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx

Goal state after:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ x ∈ E, closedBall x δ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Preorder β
s : Set α
f₁ f₂ g₁ g₂ : α →ₛ β
hs : MeasurableSet s
hf : ∀ a ∈ s, f₁ a ≤ f₂ a
hg : ∀ a ∉ s, g₁ a ≤ g₂ a
⊢ piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂

Tactic:
exact Set.piecewise_mono hf hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ s.piecewise ⇑f ⇑0 = s.indicator ⇑f

Tactic:
coe_zero,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ s.piecewise (⇑f) 0 = s.indicator ⇑f
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ (piecewise {a | ennrealRatEmbed b ≤ f a} h✝ (const α (ennrealRatEmbed b)) 0) a < ∞

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ∞

Tactic:
· simp only [coe_zero, coe_piecewise, piecewise_eq_indicator, coe_const]
    calc
      { a : α | ennrealRatEmbed b ≤ f a }.indicator (fun _ => ennrealRatEmbed b) a ≤
          ennrealRatEmbed b :=
        indicator_le_self _ _ a
      _ < ⊤ := ENNReal.coe_lt_top

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
a✝ : b ∈ Finset.range n
h✝ : ¬MeasurableSet {a | ennrealRatEmbed b ≤ f a}
⊢ 0 a < ∞