awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a : Finset ι
a_1 : ι → Set Ω
h_1 : ∀ i ∈ a, a_1 i ∈ π i
⊢ (∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)) ↔
    ∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
have h₁ : ∀
  (h' :
    ∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)),
  ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
Tactic: refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a : Finset ι
a_1 : ι → Set Ω
h_1 : ∀ i ∈ a, a_1 i ∈ π i
h₁ :
  ∀
    (h' :
      ∀ᵐ (a_2 : α) ∂μ,
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
          (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)),
    ∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
⊢ (∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)) ↔
    ∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
have h₂ : ∀
  (h' :
    ∀ᵐ (a_2 : α) ∂μ,
      Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
        (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)),
  ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
Tactic: refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a : Finset ι
a_1 : ι → Set Ω
h_1 : ∀ i ∈ a, a_1 i ∈ π i
h' :
  ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
⊢ ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
have h₁ : ∀ (a_2 : α)
  (ha :
    Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a_2 : Measure Ω)
      ((η : (a : α) → Measure Ω) a_2 : Measure Ω))
  (h'a :
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
    (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
Tactic: filter_upwards [h, h'] with a ha h'a
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a : Finset ι
a_1 : ι → Set Ω
h_1 : ∀ i ∈ a, a_1 i ∈ π i
h' :
  ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
⊢ ∀ᵐ (a_2 : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
have h₁ : ∀ (a_2 : α)
  (ha :
    Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a_2 : Measure Ω)
      ((η : (a : α) → Measure Ω) a_2 : Measure Ω))
  (h'a :
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
      (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
    (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)
Tactic: filter_upwards [h, h'] with a ha h'a
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ
have h₁ : ∀ (a a_1 : Set Ω),
  a ∈ s1 →
    a_1 ∈ s2 →
      ((∀ᵐ (a_4 : α) ∂μ,
          (((κ : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
              ((((κ : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
              ((((κ : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)) ↔
        ∀ᵐ (a_4 : α) ∂μ,
          (((η : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
              ((((η : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
              ((((η : (a : α) → Measure Ω) a_4 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞))
Tactic: peel 4
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a a_1 : Set Ω
h_1 : a ∈ s1
h_2 : a_1 ∈ s2
⊢ (∀ᵐ (a_2 : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)) ↔
    ∀ᵐ (a_2 : α) ∂μ,
      (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
have h₁ : ∀
  (h' :
    ∀ᵐ (a_2 : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)),
  ∀ᵐ (a_2 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
Tactic: refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a a_1 : Set Ω
h_1 : a ∈ s1
h_2 : a_1 ∈ s2
h₁ :
  ∀
    (h' :
      ∀ᵐ (a_2 : α) ∂μ,
        (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
            ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
            ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)),
    ∀ᵐ (a_2 : α) ∂μ,
      (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
⊢ (∀ᵐ (a_2 : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)) ↔
    ∀ᵐ (a_2 : α) ∂μ,
      (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
have h₂ : ∀
  (h' :
    ∀ᵐ (a_2 : α) ∂μ,
      (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
          ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)),
  ∀ᵐ (a_2 : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
Tactic: refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a a_1 : Set Ω
h_1 : a ∈ s1
h_2 : a_1 ∈ s2
h' :
  ∀ᵐ (a_2 : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
⊢ ∀ᵐ (a_2 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
have h₁ : ∀ (a_2 : α)
  (ha :
    Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a_2 : Measure Ω)
      ((η : (a : α) → Measure Ω) a_2 : Measure Ω))
  (h'a :
    (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)),
  (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
Tactic: filter_upwards [h, h'] with a ha h'a
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
a a_1 : Set Ω
h_1 : a ∈ s1
h_2 : a_1 ∈ s2
h' :
  ∀ᵐ (a_2 : α) ∂μ,
    (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
⊢ ∀ᵐ (a_2 : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
have h₁ : ∀ (a_2 : α)
  (ha :
    Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a_2 : Measure Ω)
      ((η : (a : α) → Measure Ω) a_2 : Measure Ω))
  (h'a :
    (((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)),
  (((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a ∩ a_1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a_2 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
Tactic: filter_upwards [h, h'] with a ha h'a
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
have h₁ : ∀ (a : α)
  (ha :
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), univ) :
        ℝ≥0∞)
      (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)),
  IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
Tactic: filter_upwards [h.meas_biInter ∅ (f := fun _ ↦ Set.univ) (by simp)] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (a : α) ↦
                Eq (α := ℝ≥0∞)
                  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
                      (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
                    ℝ≥0∞)
                  (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (a : α) ↦
                Eq (α := ℝ≥0∞)
                  ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
                  (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
              x}
          x}
    a
Tactic: filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
                        (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
                      ℝ≥0∞)
                    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (a : α) ↦
                  Eq (α := ℝ≥0∞)
                    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
                    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞))
                x}
            x}
      a
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
have h₂ : ∀ (a : α),
  Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
        ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha]
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
have h₁ : ∀ (a : α)
  (ha :
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i) :
        ℝ≥0∞)
      (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞)
    (∏ i : ι, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have inl : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ m i),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
        ℝ≥0∞)
      (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: obtain rfl | ⟨i, rfl⟩ : s = ∅ ∨ ∃ i, s = {i} := by
    simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst_1 : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
inl :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ m i),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
            (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Finset ι) ∅ i), f i) :
          ℝ≥0∞)
        (∏ i ∈ ∅, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have inr : ∀ (i : ι) (hf : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → f i_1 ∈ m i_1),
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (⋂ (i_1 : ι), ⋂ (_ : Membership.mem (γ := Finset ι) {i} i_1), f i_1) :
        ℝ≥0∞)
      (∏ i ∈ {i}, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: obtain rfl | ⟨i, rfl⟩ : s = ∅ ∨ ∃ i, s = {i} := by
    simpa using (subsingleton_of_subsingleton (s := (s : Set ι))).eq_empty_or_singleton
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
      (∏ i ∈ s, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have f'_apply : ∀ (x : ι'), f' (g x) = f x
Tactic: have f'_apply x : f' (g x) = f x := hg.extend_apply ..
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun (x : ι) ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
⊢ ∀ i ∈ Finset.image g s, f' i ∈ π i
have simp_rw : ∀ ⦃x : ι'⦄, x ∈ s → f x ∈ π (g x)
Tactic: simp_rw [Finset.forall_mem_image, f'_apply]