awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
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 :
  ∀ (ω : Ω)
    (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 ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    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ωψ
-- Module: Mathlib.Probability.StrongLaw
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
    (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 ω)))
    atTop
    (𝓝 (HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (x : Ω), ((⇑ψ : (a : E) → E) ∘ X 0) x ∂μ)))

Tactic:
hωφ.add hωψ

Premises used: Filter.Tendsto.add
-- Module: Mathlib.Probability.StrongLaw
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 ω))
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 ∂μ))
⊢ 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:
convert! hωφ.add hωψ using 1

Premises used: Filter.Tendsto.add
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ 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:
simp [sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Probability.StrongLaw
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 :
  ∫ (x : Ω), ((⇑(φ + ψ) : (a : E) → E) ∘ X 0) x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : Ω), ((⇑φ : (a : E) → E) ∘ X 0) x ∂μ) (∫ (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 ∂μ))

Tactic:
congr 1
-- Module: Mathlib.Probability.StrongLaw
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) μ
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 ∂μ)

Tactic:
rw [← integral_add]

Premises used: MeasureTheory.integral_add
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ 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:
rfl
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ Integrable (ε := E) ((⇑φ : (a : E) → E) ∘ X 0) μ

Tactic:
(φ.comp (X 0) h').integrable_of_isFiniteMeasure

Premises used: MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ Integrable (ε := E) ((⇑φ : (a : E) → E) ∘ X 0) μ

Tactic:
exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure

Premises used: MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ Integrable (ε := E) ((⇑ψ : (a : E) → E) ∘ X 0) μ

Tactic:
(ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Premises used: MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
⊢ Integrable (ε := E) ((⇑ψ : (a : E) → E) ∘ X 0) μ

Tactic:
exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Premises used: MeasureTheory.SimpleFunc.integrable_of_isFiniteMeasure, OfNat.ofNat, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.Probability.StrongLaw
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}
⊢ 0 ∈ s

Tactic:
simp [s]
-- Module: Mathlib.Probability.StrongLaw
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}
⊢ 0 ∈ s

Tactic:
have zero_s : 0 ∈ s := by simp [s]
-- Module: Mathlib.Probability.StrongLaw
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
⊢ SeparableSpace.{u_2} (↑s : Type u_2)

Tactic:
have : SeparableSpace s := h'.separableSpace_range_union_singleton
-- Module: Mathlib.Probability.StrongLaw
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)
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
have : Nonempty s := ⟨0, zero_s⟩
-- Module: Mathlib.Probability.StrongLaw
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
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ (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))
-- Module: Mathlib.Probability.StrongLaw
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 ∂μ))
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 ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ (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 ∂μ))

Tactic:
apply ae_all_iff.2 (fun k ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff