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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᵐ[μ] g
s : Set β
hs : MeasurableSet s
⊢ ((mapₗ f) μ) s = ((mapₗ g) μ) s

Tactic:
simpa only [mapₗ, hf, hg, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply]
    using! measure_congr (h.preimage s)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᵐ[μ] g
⊢ (mapₗ f) μ = (mapₗ g) μ

Tactic:
ext1 s hs
  simpa only [mapₗ, hf, hg, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply]
    using! measure_congr (h.preimage s)

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

Tactic:
have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ map f (c • μ) = c • map f μ
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ c • map f μa ≪ c • μb

Tactic:
exact hf.2.smul c

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

Goal state before:
pp: case hfi
β : Type u_2
mβ : MeasurableSpace β
μ : Measure β
s : Set β
hs : MeasurableSet s
⊢ Injective fun x ↦ x

Tactic:
exact injective_id

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∑ x ∈ s, μ (id ⁻¹' {x}) = μ ↑s

Tactic:
sum_measure_preimage_singleton

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ μ (id ⁻¹' ↑s) = μ ↑s

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst✝ : MeasurableSingletonClass α
⊢ ∀ y ∈ s, MeasurableSet (id ⁻¹' {y})
Module: Mathlib.Topology.Order.AtTopBotIxx

Goal state before:
pp: case pos.mpr.refine_1
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
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ ∀ i < b, ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo i b

Tactic:
intro a hab

Goal state after:
case pos.mpr.refine_1
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
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
hab : a < b
⊢ ∃ i', True ∧ Ici i' ⊆ Subtype.val ⁻¹' Ioo a b
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ μ t - μ s = 0

Tactic:
h₂,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᵐ[μ] t
hsm : NullMeasurableSet s μ
h₂ : μ t = μ s
ht : μ s ≠ ∞
⊢ μ s - μ s = 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (0 n)

Tactic:
Pi.zero_apply

Goal state after:
case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure 0
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ∞

Tactic:
by
  simp [isFiniteMeasure_iff, lt_top_iff_ne_top]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ (univ ∩ s) = μ s

Tactic:
Set.univ_inter

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ s
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : ∀ t ⊆ s, MeasurableSet t → μ t = ν t
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) = ν (t ∩ s)

Tactic:
H _ inter_subset_right (ht.inter hs)

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
H : ∀ t ⊆ s, MeasurableSet t → μ t = ν t
t : Set α
ht : MeasurableSet t
⊢ ν (t ∩ s) = ν (t ∩ s)
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: β : Type u_2
m₁ m₂ : MeasurableSpace β
h₁ : CountablyGenerated β
h₂ : CountablyGenerated β
⊢ CountablyGenerated β

Tactic:
rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩

Goal state after:
β : Type u_2
m₂ : MeasurableSpace β
h₂ : CountablyGenerated β
b₁ : Set (Set β)
hb₁c : b₁.Countable
⊢ CountablyGenerated β
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case hC
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
t : Set ↑s
hs : NullMeasurableSet s μ
t' : Set ↑s
ht' : t' ∈ {t | ∃ s_1, MeasurableSet s_1 ∧ Subtype.val ⁻¹' s_1 = t}
ht✝ : MeasurableSet t'
⊢ NullMeasurableSet (Subtype.val '' t') μ

Tactic:
| hC t' ht' =>

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
h : CountablySeparated α
⊢ ∃ m', CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Tactic:
rcases h with ⟨b, bct, hbm, hb⟩
  refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩
  · use b
  rw [@separatesPoints_iff]
  exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ <| measurableSet_generateFrom hs

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

Goal state before:
pp: 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

Tactic:
simp only [Finset.coe_sdiff, coe_toFinset]
        exact sdiff_subset

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 : α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : IsLocallyFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
choose s hsx hsμ using μ.finiteAt_nhds
  rcases TopologicalSpace.countable_cover_nhds hsx with ⟨t, htc, htU⟩
  refine Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_
  rwa [sUnion_image]

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

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

Tactic:
exact ⟨fun _ => f default, measurable_const, rfl⟩

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

Goal state before:
pp: α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ generateFrom (memPartition t n) ≤ generateFrom (range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t]
  exact generateFrom_mono (subset_iUnion _ _)

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

Goal state before:
pp: case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (β × α) γ

Tactic:
· exact ⟨Or.inr h⟩

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

Goal state before:
pp: α✝ : Type u_1
G : Type u_2
α : Type u_3
β✝ : Type u_4
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β✝
f g : α → G
μ : Measure α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
⊢ MeasurableSet {p | p.1 = p.2}

Tactic:
le_antisymm_iff,

Goal state after:
α✝ : Type u_1
G : Type u_2
α : Type u_3
β✝ : Type u_4
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β✝
f g : α → G
μ : Measure α
β : Type u_5
inst✝⁶ : AddCommMonoid β
inst✝⁵ : PartialOrder β
inst✝⁴ : CanonicallyOrderedAdd β
inst✝³ : Sub β
inst✝² : OrderedSub β
x✝ : MeasurableSpace β
inst✝¹ : MeasurableSub₂ β
inst✝ : MeasurableSingletonClass β
⊢ MeasurableSet {p | p.1 ≤ p.2 ∧ p.2 ≤ p.1}
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet ((fun y ↦ (x, f y)) '' s)

Tactic:
convert! (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
s : Set γ
hs : MeasurableSet s
⊢ (fun y ↦ (x, f y)) '' s = {x} ×ˢ (f '' s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)

Tactic:
by
  simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
    ENNReal.tsum_mul_left]
  apply ENNReal.tsum_comm

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : PseudoMetrizableSpace β
inst✝² : MeasurableSpace β
inst✝¹ : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun x f' ↦ Tendsto (fun n ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → β := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ f (v i) x) atTop (𝓝 (g x))

Tactic:
exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx

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

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
⊢ ⇑0 '' ⇑f ⁻¹' {x} ⊆ {0}

Tactic:
rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
⊢ ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i

Tactic:
refine Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => ?_

Goal state after:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ norm_sets i → x ∈ norm_sets j
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {c} = ↑s → P f
f : α →ₛ γ
h : range ⇑f \ {c} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α c) f
⊢ ⇑(SimpleFunc.const α c) '' ⇑f ⁻¹' {x} ⊆ {c}

Tactic:
rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)

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

Goal state before:
pp: case neg
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) (g' x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g') p) < ε

Tactic:
simp only [SimpleFunc.piecewise_apply, H, ite_false]
        apply hg'
        simpa [H] using (mem_union _ _ _).1 hp

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

Goal state before:
pp: case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ∞
h_meas : μ (⇑φ ⁻¹' {∞}) ≠ 0
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {∞})
⊢ (∀ (x : α), (⇑φ ⁻¹' {∞}).indicator (fun x ↦ ↑(Function.const α (↑n) x)) x ≤ f x) ∧ b < ↑n * μ (⇑φ ⁻¹' {∞})

Tactic:
refine ⟨indicator_le fun x hx => le_trans ?_ (hφ _), hn⟩

Goal state after:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ∞
h_meas : μ (⇑φ ⁻¹' {∞}) ≠ 0
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {∞})
x : α
hx : x ∈ ⇑φ ⁻¹' {∞}
⊢ ↑(Function.const α (↑n) x) ≤ φ x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : PseudoMetrizableSpace β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
borelize β
  refine aestronglyMeasurable_iff_aemeasurable_separable.2 ⟨?_, ?_⟩
  · exact aemeasurable_of_tendsto_metrizable_ae _ (fun n => (hf n).aemeasurable) lim
  · rcases u.exists_seq_tendsto with ⟨v, hv⟩
    have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ := fun n =>
      (aestronglyMeasurable_iff_aemeasurable_separable.1 (hf (v n))).2
    choose t t_sep ht using this
    refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩
    filter_upwards [ae_all_iff.2 ht, lim] with x hx h'x
    apply mem_closure_of_tendsto (h'x.comp hv)
    filter_upwards with n using mem_iUnion_of_mem n (hx n)

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
⊢ f = fun x ↦ f hα.some

Tactic:
have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx

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))
⊢ f = fun x ↦ f hα.some
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

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

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ

Tactic:
rw [hfi, add_top]

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∞
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
⊢ Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
· by_cases hxt : x ∈ t
    swap
    · rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]
      exact tendsto_const_nhds
    have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x
    obtain ⟨n₁, hn₁⟩ : ∃ n, ∀ m, n ≤ m → fs m x = f_approx m x := by
      obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
      refine ⟨n, fun m hnm => ?_⟩
      simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]
    rw [tendsto_atTop'] at h ⊢
    intro s hs
    obtain ⟨n₂, hn₂⟩ := h s hs
    refine ⟨max n₁ n₂, fun m hm => ?_⟩
    rw [hn₁ m ((le_max_left _ _).trans hm)]
    exact hn₂ m ((le_max_right _ _).trans hm)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ r * μ (univ ∩ {x | f x = r}) = r * μ {x | f x = r}

Tactic:
Set.univ_inter

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
r : ℝ≥0∞
this : ∀ x ∈ {x | f x = r}, f x = r
⊢ r * μ {x | f x = r} = r * μ {x | f x = r}
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : ¬u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : μ (support g) < ∞
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
x✝ : α
⊢ x✝ ∈ (support g)ᶜ → f x✝ = (fun a ↦ f a - g a) x✝

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ Set.univ ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n

Tactic:
Set.univ_inter

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun p ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ x ∈ C, x ≠ y

Tactic:
by
    have := hC.acc _ yC
    rw [accPt_iff_nhds] at this
    rcases this univ univ_mem with ⟨x, xC, hxy⟩
    exact ⟨x, xC.2, hxy⟩

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

Goal state before:
pp: case refine_2.refine_2
α : 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 : Set α := ⋃ n, T n
⊢ ⋃ i, tᶜ ∪ T i = univ

Tactic:
← Set.union_iUnion tᶜ T

Goal state after:
case refine_2.refine_2
α : 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 : Set α := ⋃ n, T n
⊢ tᶜ ∪ ⋃ i, T i = univ