awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
⊢ Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)

Tactic:
have tends_neg := (ENNReal.tendsto_toReal (f_neg.lintegral_lt_top_of_nnreal μ).ne).comp (h f_neg)
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
⊢ ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal

Tactic:
have aux :
    ∀ g : Ω →ᵇ ℝ≥0,
      (ENNReal.toReal ∘ fun i : γ ↦ ∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)) =
        fun i : γ ↦ (∫⁻ x : Ω, ↑(g x) ∂(μs i : Measure Ω)).toReal :=
    fun _ ↦ rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))

Tactic:
simp_rw [aux, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral] at tends_pos tends_neg

Premises used: BoundedContinuousFunction.toReal_lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
tends_pos :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
tends_neg :
  Tendsto (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
tends_pos₁ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))

Tactic:
simp_rw [aux, BoundedContinuousFunction.toReal_lintegral_coe_eq_integral] at tends_pos tends_neg

Premises used: BoundedContinuousFunction.toReal_lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
tends_pos :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
tends_neg :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
⊢ Tendsto
    (fun (i : γ) ↦
      HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
        (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
    F
    (𝓝
      (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
        (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))

Tactic:
Tendsto.sub tends_pos tends_neg

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart
_def_f_pos : f_pos = f.nnrealPart
f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart
_def_f_neg : f_neg = (-f).nnrealPart
aux :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Eq.{u_2 + 1} (α := γ → ℝ)
      (ENNReal.toReal ∘ fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω))
      fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toReal
tends_pos :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
tends_neg :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω)))
⊢ Tendsto
    (fun (i : γ) ↦
      HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω))
        (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑(μs i) : Measure Ω)))
    F
    (𝓝
      (HSub.hSub (α := ℝ) (∫ (x : Ω), (↑((f_pos : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
        (∫ (x : Ω), (↑((f_neg : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))))

Tactic:
exact Tendsto.sub tends_pos tends_neg

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
rw :
  (∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))

Tactic:
rw [tendsto_iff_forall_integral_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))

Tactic:
⟨fun h f ↦ ?_, fun h f ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
refine_1 :
  ∀
    (h :
      ∀ (f : Ω →ᵇ ℝ),
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
          (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))))
    (f : Ω →ᵇ 𝕜),
    Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
refine_2 :
  ∀
    (h :
      ∀ (f : Ω →ᵇ 𝕜),
        Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
          (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω))))
    (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))) ↔
    ∀ (f : Ω →ᵇ 𝕜),
      Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))

Tactic:
refine ⟨fun h f ↦ ?_, fun h f ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
refine_1 :
  Tendsto (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝
      ((↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
          RCLike.I))
⊢ Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))

Tactic:
rw [← integral_re_add_im (integrable μ f)]

Premises used: BoundedContinuousFunction.integrable, integral_re_add_im
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
refine_1 :
  Tendsto
    (fun (i : γ) ↦
      (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜)
          (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) RCLike.I)
    F
    (𝓝
      ((↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
          RCLike.I))
⊢ Tendsto (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝
      ((↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
          RCLike.I))

Tactic:
simp_rw [← integral_re_add_im (integrable (μs _) f)]

Premises used: BoundedContinuousFunction.integrable, integral_re_add_im
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
⊢ Tendsto
    (fun (i : γ) ↦
      (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜)
          (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) RCLike.I)
    F
    (𝓝
      ((↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
          RCLike.I))

Tactic:
Tendsto.add ?_ ?_

Premises used: Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
refine_1 :
  Tendsto.{u_2, u_3} (β := 𝕜)
    (fun (i : γ) ↦ (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜))
refine_1₁ :
  Tendsto
    (fun (i : γ) ↦
      HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)
        RCLike.I)
    F
    (𝓝
      (HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
        RCLike.I))
⊢ Tendsto
    (fun (i : γ) ↦
      (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜)
          (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜) RCLike.I)
    F
    (𝓝
      ((↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜) +
        HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
          RCLike.I))

Tactic:
refine Tendsto.add ?_ ?_

Premises used: Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
⊢ Tendsto.{u_2, u_3} (β := 𝕜)
    (fun (i : γ) ↦ (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜))

Tactic:
(RCLike.continuous_ofReal.tendsto _).comp (h (f.comp RCLike.re RCLike.lipschitzWith_re))

Premises used: BoundedContinuousFunction.comp, RCLike.continuous_ofReal, RCLike.lipschitzWith_re, Continuous.tendsto, RCLike.re, Filter.Tendsto.comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
⊢ Tendsto.{u_2, u_3} (β := 𝕜)
    (fun (i : γ) ↦ (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (RCLike.re : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜))

Tactic:
exact (RCLike.continuous_ofReal.tendsto _).comp (h (f.comp RCLike.re RCLike.lipschitzWith_re))

Premises used: BoundedContinuousFunction.comp, RCLike.continuous_ofReal, RCLike.lipschitzWith_re, Continuous.tendsto, RCLike.re, Filter.Tendsto.comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
⊢ Tendsto
    (fun (i : γ) ↦
      HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)
        RCLike.I)
    F
    (𝓝
      (HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
        RCLike.I))

Tactic:
(Tendsto.comp (RCLike.continuous_ofReal.tendsto _)
        (h (f.comp RCLike.im RCLike.lipschitzWith_im))).mul_const _

Premises used: BoundedContinuousFunction.comp, Filter.Tendsto.mul_const, RCLike.im, RCLike.continuous_ofReal, Continuous.tendsto, Filter.Tendsto.comp, DFunLike.coe, RCLike.lipschitzWith_im
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ 𝕜
⊢ Tendsto
    (fun (i : γ) ↦
      HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑(μs i) : Measure Ω)) : 𝕜)
        RCLike.I)
    F
    (𝓝
      (HMul.hMul (α := 𝕜) (↑(∫ (x : Ω), (RCLike.im : (a : 𝕜) → ℝ) ((f : (a : Ω) → 𝕜) x : 𝕜) ∂(↑μ : Measure Ω)) : 𝕜)
        RCLike.I))

Tactic:
exact (Tendsto.comp (RCLike.continuous_ofReal.tendsto _)
        (h (f.comp RCLike.im RCLike.lipschitzWith_im))).mul_const _

Premises used: BoundedContinuousFunction.comp, Filter.Tendsto.mul_const, RCLike.im, RCLike.continuous_ofReal, Continuous.tendsto, Filter.Tendsto.comp, DFunLike.coe, RCLike.lipschitzWith_im
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ 𝕜),
    Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ
⊢ Tendsto.{u_2, u_3} (β := 𝕜)
    (fun (i : γ) ↦
      ∫ (ω : Ω),
        (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) ⋯ : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
            (a : Ω) → 𝕜)
          ω ∂(↑(μs i) : Measure Ω))
    F
    (𝓝
      (∫ (ω : Ω),
        (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) ⋯ : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
            (a : Ω) → 𝕜)
          ω ∂(↑μ : Measure Ω)))

Tactic:
specialize h ((RCLike.ofRealAm (K := 𝕜)).compLeftContinuousBounded ℝ
      RCLike.lipschitzWith_ofReal f)

Premises used: Real, RCLike.ofRealAm, RCLike.lipschitzWith_ofReal, BoundedContinuousFunction.AlgHom.compLeftContinuousBounded, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ
h :
  Tendsto.{u_2, u_3} (β := 𝕜)
    (fun (i : γ) ↦
      ∫ (ω : Ω),
        (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) ⋯ : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
            (a : Ω) → 𝕜)
          ω ∂(↑(μs i) : Measure Ω))
    F
    (𝓝
      (∫ (ω : Ω),
        (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) ⋯ : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
            (a : Ω) → 𝕜)
          ω ∂(↑μ : Measure Ω)))
⊢ Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) : 𝕜))

Tactic:
simp only [AlgHom.compLeftContinuousBounded_apply_apply, RCLike.ofRealAm_coe,
      integral_ofReal] at h

Premises used: BoundedContinuousFunction.AlgHom.compLeftContinuousBounded_apply_apply, integral_ofReal, RCLike.ofRealAm_coe