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

Goal state before:
pp: case refine_1.compl
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ∃ S_1, ↑S_1 ⊆ memPartition t n ∧ (⋃₀ ↑S)ᶜ = ⋃₀ ↑S_1

Tactic:
refine ⟨(memPartition t n).toFinset \ S, ?_, ?_⟩

Goal state after:
case refine_1.compl.refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ ↑((memPartition t n).toFinset \ S) ⊆ memPartition t n

case refine_1.compl.refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
S : Finset (Set α)
hS_subset : ↑S ⊆ memPartition t n
ht✝ : MeasurableSet (⋃₀ ↑S)
⊢ (⋃₀ ↑S)ᶜ = ⋃₀ ↑((memPartition t n).toFinset \ S)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ Fintype ↑(⋃ n, ↑(S n))

Tactic:
refine (Finite.subset (finite_memPartition t n) ?_).fintype

Goal state after:
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
f : ℕ → Set α
hs✝ : ∀ (n_1 : ℕ), MeasurableSet (f n_1)
S : ℕ → Finset (Set α)
hS_subset : ∀ (n_1 : ℕ), ↑(S n_1) ⊆ memPartition t n
hS_eq : ∀ (n : ℕ), f n = ⋃₀ ↑(S n)
⊢ ⋃ n, ↑(S n) ⊆ memPartition t n
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_2
α : 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 : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
⊢ g x ∈ t

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : 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 : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∈ s
⊢ g x ∈ t

case neg
α : 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 : α → β := s.piecewise (fun x ↦ h₀.some) (mk f H)
x : α
hx : x ∉ s
⊢ g x ∈ t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)

Tactic:
← map_comap_subtype_coe hs,

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ)) ↔
    AEMeasurable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ ν : Measure α
f : α → δ
h : μ ≤ ν
hf : AEMeasurable f ν
s : Set δ
hs : MeasurableSet s
⊢ (map f μ) s ≤ (map f ν) s

Tactic:
simpa [hf, hs, hf.mono_measure h] using h (f ⁻¹' s)

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

Goal state before:
pp: α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
C : Finset ι
hC : C ∈ Cs
⊢ #({a ∈ F | a ∈ C}) • (μ.restrict (P C)) t ≤ M • (μ.restrict (P C)) t

Tactic:
by_cases hPC : P C = ∅

Goal state after:
case pos
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
C : Finset ι
hC : C ∈ Cs
hPC : P C = ∅
⊢ #({a ∈ F | a ∈ C}) • (μ.restrict (P C)) t ≤ M • (μ.restrict (P C)) t

case neg
α : Type u_2
ι : Type u_6
x✝ : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), {i | y ∈ s i}.encard ≤ ↑M
t : Set α
ht : MeasurableSet t
F : Finset ι
P : Finset ι → Set α := fun C ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
G : ι → Set (Finset ι) := fun i ↦ {C | C ∈ F.powerset ∧ i ∈ C}
P_meas : ∀ (C : Finset ι), MeasurableSet (P C)
P_cover : ∀ {i : ι}, i ∈ F → s i ⊆ ⋃ C ∈ G i, P C
iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i
P_subset_s : ∀ {i : ι} {C : Finset ι}, i ∈ C → P C ⊆ s i
mem_C : ∀ {i : ι}, i ∈ F → ∀ {C : Finset ι} {x : α}, x ∈ P C → x ∈ s i → i ∈ C
C_subset_C : ∀ {C₁ C₂ : Finset ι}, C₁ ∈ Cs → ∀ {x : α}, x ∈ P C₁ ∩ P C₂ → C₁ ⊆ C₂
C : Finset ι
hC : C ∈ Cs
hPC : ¬P C = ∅
⊢ #({a ∈ F | a ∈ C}) • (μ.restrict (P C)) t ≤ M • (μ.restrict (P C)) t
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

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

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

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ AEMeasurable f (sum fun i ↦ m ↑i)

Tactic:
rwa [sum_coe_finset]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PartialOrder α
a : α
ha : μ {a} = 0
⊢ Iio a =ᵐ[μ] Iic a

Tactic:
← Iic_sdiff_right,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : PartialOrder α
a : α
ha : μ {a} = 0
⊢ Iic a \ {a} =ᵐ[μ] Iic a
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M
g : α → X
inst✝⁴ : MeasurableConstSMul M X
inst✝³ : SMul M α
inst✝² : SMul Mᵐᵒᵖ α
inst✝¹ : IsCentralScalar M α
inst✝ : MeasurableConstSMul M α
⊢ ∀ (c : Mᵐᵒᵖ), Measurable fun x ↦ c • x

Tactic:
simpa using measurable_const_smul

Goal state after:
Module: Mathlib.MeasureTheory.Group.Arithmetic

Goal state before:
pp: M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
s : Multiset (α → M)
hs : ∀ f ∈ s, AEMeasurable f μ
⊢ AEMeasurable (fun x ↦ (map (fun f ↦ f x) s).prod) μ

Tactic:
by
  simpa only [← Pi.multiset_prod_apply] using s.aemeasurable_prod hs

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ hausdorffEDist s t

Tactic:
rw [hausdorffEDist_def]
  refine le_trans ?_ le_sup_left
  exact le_iSup₂ (α := ℝ≥0∞) x h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
⊢ Pairwise (Disjoint on fun r ↦ frontier (thickening r A))

Tactic:
by
  refine (pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_
  rcases le_total r₁ 0 with h₁ | h₁
  · simp [thickening_of_nonpos h₁]
  refine ((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
    (frontier_thickening_subset _)
  apply_fun ENNReal.toReal at h
  rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ E ⊆ cthickening δ E

Tactic:
intro x hx
  rw [thickening, mem_ofPred_eq] at hx
  exact hx.le

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ (∀ (i : ι),
      ∀ i_1 ∈ s i, infEDist i_1 (⋃ i, t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))) ∧
    ∀ (i : ι),
      ∀ i_1 ∈ t i, infEDist i_1 (⋃ i, s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

Tactic:
infEDist_iUnion

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ (∀ (i : ι),
      ∀ i_1 ∈ s i, ⨅ i, infEDist i_1 (t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))) ∧
    ∀ (i : ι),
      ∀ i_1 ∈ t i, ⨅ i, infEDist i_1 (s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
by
  rcases hne with ⟨z, hz⟩
  rw [← infDist_inter_closedBall_of_mem hz]
  set t := s ∩ closedBall x (dist z x)
  have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
  have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
  obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
  exact ⟨y, hys, hyd⟩

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

Goal state before:
pp: case neg.h₁
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E

Tactic:
exact subset_iInter₂ fun ε _ => closure_subset_cthickening ε E

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
fin : hausdorffEDist s t ≠ ∞
⊢ hausdorffDist s t = 0 ↔
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
simp [← hausdorffEDist_zero_iff_closure_eq_closure, hausdorffDist,
    ENNReal.toReal_eq_zero_iff, fin]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]
  congrm (∀ ε hε, ?_)
  simp [mem_thickening_iff_infDist_lt hs₂]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s✝ : Set α
inst✝ : NullSingletonClass μ
s : Set α
⊢ NullSingletonClass (μ.restrict s)

Tactic:
by
  refine ⟨fun x => ?_⟩
  obtain ⟨t, hxt, ht1, ht2⟩ := exists_measurable_superset_of_null (measure_singleton x : μ {x} = 0)
  apply measure_mono_null hxt
  rw [Measure.restrict_apply ht1]
  apply measure_mono_null inter_subset_left ht2

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

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
s : Multiset (α → M)
hs : ∀ f ∈ s, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x ↦ (Multiset.map (fun f ↦ f x) s).prod) μ

Tactic:
by
  simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod hs

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
s : Set α
hs : μ s < (ε₂ - ε₁) / ↑C
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ (SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤
    (SimpleFunc.map ofNNReal (φ + (ψ - φ))).lintegral (μ.restrict s)

Tactic:
refine SimpleFunc.lintegral_mono (fun x => ?_) le_rfl

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
s : Set α
hs : μ s < (ε₂ - ε₁) / ↑C
ψ : α →ₛ ℝ≥0
hψ : ∀ (x : α), ↑(ψ x) ≤ f x
x : α
⊢ (SimpleFunc.map ofNNReal ψ) x ≤ (SimpleFunc.map ofNNReal (φ + (ψ - φ))) x
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 : α), φ x ∂μ + ε * μ {x | φ x + ε ≤ g x} = ∫⁻ (x : α), φ x + {x | φ x + ε ≤ g x}.indicator (fun x ↦ ε) x ∂μ

Tactic:
rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
      exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
⊢ f x ≤ s.indicator 1 x

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∈ s
⊢ f x ≤ s.indicator 1 x

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
hx : x ∉ s
⊢ f x ≤ s.indicator 1 x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, ⨆ i, ⨆ (_ : i ≥ 0), f i a ≤ g a

Tactic:
refine (ae_all_iff.2 h_bound).mono fun n hn => ?_

Goal state after:
case refine_3
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ ⨆ i, ⨆ (_ : i ≥ 0), f i n ≤ g n
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))

case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop (𝓝 (s.piecewise f g x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))

case neg
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : StronglyMeasurable f
g : ↑sᶜ → β
hg : StronglyMeasurable g
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ SimpleFunc.dite s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 ((fun x ↦ if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩) x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ t }
hxs : ↑x ∉ s
⊢ Function.extend Subtype.val (fun x ↦ f ↑x) (fun x ↦ default) ↑x = f ↑x

pp: case neg.hb
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ t }
hxs : ↑x ∉ s
⊢ ¬∃ a, ↑a = ↑x

Tactic:
Subtype.coe_injective.extend_apply

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ t }
hxs : ↑x ∉ s
⊢ f ↑x = f ↑x

case neg.hb
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable fun a ↦ f ↑a
hd : StronglyMeasurable fun a ↦ f ↑a
a✝ : Nontrivial β
inhabited_h : Inhabited β
x : { x // x ∈ t }
hxs : ↑x ∉ s
⊢ ¬∃ a, ↑a = ↑x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).restrict s) n) x) atTop (𝓝 (f x))

Tactic:
by_cases hx : x ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).restrict s) n) x) atTop (𝓝 (f x))

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
x : α
hx : x ∉ s
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).restrict s) n) x) atTop (𝓝 (f x))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C U : Set α
hC : Preperfect C
hU : IsOpen[inst✝] U
⊢ Preperfect (U ∩ C)

Tactic:
rintro x ⟨xU, xC⟩
  apply (hC _ xC).nhds_inter
  exact hU.mem_nhds xU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)

Goal state after:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
h_approx : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n ↦ support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
have h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ :=
    measure_eq_top_of_subset_compl_sigmaFiniteSetWRT subset_rfl

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ ∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D

Tactic:
refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ IsClosed[inst✝¹] D

case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ Preperfect D

case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
Vct : (V ∩ C).Countable
⊢ C = V ∩ C ∪ D