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

Goal state before:
pp: case cons
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t✝ : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
⊢ a ∩ ⋂ x ∈ t, x ∈ S

Tactic:
refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'

Goal state after:
case cons
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t✝ : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
h' : (a ∩ ⋂ x ∈ t, x).Nonempty
ht : ∀ (s : Set α), s = a ∨ s ∈ t → s ∈ S
⊢ ⋂ x ∈ t, x ∈ S
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
ι : Type u_1
s : ι → Set α
t : Finset ι
h : ∀ i ∈ ↑t, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i ∈ ↑t, s i)

Tactic:
induction t using Finset.induction_on with

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ f_s b ∩ f_t' b ∈ g b

Tactic:
refine h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono ?_ h_nonempty)

Goal state after:
case pos
α : Type u_3
β : Type u_4
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ b ∈ T_t', f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_t', f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ b ∈ T_s, f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ b, g b) (⋂ b ∈ T_s, f_s b)
h_nonempty : ((⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b).Nonempty
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (⋂ b ∈ T_s, f_s b) ∩ ⋂ b ∈ T_t', f_t' b ⊆ f_s b ∩ f_t' b
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t = ∅
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
by simp [ht]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case refine_1
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} → s ∈ π i ∨ s ∈ {univ}

Tactic:
rintro ⟨t, hti, f, hfπ, rfl⟩
    simp only [subset_singleton_iff, Finset.mem_coe] at hti
    by_cases hi : i ∈ t
    · have ht_eq_i : t = {i} := by
        ext1 x
        rw [Finset.mem_singleton]
        exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
      simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
      exact Or.inl (hfπ i hi)
    · have ht_empty : t = ∅ := by
        ext1 x
        simp only [Finset.notMem_empty, iff_false]
        exact fun hx => hi (hti x hx ▸ hx)
      simp [ht_empty, iInter_univ, Set.mem_singleton univ]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ ↑(p1 ∪ p2) ⊆ S

Tactic:
simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
x : α
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
by by_cases h : x ∈ s <;> simp [h]

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

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
i₁ : α₁ → α
i₂ : α₂ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
h : univ ⊆ range i₁ ∪ range i₂
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
⊢ s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

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

Goal state before:
pp: α : Type u_1
α₁ : Type u_6
α₂ : Type u_7
α₃ : Type u_8
mα : MeasurableSpace α
mα₁ : MeasurableSpace α₁
mα₂ : MeasurableSpace α₂
mα₃ : MeasurableSpace α₃
i₁ : α₁ → α
i₂ : α₂ → α
i₃ : α₃ → α
s : Set α
hi₁ : MeasurableEmbedding i₁
hi₂ : MeasurableEmbedding i₂
hi₃ : MeasurableEmbedding i₃
h : univ ⊆ range i₁ ∪ range i₂ ∪ range i₃
hs₁ : MeasurableSet (i₁ ⁻¹' s)
hs₂ : MeasurableSet (i₂ ⁻¹' s)
hs₃ : MeasurableSet (i₃ ⁻¹' s)
⊢ s = i₁ '' i₁ ⁻¹' s ∪ i₂ '' i₂ ⁻¹' s ∪ i₃ '' i₃ ⁻¹' s

Tactic:
simp [image_preimage_eq_range_inter, ← union_inter_distrib_right, univ_subset_iff.1 h]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s

Tactic:
by
  rcases h with ⟨t, htm, hst⟩
  refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩
  · exact sdiff_subset_iff.1 (subset_toMeasurable _ _)
  · have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
    simpa only [union_empty] using hst.symm.union this

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 μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s

Tactic:
else

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → α
hf : map f μ = μ
s : Set α
hs : NullMeasurableSet s μ
hfm : ¬AEMeasurable f μ
⊢ μ (f ⁻¹' s) = μ s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
⊢ Measure.comap f (μ + ν) = Measure.comap f μ + Measure.comap f ν

Tactic:
ext s hs
  simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs,
    map_add, add_apply]

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

Goal state before:
pp: case pos.mpr
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty ↑s
hsub : s ⊆ Iio b
⊢ (∀ a < b, (s ∩ Ioo a b).Nonempty) → comap Subtype.val (𝓝[<] b) = atTop

Tactic:
intro h
      refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
      · intro a hab
        rcases h a hab with ⟨c, hcs, hc⟩
        use ⟨c, hcs⟩
        simp_all [subset_def, hc.1.trans_le]
      · rintro ⟨a, has⟩ -
        use a, hsub has
        simp_all [subset_def, le_of_lt]

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

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
rw [← ENNReal.sub_sub_cancel hk (iInf_le (fun i => μ (s i)) k), ENNReal.sub_iInf, ←
    ENNReal.sub_sub_cancel hk (measure_mono (iInter_subset _ k)), ←
    measure_sdiff (iInter_subset _ k) (.iInter h) (this _ (iInter_subset _ k)),
    sdiff_iInter, Directed.measure_iUnion]

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ s k \ s i
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
restrict_apply' hs

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ μ (t ∩ s) = 0 ↔ μ (t ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < ∑' (i_1 : ℕ), (sfiniteSeq μ i_1) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ False

pp: case hs
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))

Tactic:
· simp_rw [con] at hi
      simp at hi

Goal state after:
case hs
α : Type u_1
ι : Type u_4
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : 0 < (sum (sfiniteSeq μ)) (As i)
con : ∀ (x : ℕ), (sfiniteSeq μ x) (As i) = 0
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))
Module: Mathlib.MeasureTheory.Measure.Trim

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable f

Tactic:
· exact Measurable.of_comap_le le_rfl

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

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

Tactic:
@measure_toMeasurable _ m

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : (μ.trim hm) s = 0
⊢ (μ.trim hm) s = 0
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
⊢ memPartitionSet f n a ∈ memPartition f n

Tactic:
by
  induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]

Goal state after:
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α p t

Tactic:
choose! V hpV hV using fun s hs ↦ hpq s (hSq s hs)

Goal state after:
α : Type u_1
p : Set α → Prop
t : Set α
q : Set ↑t → Prop
h : HasCountableSeparatingOn (↑t) q univ
hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U
S : Set (Set ↑t)
hSc : S.Countable
hSq : ∀ s ∈ S, q s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
V : Set ↑t → Set α
hpV : ∀ s ∈ S, p (V s)
hV : ∀ s ∈ S, Subtype.val ⁻¹' V s = s
⊢ HasCountableSeparatingOn α p t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : 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 : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : ¬(⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)

Tactic:
else

Goal state after:
α : 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 : Set α
m : Set (Measure α)
x✝ : MeasurableSpace α
f : ℕ → Set α
a✝¹ : ∀ (i : ℕ), MeasurableSet (f i)
a✝ : Pairwise (Disjoint on f)
hne : ¬(⋃ i, f i).Nonempty
⊢ ∑' (i : ℕ), ⊤ (f i) ≤ ⊤ (⋃ i, f i)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: α : Type u_1
l : Filter α
inst✝ : CountableInterFilter l
p : Set α → Prop
s : Set α
h : HasCountableSeparatingOn α p s
hs : s ∈ l
hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l
⊢ ∃ t ⊆ s, t.Subsingleton ∧ t ∈ l

Tactic:
by
  rcases h.1 with ⟨S, hSc, hSp, hS⟩
  refine ⟨s ∩ ⋂₀ (S ∩ l.sets) ∩ ⋂ (U ∈ S) (_ : Uᶜ ∈ l), Uᶜ, ?_, ?_, ?_⟩
  · exact fun _ h ↦ h.1.1
  · intro x hx y hy
    simp only [mem_sInter, mem_inter_iff, mem_iInter, mem_compl_iff] at hx hy
    refine hS x hx.1.1 y hy.1.1 (fun s hsS ↦ ?_)
    cases hl s (hSp s hsS) with
    | inl hsl => simp only [hx.1.2 s ⟨hsS, hsl⟩, hy.1.2 s ⟨hsS, hsl⟩]
    | inr hsl => simp only [hx.2 s hsS hsl, hy.2 s hsS hsl]
  · exact inter_mem
      (inter_mem hs ((countable_sInter_mem (hSc.mono inter_subset_left)).2 fun _ h ↦ h.2))
      ((countable_bInter_mem hSc).2 fun U hU ↦ iInter_mem'.2 id)

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ (μ.restrict s) (t \ s) = 0

Tactic:
rw [Measure.restrict_apply₀' hs]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
h : NullMeasurableSet (t ∩ s) μ
⊢ μ (t \ s ∩ s) = 0
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ MeasurableSet {x}

Tactic:
convert! MeasurableSet.iInter fun y ↦ .iInter fun h ↦ hsm y h

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : SeparatesPoints α
x : α
s : (y : α) → x ≠ y → Set α
hsm : ∀ (y : α) (h : x ≠ y), MeasurableSet (s y h)
hxs : ∀ (y : α) (h : x ≠ y), x ∈ s y h
hys : ∀ (y : α) (h : x ≠ y), y ∉ s y h
⊢ {x} = ⋂ b, ⋂ (b_1 : x ≠ b), s b b_1
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g

Tactic:
let s : Set α := toMeasurable μ { x | f x = H.mk f x ∧ f x ∈ t }ᶜ

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
H : AEMeasurable f μ
t : Set β
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
h₀ : t.Nonempty
s : Set α := toMeasurable μ {x | f x = mk f H x ∧ f x ∈ t}ᶜ
⊢ ∃ g, Measurable g ∧ range g ⊆ t ∧ f =ᵐ[μ] g
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), (f i) t = (f i) s
⊢ ∑' (i : ι), (f i) t = ∑' (i : ι), (f i) s

Tactic:
by simp [ht]

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 δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
s : (a : ι) → Set (X a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ countableBasis (X a)
a : ι
ha : a ∈ ↑i
⊢ IsOpen[t' a] (s a)

Tactic:
rw [eq_generateFrom_countableBasis (X a)]

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 δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
this :
  topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = (↑i).pi s}
s : (a : ι) → Set (X a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ countableBasis (X a)
a : ι
ha : a ∈ ↑i
⊢ IsOpen[TopologicalSpace.generateFrom (countableBasis (X a))] (s a)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case neg
α : 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 = ∅
⊢ MeasurableSet (Iio a)

Tactic:
rcases ha with ⟨b, ba, hb⟩
    have hbs : b ∈ s := hIoo b a ba hb
    convert_to MeasurableSet (⋃ (l ∈ t) (_ : l ≤ b), Icc l b)
    · ext x
      simp only [mem_Iio, mem_iUnion, mem_Icc, exists_and_left, exists_prop]
      refine ⟨fun h ↦ ?_, fun ⟨y, yx, hy1, hy2, hy⟩ ↦ by order⟩
      have : x ≤ b := by
        contrapose! hb
        exact ⟨x, hb, h⟩
      rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
      exact ⟨z, hzx, by order, hzt, by order⟩
    · refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
      exact .basic _ ⟨x, hts hx, b, hbs, hlt, mem_singleton _⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s₁ t₁ : Set α
s₂ t₂ : Set β
⊢ hausdorffEDist (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) ≤ max (hausdorffEDist s₁ t₁) (hausdorffEDist s₂ t₂)

Tactic:
refine le_of_forall_ge fun _ _ => ?_
  simp_all only [hausdorffEDist, infEDist_prod, max_le_iff, iSup_le_iff, mem_prod, true_and,
    implies_true]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x s ≤ dist x y

Tactic:
rw [dist_edist, infDist]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEDist x s).toReal ≤ (edist x y).toReal
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
A :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
⊢ (fun x ↦ μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) =ᶠ[𝓝[≤] 0] fun r ↦ μ (cthickening r s)

Tactic:
filter_upwards [self_mem_nhdsWithin (α := ℝ)] with _ hr

Goal state after:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ∞
A :
  Tendsto (fun r ↦ μ (cthickening r s)) (𝓝[>] 0)
    (𝓝 (μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
a✝ : ℝ
hr : a✝ ∈ Iic 0
⊢ μ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = μ (cthickening a✝ s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a | f a ≤ g a} x

Tactic:
change (hf.mk f x ≤ hg.mk g x) = (f x ≤ g x)

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ (AEStronglyMeasurable.mk f hf x ≤ AEStronglyMeasurable.mk g hg x) = (f x ≤ g x)
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:
by
  convert! (monotone_lintegral μ).le_map_iSup₂ f with a
  simp only [iSup_apply]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), f x ∂μ + ε * μ {x | f x + ε ≤ g x} = ∫⁻ (x : α), φ x ∂μ + ε * μ {x | f x + ε ≤ g x}

Tactic:
hφ_eq

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), φ a ∂μ + ε * μ {x | f x + ε ≤ g x} = ∫⁻ (x : α), φ x ∂μ + ε * μ {x | f x + ε ≤ g x}