awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω)))
      atTop (𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ))
have h : ∀ (ω : Ω)
  (hωφ :
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ)))
  (hωψ :
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))),
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ))
Tactic: filter_upwards [hφ, hψ] with ω hωφ hωψ
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
⊢ Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ))
have h : Eq.{u_2 + 1} (α := ℕ → E)
  (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω)))
  fun (x : ℕ) ↦
  HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, (φ : (a : E) → E) (X i ω)) +
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, (ψ : (a : E) → E) (X i ω))
Tactic: convert! hωφ.add hωψ using 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
h :
  Eq.{u_2 + 1} (α := ℕ → E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω)))
    fun (x : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, (φ : (a : E) → E) (X i ω)) +
      HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ Finset.range x, (ψ : (a : E) → E) (X i ω))
⊢ Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ + ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ))
have h₁ : 𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ) =
  𝓝 (HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
Tactic: convert! hωφ.add hωψ using 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
⊢ 𝓝 (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ) =
    𝓝 (HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
have h : ∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ =
  HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
⊢ ∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ)
  (∫ (a : Ω), HAdd.hAdd (α := E) (((⇑φ : (a : E) → E) ∘ X 0) a) (((⇑ψ : (a : E) → E) ∘ X 0) a) ∂μ)
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
h :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ)
    (∫ (a : Ω), HAdd.hAdd (α := E) (((⇑φ : (a : E) → E) ∘ X 0) a) (((⇑ψ : (a : E) → E) ∘ X 0) a) ∂μ)
⊢ ∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)
have h₁ : Integrable (ε := E) ((⇑φ : (a : E) → E) ∘ X 0) μ
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ_1 φ ψ : SimpleFunc E E
hφ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hψ :
  ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
ω : Ω
hωφ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
hωψ :
  Tendsto.{0, u_2} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω))) atTop
    (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ))
h :
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ)
    (∫ (a : Ω), HAdd.hAdd (α := E) (((⇑φ : (a : E) → E) ∘ X 0) a) (((⇑ψ : (a : E) → E) ∘ X 0) a) ∂μ)
h₁ : Integrable (ε := E) ((⇑φ : (a : E) → E) ∘ X 0) μ
⊢ ∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)
have h₂ : Integrable (ε := E) ((⇑ψ : (a : E) → E) ∘ X 0) μ
Tactic: rw [← integral_add]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E)
      (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (φ : (a : E) → E) (X i ω))) atTop
      (𝓝 (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ))
have refine_1 : ∀ (c : E) {s : Set E} (hs : MeasurableSet s),
  (fun (ψ : SimpleFunc E E) ↦
      ∀ᵐ (ω : Ω) ∂μ,
        Tendsto.{0, u_2} (β := E)
          (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, (ψ : (a : E) → E) (X i ω)))
          atTop (𝓝 (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))
    (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0))
Tactic: classical
  refine SimpleFunc.induction (motive := fun ψ ↦ ∀ᵐ ω ∂μ,
    Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, ψ (X i ω))) atTop (𝓝 μ[ψ ∘ (X 0)])) ?_ ?_ φ
  · intro c s hs
    simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, piecewise_eq_indicator, Function.comp_apply]
    let F : E → ℝ := indicator s 1
    have F_meas : Measurable F := (measurable_indicator_const_iff 1).2 hs
    let Y : ℕ → Ω → ℝ := fun n ↦ F ∘ (X n)
    have : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (n : ℕ) ↦ (n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, Y i ω)
        atTop (𝓝 μ[Y 0]) := by
      simp only [smul_eq_mul, ← div_eq_inv_mul]
      apply strong_law_ae_real
      · exact SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')
      · exact fun i j hij ↦ IndepFun.comp (hindep hij) F_meas F_meas
      · exact fun i ↦ (hident i).comp F_meas
    filter_upwards [this] with ω hω
    have I : indicator s (Function.const E c) = (fun x ↦ (indicator s (1 : E → ℝ) x) • c) := by
      ext
      rw [← indicator_smul_const_apply]
      congr! 1
      ext
      simp
    simp only [I, integral_smul_const]
    convert! Tendsto.smul_const hω c using 1
    simp [F, Y, ← sum_smul, smul_smul]
  · rintro φ ψ - hφ hψ
    filter_upwards [hφ, hψ] with ω hωφ hωψ
    convert! hωφ.add hωψ using 1
    · simp [sum_add_distrib]
    · congr 1
      rw [← integral_add]
      · rfl
      · exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure
      · exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have zero_s : 0 ∈ s
Tactic: have zero_s : 0 ∈ s := by simp [s]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have this : SeparableSpace.{u_2} (↑s : Type u_2)
Tactic: have : SeparableSpace s := h'.separableSpace_range_union_singleton
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this : SeparableSpace.{u_2} (↑s : Type u_2)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have this₁ : Nonempty.{u_2 + 1} (↑s : Type u_2)
Tactic: have : Nonempty s := ⟨0, zero_s⟩
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, X i ω))
      atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
have A : ∀ᵐ (ω : Ω) ∂μ,
  ∀ (k : ℕ),
    Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
      atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
Tactic: have A : ∀ᵐ ω ∂μ, ∀ k,
      Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • (∑ i ∈ range n, Y k i ω)) atTop (𝓝 μ[Y k 0]) :=
    ae_all_iff.2 (fun k ↦ strong_law_ae_simpleFunc_comp X h'.measurable hindep hident (φ k))
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) (↑n : ℝ)) atTop
        (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
have apply : ∀ (k : ℕ),
  ∀ᵐ (a : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
Tactic: apply ae_all_iff.2 (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun (k : ℕ) (x : E) ↦ ‖HSub.hSub (β := E) x ((φ k : (a : E) → E) x : E)‖
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
have G_meas : ∀ (k : ℕ), Measurable (G k)
Tactic: have G_meas : ∀ k, Measurable (G k) :=
      fun k ↦ (measurable_id.sub_stronglyMeasurable (φ k).stronglyMeasurable).norm
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this_1 : SeparableSpace.{u_2} (↑s : Type u_2)
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
φ : ℕ → SimpleFunc E E :=
  SimpleFunc.nearestPt fun (k : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ E) k 0
      (Function.comp (β := (↑s : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (denseSeq (↑s : Type u_2)))
Y : ℕ → ℕ → Ω → E := fun (k i : ℕ) ↦ (⇑(φ k) : (a : E) → E) ∘ X i
A :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, Y k i ω))
        atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun (k : ℕ) (x : E) ↦ ‖HSub.hSub (β := E) x ((φ k : (a : E) → E) x : E)‖
G_meas : ∀ (k : ℕ), Measurable (G k)
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) (↑n : ℝ)) atTop
      (𝓝 (∫ (x : Ω), (fun (ω : Ω) ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
have I : ∀ (k i : ℕ), (fun (ω : Ω) ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
Tactic: have I : ∀ k i, (fun ω ↦ ‖(X i - Y k i) ω‖) = (G k) ∘ (X i) := fun k i ↦ rfl