awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
π : ι → Set (Set Ω)
⊢ iIndepSets π κ 0

Tactic:
simp [iIndepSets]

Premises used: ProbabilityTheory.Kernel.iIndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s1 s2 : Set (Set Ω)
⊢ IndepSets s1 s2 κ 0

Tactic:
simp [IndepSets]

Premises used: ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s1 s2 : Set (Set Ω)
⊢ IndepSets (_mΩ := _mΩ) s1 s2 0 μ

Tactic:
simp [IndepSets]

Premises used: ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ iIndep m κ 0

Tactic:
simp [iIndep]

Premises used: ProbabilityTheory.Kernel.iIndep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
⊢ Indep m₁ m₂ κ 0

Tactic:
simp [Indep]

Premises used: ProbabilityTheory.Kernel.Indep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
μ : Measure α
m₁ m₂ _mΩ : MeasurableSpace Ω
⊢ Indep m₁ m₂ (_mΩ := _mΩ) 0 μ

Tactic:
simp [Indep]

Premises used: ProbabilityTheory.Kernel.Indep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s : ι → Set Ω
⊢ iIndepSet s κ 0

Tactic:
simp [iIndepSet]

Premises used: ProbabilityTheory.Kernel.iIndepSet
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s t : Set Ω
⊢ IndepSet s t κ 0

Tactic:
simp [IndepSet]

Premises used: ProbabilityTheory.Kernel.IndepSet
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
⊢ IndepSet (_mΩ := _mΩ) s t 0 μ

Tactic:
simp [IndepSet]

Premises used: ProbabilityTheory.Kernel.IndepSet
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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 Ω)
h₁ :
  ∀ (a : Finset ι) (a_1 : ι → Set Ω),
    (∀ i ∈ a, a_1 i ∈ π i) →
      ((∀ᵐ (a_3 : α) ∂μ,
          Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
            (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)) ↔
        ∀ᵐ (a_3 : α) ∂μ,
          Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
            (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞))
⊢ iIndepSets π κ μ ↔ iIndepSets π η μ

Tactic:
peel 3
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)

Tactic:
⟨fun h' ↦ ?_, fun h' ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)

Tactic:
refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)
⊢ ∀ᵐ (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:
filter_upwards [h, h'] with a ha h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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_1 : Finset ι
a_2 : ι → Set Ω
h_1 : ∀ i ∈ a_1, a_2 i ∈ π i
h' :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
      (∏ i ∈ a_1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)
a : α
ha : Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω) ((η : (a : α) → Measure Ω) a : Measure Ω)
h'a :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
    (∏ i ∈ a_1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
    (∏ i ∈ a_1, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)

Tactic:
simpa [ha] using h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)
⊢ ∀ᵐ (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:
filter_upwards [h, h'] with a ha h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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_1 : Finset ι
a_2 : ι → Set Ω
h_1 : ∀ i ∈ a_1, a_2 i ∈ π i
h' :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
      (∏ i ∈ a_1, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)
a : α
ha : Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω) ((η : (a : α) → Measure Ω) a : Measure Ω)
h'a :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
    (∏ i ∈ a_1, (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a_1, a_2 i) : ℝ≥0∞)
    (∏ i ∈ a_1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_2 i) : ℝ≥0∞)

Tactic:
simpa [ha] using h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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 Ω)
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∞))
⊢ IndepSets s1 s2 κ μ ↔ IndepSets s1 s2 η μ

Tactic:
peel 4
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)

Tactic:
⟨fun h' ↦ ?_, fun h' ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)

Tactic:
refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)
⊢ ∀ᵐ (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:
filter_upwards [h, h'] with a ha h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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_1 a_2 : Set Ω
h_1 : a_1 ∈ s1
h_2 : a_2 ∈ s2
h' :
  ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)
a : α
ha : Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω) ((η : (a : α) → Measure Ω) a : Measure Ω)
h'a :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)
⊢ (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)

Tactic:
simpa [ha] using h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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∞)
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∞)
⊢ ∀ᵐ (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:
filter_upwards [h, h'] with a ha h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
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_1 a_2 : Set Ω
h_1 : a_1 ∈ s1
h_2 : a_2 ∈ s2
h' :
  ∀ᵐ (a : α) ∂μ,
    (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
        ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)
a : α
ha : Eq.{u_2 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω) ((η : (a : α) → Measure Ω) a : Measure Ω)
h'a :
  (((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
      ((((η : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 ∩ a_2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) a_2 : ℝ≥0∞)

Tactic:
simpa [ha] using h'a
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ iIndep m κ μ ↔ iIndep m η μ

Tactic:
iIndepSets_congr h

Premises used: ProbabilityTheory.Kernel.iIndep, ProbabilityTheory.Kernel.iIndepSets_congr
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
μ : Measure α
m₁ m₂ _mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ Indep m₁ m₂ κ μ ↔ Indep m₁ m₂ η μ

Tactic:
indepSets_congr h

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Kernel.indepSets_congr
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s : ι → Set Ω
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ iIndepSet s κ μ ↔ iIndepSet s η μ

Tactic:
iIndep_congr h

Premises used: ProbabilityTheory.Kernel.iIndepSet, ProbabilityTheory.Kernel.iIndep_congr
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s t : Set Ω
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ IndepSet s t κ μ ↔ IndepSet s t η μ

Tactic:
indep_congr h

Premises used: ProbabilityTheory.Kernel.indep_congr, ProbabilityTheory.Kernel.IndepSet