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

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

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'

Tactic:
· refine mem_iUnion.2 ⟨0, ?_⟩
        simp [hx, hxt]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ ∀ t ∈ ⋃ y, {measurableAtom y}, MeasurableSet t

Tactic:
simp [MeasurableSet.measurableAtom_of_countable]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
⊢ ∀ t ∈ ⋃ y, {measurableAtom y}, MeasurableSet t

Tactic:
by simp [MeasurableSet.measurableAtom_of_countable]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
x : α
⊢ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1

Tactic:
simp [countablyGeneratedAtom]; grind

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : CountablyGenerated α
s : Set α
hs : MeasurableSet s
n : ℕ
x✝ : MeasurableSet (natGeneratingSequence α n)
x : α
hx : x ∈ natGeneratingSequence α n
⊢ (fun x_1 ↦ x ∈ natGeneratingSequence α x_1) n ∧ x ∈ countablyGeneratedAtom α fun x_1 ↦ x ∈ natGeneratingSequence α x_1

Tactic:
simp [countablyGeneratedAtom]; grind

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
hμ : ∀ (a : α), μ {a} < ∞
h✝ : Nonempty α
⊢ SigmaFinite μ

Tactic:
· obtain ⟨f, hf⟩ := exists_surjective_nat α
      exact ⟨⟨⟨fun n ↦ {f n}, by simp, by simpa [hf.forall] using hμ, by simp [hf.range_eq]⟩⟩⟩

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

Goal state before:
pp: α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ False

Tactic:
have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas

Goal state after:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : ℕ → Set α := spanningSets μ
hs_univ : ⋃ i, s i = univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬univ = ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ AEMeasurable f μ

Tactic:
rcases eq_empty_or_nonempty t with rfl | hne
  · obtain rfl : μ = 0 := by simpa using hft
    apply aemeasurable_zero_measure
  · rw [← μ.ae_completion] at hft
    obtain ⟨f', hf'm, hf't, hff'⟩ :
        ∃ f' : α → β, NullMeasurable f' μ ∧ range f' ⊆ t ∧ f =ᵐ[μ] f' :=
      h.measurable'.aemeasurable.exists_ae_eq_range_subset hft hne
    rw [range_subset_iff] at hf't
    lift f' to α → t using hf't
    replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk
    exact (measurable_subtype_coe.comp_aemeasurable hf'm.aemeasurable).congr hff'.symm

Goal state after:
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:
by simpa using measurable_const_smul

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
⊢ Measurable (s.piecewise f g)

Tactic:
refine measurable_of_isOpen fun t ht => ?_
  rw [piecewise_preimage, Set.ite]
  apply MeasurableSet.union
  · rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
    rw [hu]
    exact u_open.measurableSet.inter hs
  · rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
    rw [sdiff_eq_compl_inter, inter_comm, hu]
    exact u_open.measurableSet.inter hs.compl

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ediam (s ∪ t)

Tactic:
intro z hz

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ s
⊢ ∃ y ∈ t, edist z y ≤ ediam (s ∪ t)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ediam (s ∪ t)

Tactic:
intro z hz

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ ediam (s ∪ t)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x z : X
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ

Tactic:
dist_edist,

Goal state after:
δ : ℝ
X : Type u
inst✝ : PseudoMetricSpace X
E : Set X
x z : X
⊢ edist x z < ENNReal.ofReal δ ↔ (edist x z).toReal < δ
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:
dist_edist,

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

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

Tactic:
· apply generateFrom_le
    rintro - ⟨u, v, -, rfl⟩
    borelize α
    exact measurableSet_Ioc

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

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

Tactic:
dist_edist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
h : IsCompact s
hne : s.Nonempty
x y : α
hys : y ∈ s
hy : infEDist x s = edist x y
⊢ (infEDist x s).toReal = (edist x y).toReal
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), thickening ε E

Tactic:
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
  simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
  exact fun _ hε => nonempty_Ioc.mpr hε

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 α
x : α
t : Set α
hxt : {x} ⊆ t
ht1 : MeasurableSet t
ht2 : μ t = 0
⊢ μ (t ∩ s) = 0

Tactic:
apply measure_mono_null inter_subset_left ht2

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((map ENNReal.toNNReal (eapprox f (n + 1) - eapprox f n)) a) = (eapprox f (n + 1)) a

Tactic:
coe_map,

Goal state after:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH : ∑ k ∈ Finset.range (n + 1), ↑((eapproxDiff f k) a) = (eapprox f n) a
⊢ (eapprox f n) a + ↑((ENNReal.toNNReal ∘ ⇑(eapprox f (n + 1) - eapprox f n)) a) = (eapprox f (n + 1)) a
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
⊢ motive g

Tactic:
apply ih

Goal state after:
α : 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 : α →ₛ γ := ⋯
⊢ range ⇑g \ {0} = ↑s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable

Goal state before:
pp: α : 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
⊢ AEMeasurable g μ

Tactic:
set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some

Goal state after:
α : 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
⊢ AEMeasurable g μ
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
⊢ P g

Tactic:
apply ih

Goal state after:
α : 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 : γ := ⋯
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 : α →ₛ γ := ⋯
⊢ range ⇑g \ {c} = ↑s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case e_a.inr
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
x : α
H : f x < ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞

Tactic:
· simp only [H, H.ne, and_true, false_or]

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 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
H : p ∉ s
this : f p = 0
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε

Tactic:
simp [SimpleFunc.piecewise_apply, H, this, hε]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : Countable α
⊢ StronglyMeasurable f

Tactic:
by
  nontriviality α
  obtain ⟨g, hg⟩ := exists_surjective_nat α
  exact ⟨simpleFuncAux f g, hg.forall.2 fun m ↦
    tendsto_nhds_of_eventually_eq simpleFuncAux_eventuallyEq⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n ↦ ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖min 1 (c / ‖(hf.approx n) x‖)‖ * ‖(hf.approx n) x‖ ≤ ‖1‖ * ‖(hf.approx n) x‖

Tactic:
by
        gcongr
        rw [norm_one, Real.norm_of_nonneg]
        · exact min_le_left _ _
        · exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))

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

Goal state before:
pp: α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n ↦ (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ ‖f x‖ ≤ c

Tactic:
exact hfx

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

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

Tactic:
simp only [← iSup_apply]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_4
f : ι → α → ℝ≥0∞
⊢ ⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ i, f i) a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case right
α : 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
⊢ ∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral (μ.restrict s) ≤ ε₂

Tactic:
intro ψ hψ

Goal state after:
case right
α : 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) ≤ ε₂
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))

Tactic:
have : MeasurableSet {x | f x ≠ 0} := ((MeasurableSet.singleton 0).preimage hf.measurable).compl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : GroupWithZero β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | f x ≠ 0}
⊢ Tendsto (fun n ↦ ((fun n ↦ ((hf.approx n).restrict {x | f x ≠ 0})⁻¹) n) x) atTop (𝓝 (f⁻¹ x))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁶ : AddGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : ContinuousAdd E
inst✝¹ : ContinuousNeg E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g - f)

Tactic:
by
  rw [sub_eq_add_neg]
  exact hg.add_stronglyMeasurable hf.neg

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
⊢ ∫⁻ (a : α) in ∅ᶜ, f a ∂μ < ε

Tactic:
simpa [hf₀, pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ

Tactic:
lintegral_congr_ae (hf.ae_eq_mk.fun_add (ae_eq_refl g))

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
⊢ AEMeasurable.mk (F n) ⋯ ≤ᵐ[μ] bound

Tactic:
filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
a : α
H : F n a ≤ bound a
H' : F n a = AEMeasurable.mk (F n) ⋯ a
⊢ AEMeasurable.mk (F n) ⋯ a ≤ bound a
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pcw
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty β
inst✝ : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun x ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f✝ : α → β
hf : StronglyMeasurable f✝
s✝ : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P ⇑f ⋯
Pg : P ⇑g ⋯
⊢ P ⇑(SimpleFunc.piecewise s hs f g) ⋯

Tactic:
simp_rw [SimpleFunc.coe_piecewise]

Goal state after:
case pcw
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Nonempty β
inst✝ : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
const : ∀ (c : β), P (fun x ↦ c) ⋯
pcw :
  ∀ ⦃f g : α → β⦄ {s : Set α} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hs : MeasurableSet s),
    P f hf → P g hg → P (s.piecewise f g) ⋯
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun x_1 ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f✝ : α → β
hf : StronglyMeasurable f✝
s✝ : ℕ → α →ₛ β := hf.approx
n : ℕ
f g : α →ₛ β
s : Set α
hs : MeasurableSet s
Pf : P ⇑f ⋯
Pg : P ⇑g ⋯
⊢ P (s.piecewise ⇑f ⇑g) ⋯
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ Perfect (closure[inst✝¹] (U ∩ C)) ∧ (closure[inst✝¹] (U ∩ C)).Nonempty ∧ closure[inst✝¹] (U ∩ C) ⊆ C

Tactic:
← and_assoc

Goal state after:
case h.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (U ∩ C)) ∧ (closure[inst✝¹] (U ∩ C)).Nonempty) ∧ closure[inst✝¹] (U ∩ C) ⊆ C
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ (Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty ∧ closure[inst✝¹] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))

Tactic:
← and_assoc

Goal state after:
case h.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen[inst✝¹] U
V : Set α
yV : y ∈ V
Vop : IsOpen[inst✝¹] V
hUV : Disjoint (closure[inst✝¹] U) (closure[inst✝¹] V)
⊢ ((Perfect (closure[inst✝¹] (V ∩ C)) ∧ (closure[inst✝¹] (V ∩ C)).Nonempty) ∧ closure[inst✝¹] (V ∩ C) ⊆ C) ∧
    Disjoint (closure[inst✝¹] (U ∩ C)) (closure[inst✝¹] (V ∩ C))