awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
⊢ (∀ (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 Ω)))
have 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 Ω)))
Tactic: refine ⟨fun h f ↦ ?_, fun h f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 : γ) ↦ ∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → 𝕜) ω ∂(↑μ : Measure Ω)))
have 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))
Tactic: rw [← integral_re_add_im (integrable μ f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 : γ) ↦ ∫ (ω : Ω), (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))
have 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))
Tactic: simp_rw [← integral_re_add_im (integrable (μs _) f)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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))
have 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 Ω)) : 𝕜))
Tactic: refine Tendsto.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)) : 𝕜))
⊢ 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))
have 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))
Tactic: refine Tendsto.add ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
have h₁ : Tendsto.{u_2, u_3} (β := 𝕜)
  (fun (i : γ) ↦
    ∫ (ω : Ω),
      (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) sorry : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
          (a : Ω) → 𝕜)
        ω ∂(↑(μs i) : Measure Ω))
  F
  (𝓝
    (∫ (ω : Ω),
      (((AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm (C := 1) sorry : (a : Ω →ᵇ ℝ) → Ω →ᵇ 𝕜) f : Ω →ᵇ 𝕜) :
          (a : Ω) → 𝕜)
        ω ∂(↑μ : Measure Ω)))
Tactic: specialize h ((RCLike.ofRealAm (K := 𝕜)).compLeftContinuousBounded ℝ
      RCLike.lipschitzWith_ofReal f)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ ContinuousAdd.{u_1} (FiniteMeasure Ω)
have refine : ∀ (p : FiniteMeasure Ω × FiniteMeasure Ω),
  ContinuousAt (Y := FiniteMeasure Ω) (fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p
Tactic: refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : FiniteMeasure Ω × FiniteMeasure Ω
⊢ ContinuousAt (Y := FiniteMeasure Ω) (fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p
have 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 Ω)))
Tactic: apply tendsto_iff_forall_lintegral_tendsto.2 (fun g ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
have 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 Ω)))
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 + i.2) : Measure Ω))
    (𝓝 p)
    (𝓝
      (∫⁻ (x : Ω),
        (↑((g : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω)))
have 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 Ω)))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
have 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 Ω)))
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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.1 + i.2) : Measure Ω))
    (𝓝 p)
    (𝓝
      (∫⁻ (x : Ω),
        (↑((g : (a : Ω) → ℝ≥0) x) :
          ℝ≥0∞) ∂(↑((fun (p : FiniteMeasure Ω × FiniteMeasure Ω) ↦ p.1 + p.2) p) : Measure Ω)))
have 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 Ω)))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 (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 Ω)))
have 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 Ω)
Tactic: convert! A.add B with q
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)
⊢ 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 Ω)))
have 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 Ω)
Tactic: convert! A.add B with q
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ ContinuousSMul.{0, u_1} ℝ≥0 (FiniteMeasure Ω)
have refine : ∀ (p : ℝ≥0 × FiniteMeasure Ω), ContinuousAt (Y := FiniteMeasure Ω) (fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p
Tactic: refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
⊢ ContinuousAt (Y := FiniteMeasure Ω) (fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p
have 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))
Tactic: apply tendsto_iff_forall_integral_tendsto.2 (fun g ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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)
have rw : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p.1 ×ˢ 𝓝 p.2) (𝓝 p.1)
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
p : ℝ≥0 × FiniteMeasure Ω
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))
have A : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω)))
have rw : Tendsto (β := ℝ) (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑i.2 : Measure Ω)) (𝓝 p.1 ×ˢ 𝓝 p.2)
  (𝓝 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑p.2 : Measure Ω)))
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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.1 • i.2) : Measure Ω)) (𝓝 p)
    (𝓝
      (@integral _ _ _ _ inst (↑((fun (p : ℝ≥0 × FiniteMeasure Ω) ↦ p.1 • p.2) p) : Measure Ω) fun (x : Ω) ↦
        (g : (a : Ω) → ℝ) x))
have B : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 (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))
have h : ∀ (q : ℝ≥0 × FiniteMeasure Ω),
  ∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑(q.1 • q.2) : Measure Ω) =
    HSMul.hSMul (β := ℝ) q.1 (∫ (x : Ω), (g : (a : Ω) → ℝ) x ∂(↑q.2 : Measure Ω))
Tactic: convert! A.smul B with q
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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 Ω))
⊢ 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))
have 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 Ω))
Tactic: convert! A.smul B with q
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
inst : MeasurableSpace Ω
inst_1 : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ mass (comap f μ) ≤ μ.mass
have simp : LE.le (α := ℝ≥0∞) (((Measure.comap f (↑μ : Measure Ω') : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
  (((↑μ : Measure Ω') : (a : Set Ω') → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp only [mass, comap, mk_apply, coeFn_def, ne_eq, measure_ne_top, not_false_eq_true,
    ENNReal.toNNReal_le_toNNReal]