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

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b : ∃ a, (∃ (x : a ∈ s), ⟨a, ⋯⟩ ∈ T) ∧ a = b
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b

Tactic:
exists_eq_right

Goal state after:
case refine_2
α : Type u_3
β : Type u_4
g : β → Set (Set α)
s : Set β
h_pi : ∀ b ∈ s, IsPiSystem (g b)
T : Finset ↑s
f : ↑s → Set α
h_t' : ∀ b ∈ T, f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b ∈ s, g b)
this : ⋂ b ∈ T, f b ∈ generatePiSystem (⋃ b, (g ∘ Subtype.val) b)
b : β
h_b : ∃ (x : b ∈ s), ⟨b, ⋯⟩ ∈ T
⊢ Function.extend (fun x ↦ ↑x) f (fun x ↦ ∅) b ∈ g b
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ i, f i
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ ∑' (i : ℕ), extend m (f i)

Tactic:
refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)

Goal state after:
case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
f : ℕ → Set α
hf : s ⊆ ⋃ i, f i
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ extend m (⋃ i, f i)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
P0 : P ∅
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
Pu : P univ
⊢ inducedOuterMeasure (fun x x_1 ↦ 0) P0 inducedOuterMeasure_zero._proof_1 = 0

Tactic:
by
  ext s
  rw [inducedOuterMeasure_eq_iInf PU (fun _ _ => by simp) (fun _ _ => by simp)]
  exact le_antisymm (iInf₂_le_of_le univ Pu (by simp)) zero_le

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
⊢ μ₁.trim = μ₂.toOuterMeasure

Tactic:
OuterMeasure.trim_congr (h _),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → μ₁ s = μ₂ s
⊢ μ₂.trim = μ₂.toOuterMeasure
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 : s =ᵐ[μ] ∅
⊢ s ∩ t =ᵐ[μ] ∅

Tactic:
convert! ae_eq_set_inter h (ae_eq_refl t)
  rw [empty_inter]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace ((generate s).toMeasurableSpace ⋯) ≤ ofMeasurableSpace (generateFrom s)

Tactic:
by
      rw [ofMeasurableSpace_toMeasurableSpace]
      exact generate_le _ fun t ht => measurableSet_generateFrom ht

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
⊢ EventuallyMeasurableSet m l s

Tactic:
rcases ht with ⟨t', ht', htt'⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
hst : s =ᶠ[l] t
t' : Set α
ht' : MeasurableSet t'
htt' : t =ᶠ[l] t'
⊢ EventuallyMeasurableSet m l s
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ ⇑e.symm '' s = t ↔ ⇑e.symm '' s = t

Tactic:
coe_toEquiv_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ ⇑e.symm '' s = t ↔ ⇑e.symm '' s = t
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [← measure_inter_add_sdiff₀ (s ∪ t) ht, union_inter_cancel_right, union_sdiff_right, ←
    measure_inter_add_sdiff₀ s ht, add_comm, ← add_assoc, add_right_comm]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
by rw [← measure_union_add_inter₀ s ht, hd, add_zero]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
h : f =ᵐ[μ] g
hf : AEMeasurable f μ
⊢ map f μ = map g μ

Tactic:
have hg : AEMeasurable g μ := hf.congr h
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
    exact
      mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
if hfm : AEMeasurable f μ then
    rw [← map_apply₀ hfm, hf]
    rwa [hf]
  else
    rw [map_of_not_aemeasurable hfm] at hf
    simp [← hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ Injective (map f)

Tactic:
intro μ

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
⊢ ∀ ⦃a₂ : Measure α⦄, map f μ = map f a₂ → μ = a₂
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e) μ₁ = map (⇑e) μ₂
⊢ μ₁ = μ₂

Tactic:
apply_fun Measure.map e.symm at hμ

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e.symm) (map (⇑e) μ₁) = map (⇑e.symm) (map (⇑e) μ₂)
⊢ μ₁ = μ₂
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : μ s₂ ≠ ∞
⊢ μ (s₁ \ s₂) = μ s₁ - μ s₂

Tactic:
by rw [measure_sdiff' _ h₂ h_fin, union_eq_self_of_subset_right h]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
hd : DirectedOn ((fun x1 x2 ↦ x1 ⊆ x2) on s) t
this : Countable ↑t
⊢ μ (⋃ x, s ↑x) = ⨆ i ∈ t, μ (s i)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case insert
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ ν : Measure α
t : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)
⊢ μ.restrict (t i ∪ ⋃ x ∈ s, t x) = ν.restrict (t i ∪ ⋃ x ∈ s, t x) ↔
    μ.restrict (t i) = ν.restrict (t i) ∧ ∀ a ∈ s, μ.restrict (t a) = ν.restrict (t a)

Tactic:
rw [restrict_union_congr, ← hs]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄,
    (∃ U ⊇ s, IsOpen[inst✝¹] U ∧ μ U < ∞) →
      (∃ U ⊇ t, IsOpen[inst✝¹] U ∧ μ U < ∞) → ∃ U ⊇ s ∪ t, IsOpen[inst✝¹] U ∧ μ U < ∞

Tactic:
rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩
    refine
      ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
        (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
h✝ : Nonempty α
⊢ Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen[inst✝²] K})

Tactic:
inhabit α

Goal state after:
case inr
α : 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 α
⊢ Nonempty (μ.FiniteSpanningSetsIn {K | IsOpen[inst✝²] K})
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.trim hm) s

Tactic:
Measure.trim

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ μ s ≤ (μ.toMeasure ⋯) s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ (sum μ).restrict s = sum fun i ↦ (μ i).restrict s

Tactic:
ext t ht

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s t : Set α
ht : MeasurableSet t
⊢ ((sum μ).restrict s) t = (sum fun i ↦ (μ i).restrict s) t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ x, s ↑x)) = ⨆ i ∈ t, ae (μ.restrict (s i))
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ∀ ⦃x : Measure α⦄,
    x ∈ m →
      ∀ (i : Set α),
        t ⊆ i → MeasurableSet i → (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ x i

Tactic:
intro μ

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
⊢ μ ∈ m →
    ∀ (i : Set α),
      t ⊆ i → MeasurableSet i → (⨅ μ ∈ toOuterMeasure '' m, μ (t ∩ s)) + ⨅ μ ∈ toOuterMeasure '' m, μ (t \ s) ≤ μ i
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 (μ.restrict s) = (Measure.comap f μ).restrict (f ⁻¹' s)

Tactic:
ext t ht

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
t : Set α
ht : MeasurableSet t
⊢ (Measure.comap f (μ.restrict s)) t = ((Measure.comap f μ).restrict (f ⁻¹' s)) t
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) = (comap g μ) s

Tactic:
hg.comap_apply,

Goal state after:
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
x✝ : MeasurableSpace β
f : α → β
g : β → α
μ : Measure α
hf : Measurable f
hg : MeasurableEmbedding g
hμg : ∀ᵐ (a : α) ∂μ, a ∈ range g
hfg : ∀ (a : β), f (g a) = a
s : Set β
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) = μ (g '' s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case refine_3.refine_1
α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
q : (ℕ → Prop) → Prop
htq : t = ⋃ p, if q p then countablyGeneratedAtom α p else ∅
x : α
h : ∀ (i : ℕ → Prop), q i → x ∉ countablyGeneratedAtom α i
⊢ ∃ i, ¬q i ∧ x ∈ countablyGeneratedAtom α i

Tactic:
refine ⟨fun n ↦ x ∈ natGeneratingSequence α n, ?_,
        mem_countablyGeneratedAtom_natGeneratingSequence x⟩
      contrapose! h
      refine ⟨fun n ↦ x ∈ natGeneratingSequence α n, h,
        mem_countablyGeneratedAtom_natGeneratingSequence x⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (μ + ν)

Tactic:
← sum_cond

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (sum fun b ↦ bif b then μ else ν)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

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

Tactic:
inhabit α

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f 0
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
⊢ AEMeasurable (codRestrict f s hfs) μ

Tactic:
inhabit α

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
s : Set β
hfs : ∀ (x : α), f x ∈ s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable (codRestrict f s hfs) μ
Module: Mathlib.Topology.Separation.GDelta

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
Ts : Set (Set X)
hoTs : ∀ t ∈ Ts, IsOpen[inst✝²] t
hyK : ∀ t ∈ Ts, y ∈ t
t✝ : Set X
a✝ : t✝ ∈ Ts
⊢ x ∈ t✝

Tactic:
solve_by_elim [hxy.mem_open]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s

Tactic:
by
  refine le_antisymm (infEDist_anti subset_closure) ?_
  refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_
  have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
  have : infEDist x (closure s) < infEDist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'
  obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEDist x (closure s) + ↑ε / 2⟩ :=
    infEDist_lt_iff.mp this
  obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0
  calc
    infEDist x s ≤ edist x z := infEDist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEDist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEDist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

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

Goal state before:
pp: case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ ∀ t ∈ {S | ∃ l u, l ≤ u ∧ Ioc l u = S}, MeasurableSet t

Tactic:
rintro - ⟨u, v, -, rfl⟩

Goal state after:
case a
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
u v : α
⊢ MeasurableSet (Ioc u v)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

pp: case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E

Tactic:
· exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E

Goal state after:
case h₂
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
obtain hε | hε := le_total ε 0
  · simp only [thickening_of_nonpos hε, empty_subset]
  intro x
  simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEDist_lt_iff,
    ENNReal.ofReal_add hε hδ]
  rintro ⟨y, hy, hxy⟩
  exact infEDist_le_edist_add_infEDist.trans_lt
    (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
H : ∀ x ∈ s, ∃ b, x < b
⊢ ∀ x ∈ s, ∃ y, x < y

Tactic:
exact H

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
⊢ f.lintegral μ ≤ g.lintegral μ

Tactic:
refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h
  calc
    f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left

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

Goal state before:
pp: a : ℝ
this : IsLUB (range Rat.cast ∩ Iio a) a
⊢ MeasurableSet (⋃ y ∈ Rat.cast ⁻¹' Iio a, Iio ↑y)

Tactic:
exact MeasurableSet.biUnion (to_countable _)
    fun b _ => GenerateMeasurable.basic (Iio (b : ℝ)) (by simp)

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

Goal state before:
pp: ⊢ IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b})

Tactic:
by
  convert! isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)
  ext x
  simp [eq_comm]

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b - s ≤ b - r

Tactic:
by linarith

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b r s : ℝ
_rpos : 0 < r
hrs : r ≤ s
⊢ b + r ≤ b + s

Tactic:
by linarith

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

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b r : ℝ
hr : r < 0
⊢ ¬b - r ≤ b + r

Tactic:
by linarith

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
⊢ AEStronglyMeasurable f 0

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEStronglyMeasurable f 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝ : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
⊢ StronglyMeasurable f

Tactic:
inhabit α

Goal state after:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝ : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ StronglyMeasurable f
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
ι' : ι → Sort u_5
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ⨆ i, ⨆ j, ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ i, ⨆ j, f i j a ∂μ

Tactic:
convert! (monotone_lintegral μ).le_map_iSup₂ f with a
  simp only [iSup_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
⊢ f = fun x ↦ f hα.some

Tactic:
have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
⊢ f = fun x ↦ f hα.some
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Monotone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
hx : x ∉ aeSeqSet hf p
⊢ aeSeq hf p n x ≤ aeSeq hf p m x

Tactic:
· simp only [aeSeq, hx, if_false, le_rfl]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
⊢ g.lintegral μ = g.lintegral (μ.restrict s)

Tactic:
rw [lintegral_restrict, SimpleFunc.lintegral]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
g : α →ₛ ℝ≥0∞
hg : ⇑g ≤ fun a ↦ s.indicator f a
this : ⇑g ≤ f
⊢ ∑ x ∈ g.range, x * μ (⇑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ ∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ

Tactic:
biUnion_eq_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set β
s : β → Set α
ht : t.Countable
hm : ∀ i ∈ t, NullMeasurableSet (s i) μ
hd : t.Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ ∫⁻ (a : α) in ⋃ x, s ↑x, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ

Tactic:
← lintegral_add_measure

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
⊢ ∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α), f a ∂(μ.restrict s + μ.restrict t)