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
𝕜 : Type u_3
inst_3 : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ
h :
  Tendsto.{u_2, u_3} (β := 𝕜) (fun (i : γ) ↦ (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) : 𝕜))
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
tendsto_ofReal_iff'.mp h

Premises used: Filter.tendsto_ofReal_iff', Iff.mp
-- 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 : γ) ↦ (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) : 𝕜)) F
    (𝓝 (↑(∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) : 𝕜))
⊢ Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))

Tactic:
exact tendsto_ofReal_iff'.mp h

Premises used: Filter.tendsto_ofReal_iff', Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ ContinuousAdd.{u_1} (FiniteMeasure Ω)

Tactic:
⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩

Premises used: Iff.mpr, ContinuousAdd.mk, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
refine :
  ∀ (p : FiniteMeasure Ω × FiniteMeasure Ω),
    ContinuousAt (Y := FiniteMeasure Ω) (fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p
⊢ ContinuousAdd.{u_1} (FiniteMeasure Ω)

Tactic:
refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
apply :
  ∀ (g : Ω →ᵇ ℝ≥0),
    Tendsto
      (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦
        ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(i.1 + i.2) : Measure Ω))
      (𝓝 p)
      (𝓝
        (∫⁻ (x : Ω),
          (↑((g : (a : Ω) → ℝ≥0) x) :
            ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω)))
⊢ ContinuousAt (Y := FiniteMeasure Ω) (fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p

Tactic:
apply tendsto_iff_forall_lintegral_tendsto.2 (fun g ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
rw :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))

Tactic:
(tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_fst

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))

Tactic:
exact (tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_fst

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))

Tactic:
have A : Tendsto (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ x, g x ∂i.1) (𝓝 p)
      (𝓝 (∫⁻ x, g x ∂p.1)) := by
    rw [nhds_prod_eq]
    exact (tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
rw :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))

Tactic:
(tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_snd

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))

Tactic:
exact (tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_snd

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))

Tactic:
have B : Tendsto (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ x, g x ∂i.2) (𝓝 p)
      (𝓝 (∫⁻ x, g x ∂p.2)) := by
    rw [nhds_prod_eq]
    exact (tendsto_iff_forall_lintegral_tendsto.1 tendsto_id g).comp tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
B :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))
⊢ Tendsto
    (fun (x : FiniteMeasure Ω × FiniteMeasure Ω) ↦
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑x.1 : Measure Ω) +
        ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑x.2 : Measure Ω))
    (𝓝 p)
    (𝓝
      (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω) +
        ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))

Tactic:
A.add B

Premises used: Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
B :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))
h :
  ∀ (q : FiniteMeasure Ω × FiniteMeasure Ω),
    ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(q.1 + q.2) : Measure Ω) =
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑q.1 : Measure Ω) +
        ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑q.2 : Measure Ω)
h₁ :
  ∫⁻ (x : Ω),
      (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω) =
    ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω) +
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)
⊢ Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(i.1 + i.2) : Measure Ω))
    (𝓝 p)
    (𝓝
      (∫⁻ (x : Ω),
        (↑((g : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω)))

Tactic:
convert! A.add B with q

Premises used: Filter.Tendsto.add
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
B :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))
q : FiniteMeasure Ω × FiniteMeasure Ω
⊢ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(q.1 + q.2) : Measure Ω) =
    ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑q.1 : Measure Ω) +
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑q.2 : Measure Ω)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
g : Ω →ᵇ ℝ≥0
A :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.1 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω)))
B :
  Tendsto
    (fun (i : FiniteMeasure Ω × FiniteMeasure Ω) ↦ ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑i.2 : Measure Ω))
    (𝓝 p) (𝓝 (∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)))
⊢ ∫⁻ (x : Ω),
      (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω) =
    ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.1 : Measure Ω) +
      ∫⁻ (x : Ω), (↑((g : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑p.2 : Measure Ω)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ ContinuousSMul.{0, u_1} ℝ≥0 (FiniteMeasure Ω)

Tactic:
⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩

Premises used: Iff.mpr, ContinuousSMul.mk, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
refine :
  ∀ (p : ℝ≥0 × FiniteMeasure Ω), ContinuousAt (Y := FiniteMeasure Ω) (fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p
⊢ ContinuousSMul.{0, u_1} ℝ≥0 (FiniteMeasure Ω)

Tactic:
refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
apply :
  ∀ (g : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑(i.1 • i.2) : Measure Ω))
      (𝓝 p)
      (𝓝
        (@integral _ _ _ _ inst (↑((fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p) : Measure Ω) fun (x : Ω) ↦
          (g : (a : Ω) → ℝ) x))
⊢ ContinuousAt (Y := FiniteMeasure Ω) (fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p

Tactic:
apply tendsto_iff_forall_integral_tendsto.2 (fun g ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
rw : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 p.1)
⊢ Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
⊢ Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 p.1)

Tactic:
tendsto_fst

Premises used: Filter.tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
⊢ Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 p.1)

Tactic:
exact tendsto_fst

Premises used: Filter.tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
⊢ Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)

Tactic:
have A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 (p.1)) := by
    rw [nhds_prod_eq]
    exact tendsto_fst
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
rw :
  Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
⊢ Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
⊢ Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))

Tactic:
(tendsto_iff_forall_integral_tendsto.1 tendsto_id g).comp tendsto_snd

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
⊢ Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω))
    (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))

Tactic:
exact (tendsto_iff_forall_integral_tendsto.1 tendsto_id g).comp tendsto_snd

Premises used: Filter.tendsto_id, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
⊢ Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))

Tactic:
have B : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ x, g x ∂i.2) (𝓝 p)
      (𝓝 (∫ x, g x ∂p.2)) := by
    rw [nhds_prod_eq]
    exact (tendsto_iff_forall_integral_tendsto.1 tendsto_id g).comp tendsto_snd
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
B :
  Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
⊢ Tendsto
    (fun (x : ℝ≥0 × FiniteMeasure Ω) ↦ HSMul.hSMul (β := ℝ) x.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑x.2 : Measure Ω)))
    (𝓝 p) (𝓝 (HSMul.hSMul (β := ℝ) p.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω))))

Tactic:
A.smul B

Premises used: Filter.Tendsto.smul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
B :
  Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
h :
  ∀ (q : ℝ≥0 × FiniteMeasure Ω),
    ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑(q.1 • q.2) : Measure Ω) =
      HSMul.hSMul (β := ℝ) q.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑q.2 : Measure Ω))
h₁ :
  (@integral _ _ _ _ inst (↑((fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p) : Measure Ω) fun (x : Ω) ↦
      (g : (a : Ω) → ℝ) x) =
    HSMul.hSMul (β := ℝ) p.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω))
⊢ Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑(i.1 • i.2) : Measure Ω)) (𝓝 p)
    (𝓝
      (@integral _ _ _ _ inst (↑((fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p) : Measure Ω) fun (x : Ω) ↦
        (g : (a : Ω) → ℝ) x))

Tactic:
convert! A.smul B with q

Premises used: Filter.Tendsto.smul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
B :
  Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
q : ℝ≥0 × FiniteMeasure Ω
⊢ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑(q.1 • q.2) : Measure Ω) =
    HSMul.hSMul (β := ℝ) q.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑q.2 : Measure Ω))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
g : Ω →ᵇ ℝ
A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 p.1)
B :
  Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p)
    (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
⊢ (@integral _ _ _ _ inst (↑((fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p) : Measure Ω) fun (x : Ω) ↦
      (g : (a : Ω) → ℝ) x) =
    HSMul.hSMul (β := ℝ) p.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → FiniteMeasure Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Continuous[inst_3, _] fun (x : X) ↦ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑(μs x) : Measure Ω)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_lintegral_tendsto,
    forall_comm (α := X)]

Premises used: ContinuousAt, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, forall_comm, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
X : Type u_2
inst_3 : TopologicalSpace X
μs : X → FiniteMeasure Ω
⊢ Continuous[inst_3, instTopologicalSpace] μs ↔
    ∀ (f : Ω →ᵇ ℝ), Continuous[inst_3, _] fun (x : X) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs x) : Measure Ω)

Tactic:
simp [continuous_iff_continuousAt, ContinuousAt, tendsto_iff_forall_integral_tendsto,
    forall_comm (α := X)]

Premises used: ContinuousAt, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, forall_comm, continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure X) ↦
    ∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure X)

Tactic:
continuous_iff_forall_continuous_lintegral.1 continuous_id _

Premises used: MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_lintegral, continuous_id, Iff.mp