awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : α
u : Set (β × γ)
hu : MeasurableSet u
this :
  ∀ (b : β),
    Eq (α := ℝ≥0∞)
      ((((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) {c : γ | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} :
        ℝ≥0∞)
      (s.indicator
          (fun (b : β) ↦
            (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
          b :
        ℝ≥0∞)
⊢ ∫⁻ (b : β) in s,
      (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
        ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      s.indicator
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞) ({c : γ | (b, c) ∈ u} ∩ t))
        b ∂(κ : (a : α) → Measure β) a
have h : ∫⁻ (b : β) in s,
    (((η : (a : α × β) → Measure γ) (a, b) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ({x : γ | (b, x) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a =
  ∫⁻ (a_1 : β) in s,
    (((η : (a : α × β) → Measure γ) (a, a_1) : Measure γ) : (a : Set γ) → ℝ≥0∞)
      ({c : γ | (a_1, c) ∈ u} ∩ t) ∂(κ : (a : α) → Measure β) a
Tactic: rw [lintegral_indicator hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict (s := s) hs ⊗ₖ η = (κ ⊗ₖ η).restrict (s := SProd.sprod (β := Set γ) s Set.univ) ⋯
have rw : κ.restrict (s := s) hs ⊗ₖ η = κ.restrict (s := s) hs ⊗ₖ η.restrict (s := Set.univ) sorry
Tactic: rw [← compProd_restrict hs MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
s : Set β
hs : MeasurableSet s
⊢ κ.restrict (s := s) hs ⊗ₖ η = κ.restrict (s := s) hs ⊗ₖ η.restrict (s := Set.univ) ⋯
have e_η : η = η.restrict (s := Set.univ) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict (s := t) ht = (κ ⊗ₖ η).restrict (s := SProd.sprod (α := Set β) Set.univ t) ⋯
have rw : κ ⊗ₖ η.restrict (s := t) ht = κ.restrict (s := Set.univ) sorry ⊗ₖ η.restrict (s := t) ht
Tactic: rw [← compProd_restrict MeasurableSet.univ ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
t : Set γ
ht : MeasurableSet t
⊢ κ ⊗ₖ η.restrict (s := t) ht = κ.restrict (s := Set.univ) ⋯ ⊗ₖ η.restrict (s := t) ht
have e_κ : κ = κ.restrict (s := Set.univ) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have h : ∀ (a : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) a = Function.uncurry f a
Tactic: have h : ∀ a, ⨆ n, F n a = Function.uncurry f a := SimpleFunc.iSup_eapprox_apply hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) a = Function.uncurry f a
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have h₁ : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
Tactic: simp only [Prod.forall, Function.uncurry_apply_pair] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
⊢ ∫⁻ (bc : β × γ), f bc.1 bc.2 ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f b c ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have simp_rw : ∫⁻ (bc : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (bc.1, bc.2) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
  ∫⁻ (b : β),
    ∫⁻ (c : γ),
      ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [← h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
⊢ ∫⁻ (bc : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (bc.1, bc.2) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have h_mono : Monotone F
Tactic: have h_mono : Monotone F := fun i j hij b =>
    SimpleFunc.monotone_eapprox (Function.uncurry f) hij _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
⊢ ∫⁻ (bc : β × γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (bc.1, bc.2) ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have rw : ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
  ∫⁻ (b : β),
    ∫⁻ (c : γ),
      ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: rw [lintegral_iSup (fun n => (F n).measurable) h_mono]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
⊢ ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a) =
    ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a)
have hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a_1 : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
a : β
hf₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)
⊢ ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a) =
    ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (a, c) ∂(η : (a : α × β) → Measure γ) (a_1, a)
have h_mono₁ : Monotone.{0, u_3} (β := γ → ℝ≥0∞) fun (n : ℕ) (c : γ) ↦ (F n : (a : β × γ) → ℝ≥0∞) (a, c)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have this : ∀ (b : β),
  ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
    ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: have : ∀ b, ∫⁻ c, ⨆ n, F n (b, c) ∂η (a, b) = ⨆ n, ∫⁻ c, F n (b, c) ∂η (a, b) := by
    intro a
    rw [lintegral_iSup]
    · exact fun n => (F n).measurable.comp measurable_prodMk_left
    · exact fun i j hij b => h_mono hij _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ∫⁻ (c : γ),
        ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have simp_rw : ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
  ∫⁻ (b : β),
    ⨆ (n : ℕ),
      ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
f' : SimpleFunc (β × γ) ℝ≥0∞
⊢ Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))
have h₁ : ∀ (ab : β),
  ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab, c) ∂(η : (a : α × β) → Measure γ) (a, ab) =
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
        fun (b : β) ↦ (a, b))
      ab
Tactic: ext1 ab
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
f' : SimpleFunc (β × γ) ℝ≥0∞
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
have this₁ : Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
  (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
  ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
    fun (b : β) ↦ (a, b))
Tactic: have :
      (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) =
        (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
      ext1 ab; rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this_1 :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
f' : SimpleFunc (β × γ) ℝ≥0∞
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ≥0∞)
    (fun (b : β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b))
    ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
      fun (b : β) ↦ (a, b))
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦
    ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
have rw : Measurable.{u_2, 0} (α := β) (β := ℝ≥0∞)
  ((fun (ab : α × β) ↦ ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (ab.2, c) ∂(η : (a : α × β) → Measure γ) ab) ∘
    fun (b : β) ↦ (a, b))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: have h_some_meas_integral :
    ∀ f' : SimpleFunc (β × γ) ℝ≥0∞, Measurable fun b => ∫⁻ c, f' (b, c) ∂η (a, b) := by
    intro f'
    have :
      (fun b => ∫⁻ c, f' (b, c) ∂η (a, b)) =
        (fun ab => ∫⁻ c, f' (ab.2, c) ∂η ab) ∘ fun b => (a, b) := by
      ext1 ab; rfl
    rw [this]
    fun_prop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have rw : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
  (⨆ (n : ℕ),
    ∫⁻ (a_1 : β),
      ∫⁻ (c : γ),
        (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
    (⨆ (n : ℕ),
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have hf₁ : ∀ (n : ℕ),
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
    (⨆ (n : ℕ),
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)
hf₁ :
  ∀ (n : ℕ),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ ⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a =
    ∫⁻ (b : β),
      ⨆ (n : ℕ),
        ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) ∂(κ : (a : α) → Measure β) a
have h_mono₁ : Monotone.{0, u_2} (β := β → ℝ≥0∞) fun (n : ℕ) (b : β) ↦
  ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.CompProd (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst_1 : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (a, b) = f a b
h_mono : Monotone F
this :
  ∀ (b : β),
    ∫⁻ (c : γ), ⨆ (n : ℕ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b) =
      ⨆ (n : ℕ), ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
h_some_meas_integral :
  ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞),
    Measurable (β := ℝ≥0∞) fun (b : β) ↦
      ∫⁻ (c : γ), (f' : (a : β × γ) → ℝ≥0∞) (b, c) ∂(η : (a : α × β) → Measure γ) (a, b)
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
    (⨆ (n : ℕ),
      ∫⁻ (a_1 : β),
        ∫⁻ (c : γ),
          (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a)
have e_s : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (a : β × γ), (F n : (a : β × γ) → ℝ≥0∞) a ∂(κ ⊗ₖ η : (a : α) → Measure (β × γ)) a)
  fun (n : ℕ) ↦
  ∫⁻ (a_1 : β),
    ∫⁻ (c : γ), (F n : (a : β × γ) → ℝ≥0∞) (a_1, c) ∂(η : (a : α × β) → Measure γ) (a, a_1) ∂(κ : (a : α) → Measure β) a
Tactic: congr