mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto (fun n ↦ ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto (fun n ↦ ((fun n ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case refine_2
α : 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
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ i,
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ

Tactic:
]

Goal state after:
case refine_2
α : 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
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ i,
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
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
this :
  ⋃ n,
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν
⊢ Set.univ = Set.univ

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * (μ.trim hm) s = c * μ s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ c * (μ.trim hm) s = c * μ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : (μ.trim hm) s = μ s
⊢ c * μ s = c * μ s

Tactic:
]

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 : ℕ
⊢ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h_trim_s : (μ.trim hm) s = μ s
⊢ c * (μ.trim hm) s = c * μ s

Tactic:
by rw [h_trim_s]

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

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.trim hm) s = μ s

Tactic:
exact trim_measurableSet_eq hm hs

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν) + ν s

pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ Disjoint (μ.sigmaFiniteSetWRT' ν) s

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν) + ν s

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
⊢ Disjoint (μ.sigmaFiniteSetWRT' ν) s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a + g a ∂μ
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a + g a ∂μ
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ

Tactic:
]

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun x ↦ ⨆ n, f n x) a ∂μ
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
⊢ f ↑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:
]

Goal state after:
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.Integral.Lebesgue.Add

Goal state before:
pp: case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
]

Goal state after:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ ⨆ n, ∫⁻ (a : α), f n a ∂μ.trim hm = ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t = ∞

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t = ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm

pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.restrict s).trim hm)

Tactic:
]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.restrict s).trim hm)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α) in s, f a ∂μ.trim hm

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.trim hm).restrict s)

Tactic:
]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.trim hm).restrict s)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ μ {a | ¬f a ≤ g a} = 0

pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a ≤ g a}

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ μ {a | ¬f a ≤ g a} = 0

α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝³ : TopologicalSpace E
inst✝² : Preorder E
inst✝¹ : OrderClosedTopology E
inst✝ : PseudoMetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f ≤ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a ≤ g a}
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ μ {a | ¬f a = g a} = 0

pp: α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Tactic:
]

Goal state after:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ μ {a | ¬f a = g a} = 0

α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᵐ[μ] g
⊢ MeasurableSet {a | ¬f a = g a}
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
⊢ U ∈ 𝓝[≠] x
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
x : α
U : Set α
h_acc : AccPt x (𝓟 C)
hU : U ∈ 𝓝 x
this : 𝓝[≠] x ≤ 𝓟 U
⊢ (𝓝[≠] x ⊓ 𝓟 C).NeBot
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞
hs_subset : s ⊆ h.chooseᶜ
⊢ μ s = ∞

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞
hs_subset : s ⊆ h.chooseᶜ
⊢ μ s = ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case refine_5.hf
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l

Tactic:
]

Goal state after:
case refine_5.hf
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ (b : ℕ), a ≤ b → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), k ≤ b → x b ∈ {x | (fun n ↦ AEMeasurable (F n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n ↦ F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n
hs_univ : ⋃ i, s i = univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ ↑n
⊢ ↑‖f x‖₊ ≤ ↑n

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ (μ.trim hm) (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ ↑n
hs_univ : ⋃ i, s i = univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ ↑n
⊢ ↑‖f x‖₊ ≤ ↑n
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Tactic:
]

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ¬ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ ∞ = ∞

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ closure[inst✝] C
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_absurd : Tendsto (fun i ↦ f i a) atTop atTop
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
tendsto_atTop_atTop_iff_of_monotone h_mono

Goal state after:
case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)

Tactic:
]

Goal state after:
case inl
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone fun i ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
⊢ ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ {a | ClusterPt a (𝓟 C)}
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
C : Set α
hC : Preperfect C
x : α
hx : x ∈ {a | ClusterPt a (𝓟 C)}
h : x ∉ C
this : {x}ᶜ ∩ C = C
⊢ (𝓝 x ⊓ 𝓟 C).NeBot
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)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
x : α
hxt : ∀ (x_1 : ℕ), x ∉ T x_1
⊢ (fs n) x = 0

Tactic:
]

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 : Set α := ⋃ n, T n
n : ℕ
x : α
hxt : ∀ (x_1 : ℕ), x ∉ T x_1
⊢ (fs n) x = 0