awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
⊢ SigmaFinite (μ.restrict t)

Tactic:
⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩

Premises used: trivial, Compl.compl, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, Union.union, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
refine_2 :
  ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ tᶜ ∪ T n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ tᶜ ∪ T n) i) univ
⊢ SigmaFinite (μ.restrict t)

Tactic:
refine ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
n : ℕ
refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (T n ∩ ⋃ (b : ℕ), T b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ tᶜ ∪ T n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply' (MeasurableSet.iUnion hT_meas), Set.union_inter_distrib_right,
        Set.compl_inter_self t, Set.empty_union]

Premises used: Set.empty_union, MeasurableSet.iUnion, Set.compl_inter_self, Set.union_inter_distrib_right, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (T n ∩ ⋃ (b : ℕ), T b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.inter_subset_left).trans_lt (hT_lt_top n)

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (T n ∩ ⋃ (b : ℕ), T b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono Set.inter_subset_left).trans_lt (hT_lt_top n)

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
refine_2 : tᶜ ∪ ⋃ (i : ℕ), T i = univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ tᶜ ∪ T n) i) univ

Tactic:
rw [← Set.union_iUnion tᶜ T]

Premises used: Compl.compl, Set.union_iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
⊢ tᶜ ∪ ⋃ (i : ℕ), T i = univ

Tactic:
Set.compl_union_self _

Premises used: Set.compl_union_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
⊢ tᶜ ∪ ⋃ (i : ℕ), T i = univ

Tactic:
exact Set.compl_union_self _

Premises used: Set.compl_union_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
hf : FinStronglyMeasurable f μ
⊢ Measurable f

Tactic:
hf.stronglyMeasurable.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.FinStronglyMeasurable.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f * g) μ

Tactic:
⟨fun n => hf.approx n * hg.approx n, ?_, fun x =>
      (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩

Premises used: HMul.hMul, MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, Filter.Tendsto.mul, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n * hg.approx n) n) : (a : α) → β)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable (f * g) μ

Tactic:
refine
    ⟨fun n => hf.approx n * hg.approx n, ?_, fun x =>
      (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n * hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

Premises used: Function.support_mul_subset_left, MeasureTheory.measure_mono, MeasureTheory.FinStronglyMeasurable.fin_support_approx, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n * hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono (support_mul_subset_left _ _)).trans_lt (hf.fin_support_approx n)

Premises used: Function.support_mul_subset_left, MeasureTheory.measure_mono, MeasureTheory.FinStronglyMeasurable.fin_support_approx, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : AddZeroClass β
inst_2 : ContinuousAdd β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f + g) μ

Tactic:
⟨fun n => hf.approx n + hg.approx n, fun n =>
    (measure_mono (Function.support_add _ _)).trans_lt
      ((measure_union_le _ _).trans_lt
        (ENNReal.add_lt_top.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩)),
    fun x => (hf.tendsto_approx x).add (hg.tendsto_approx x)⟩

Premises used: Iff.mpr, MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, Function.support_add, HAdd.hAdd, Function.support, And.intro, MeasureTheory.measure_mono, Filter.Tendsto.add, Exists.intro, MeasureTheory.FinStronglyMeasurable, MeasureTheory.FinStronglyMeasurable.fin_support_approx, ENNReal.add_lt_top, LE.le.trans_lt, DFunLike.coe, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (-f) μ

Tactic:
⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩

Premises used: Filter.Tendsto.neg, MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
refine :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ -hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable (-f) μ

Tactic:
refine ⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
this :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
this
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
this :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ -hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
convert! this
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
suffices :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ -hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
suffices μ (Function.support fun x ↦ -(hf.approx n) x) < ∞ by convert! this
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
rw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [Function.support_fun_neg (hf.approx n)]

Premises used: MeasureTheory.FinStronglyMeasurable.approx, Function.support_fun_neg, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
hf.fin_support_approx n

Premises used: MeasureTheory.FinStronglyMeasurable.fin_support_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact hf.fin_support_approx n

Premises used: MeasureTheory.FinStronglyMeasurable.fin_support_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousSub β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f - g) μ

Tactic:
⟨fun n => hf.approx n - hg.approx n, fun n =>
    (measure_mono (Function.support_sub _ _)).trans_lt
      ((measure_union_le _ _).trans_lt
        (ENNReal.add_lt_top.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩)),
    fun x => (hf.tendsto_approx x).sub (hg.tendsto_approx x)⟩

Premises used: Iff.mpr, Function.support_sub, MeasureTheory.FinStronglyMeasurable.tendsto_approx, HSub.hSub, MeasureTheory.FinStronglyMeasurable.approx, Function.support, And.intro, MeasureTheory.measure_mono, Exists.intro, MeasureTheory.FinStronglyMeasurable, MeasureTheory.FinStronglyMeasurable.fin_support_approx, ENNReal.add_lt_top, Filter.Tendsto.sub, LE.le.trans_lt, DFunLike.coe, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩

Premises used: MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, Filter.Tendsto.const_smul, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
refine :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ c • hf.approx n) n) : (a : α) → β)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
rw :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support (HSMul.hSMul (β := (a : α) → β) c (⇑(hf.approx n) : (a : α) → β))) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ c • hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [SimpleFunc.coe_smul]

Premises used: MeasureTheory.SimpleFunc.coe_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support (HSMul.hSMul (β := (a : α) → β) c (⇑(hf.approx n) : (a : α) → β))) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

Premises used: Function.support_const_smul_subset, MeasureTheory.measure_mono, MeasureTheory.FinStronglyMeasurable.fin_support_approx, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support (HSMul.hSMul (β := (a : α) → β) c (⇑(hf.approx n) : (a : α) → β))) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

Premises used: Function.support_const_smul_subset, MeasureTheory.measure_mono, MeasureTheory.FinStronglyMeasurable.fin_support_approx, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊔ g) μ

Tactic:
⟨fun n => hf.approx n ⊔ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩

Premises used: MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, Filter.Tendsto.sup_nhds, Max.max, And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊔ hg.approx n) n) : (a : α) → β)) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable (f ⊔ g) μ

Tactic:
refine
    ⟨fun n => hf.approx n ⊔ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊔ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(measure_mono (support_sup _ _)).trans_lt ?_

Premises used: Function.support_sup, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
refine :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊔ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine (measure_mono (support_sup _ _)).trans_lt ?_

Premises used: Function.support_sup, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β) ∪
          support.{u_1, u_2} (M := β) (⇑(hg.approx n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Premises used: Iff.mpr, MeasureTheory.measure_union_lt_top_iff, And.intro, MeasureTheory.FinStronglyMeasurable.fin_support_approx