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 α Ω
μ : Measure α
s : ι → Set Ω
ι' : Type u_5
g : ι' → ι
hg : Function.Surjective g
h : iIndepSet (s ∘ g) κ μ
⊢ iIndepSet s κ μ

Tactic:
iIndep.of_precomp hg h

Premises used: ProbabilityTheory.Kernel.iIndepSet, ProbabilityTheory.Kernel.iIndep.of_precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
ι' : Type u_5
g : ι' → ι
hg : Function.Bijective g
⊢ iIndepSet (s ∘ g) κ μ ↔ iIndepSet s κ μ

Tactic:
⟨.of_precomp hg.surjective, .precomp hg.injective⟩

Premises used: Function.Bijective.injective, ProbabilityTheory.Kernel.iIndepSet.of_precomp, Function.Bijective.surjective, Iff.intro, ProbabilityTheory.Kernel.iIndepSet.precomp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
h₁ :
  ∀ (a : α)
    (ha :
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t2 ∩ t1) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
filter_upwards [h t2 t1 ht2 ht1] with a ha
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t2 ∩ t1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
h₁ :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t2 ∩ t1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
h₂ h₃ h₄ h₅ :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t2 ∩ t1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rwa [Set.inter_comm, mul_comm]

Premises used: Set.inter_comm, mul_comm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : Indep m₁ m₂ κ μ
⊢ Indep m₂ m₁ κ μ

Tactic:
IndepSets.symm h

Premises used: ProbabilityTheory.Kernel.IndepSets.symm, ProbabilityTheory.Kernel.Indep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
_ :
  Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s →
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t →
      ∀ᵐ (a : α) ∂μ,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s →
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t →
      ∀ᵐ (a : α) ∂μ,
        (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
            ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t
⊢ t = ∅ ∨ t = univ

Tactic:
rw [Set.mem_setOf_eq, MeasurableSpace.measurableSet_bot_iff] at ht

Premises used: MeasurableSpace.measurableSet_bot_iff, Set.mem_setOf_eq
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : t = ∅ ∨ t = univ
inl :
  ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := Ω) (mα := _mα) (mβ := _mΩ) 0],
    ∀ᵐ (a : α) ∂μ,
      ((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
          (((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
          (((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
inr :
  ∀ (h : IsMarkovKernel κ),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
h : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : t = ∅ ∨ t = univ
inst : IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := Ω) (mα := _mα) (mβ := _mΩ) 0
⊢ ∀ᵐ (a : α) ∂μ,
    ((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((((0 : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h_1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
Filter.Eventually.of_forall (fun a ↦ ?_)

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h_1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
inr :
  ∀ (a : α),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
refine Filter.Eventually.of_forall (fun a ↦ ?_)

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h_1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
a : α
inr :
  ∀ (ht : t = ∅),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
inr₁ :
  ∀ (ht : t = univ),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rcases ht with ht | ht
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h_1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
h : IsMarkovKernel κ
a : α
ht : t = ∅
inr :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞)
inr₁ :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ∅ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) ∅ : ℝ≥0∞)
inr₂ :
  0 =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞)
inr₃ inr₄ : Eq (α := ℝ≥0∞) 0 0
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [ht, Set.inter_empty, measure_empty, mul_zero]

Premises used: MeasureTheory.measure_empty, MulZeroClass.mul_zero, Set.inter_empty
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s t : Set Ω
h_1 : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s
h : IsMarkovKernel κ
a : α
ht : t = univ
inr :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ univ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (1 : ℝ≥0∞)
inr₃ inr₄ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [ht, Set.inter_univ, measure_univ, mul_one]

Premises used: Set.inter_univ, MeasureTheory.IsProbabilityMeasure.measure_univ, mul_one
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
⊢ Indep ⊥ m' κ μ

Tactic:
(indep_bot_right m').symm

Premises used: ProbabilityTheory.Kernel.Indep.symm, ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s : Set Ω
simp : Indep (generateFrom {s}) ⊥ κ μ
⊢ IndepSet s ∅ κ μ

Tactic:
simp only [IndepSet, generateFrom_singleton_empty]

Premises used: ProbabilityTheory.Kernel.IndepSet, MeasurableSpace.generateFrom_singleton_empty
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥ κ μ

Tactic:
indep_bot_right _

Premises used: ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ Indep (generateFrom {s}) ⊥ κ μ

Tactic:
exact indep_bot_right _

Premises used: ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : IsZeroOrMarkovKernel κ
s : Set Ω
⊢ IndepSet ∅ s κ μ

Tactic:
(indepSet_empty_right s).symm

Premises used: ProbabilityTheory.Kernel.Indep.symm, ProbabilityTheory.Kernel.indepSet_empty_right, ProbabilityTheory.Kernel.IndepSet
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s₃ : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : IndepSets s₁ s₂ κ μ
h31 : s₃ ⊆ s₁
⊢ IndepSets s₃ s₂ κ μ

Tactic:
fun t1 t2 ht1 ht2 => h_indep t1 t2 (Set.mem_of_subset_of_mem h31 ht1) ht2

Premises used: Set.mem_of_subset_of_mem, ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s₃ : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : IndepSets s₁ s₂ κ μ
h32 : s₃ ⊆ s₂
⊢ IndepSets s₁ s₃ κ μ

Tactic:
fun t1 t2 ht1 ht2 => h_indep t1 t2 ht1 (Set.mem_of_subset_of_mem h32 ht2)

Premises used: Set.mem_of_subset_of_mem, ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ m₃ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
h31 : m₃ ≤ m₁
⊢ Indep m₃ m₂ κ μ

Tactic:
fun t1 t2 ht1 ht2 => h_indep t1 t2 (h31 _ ht1) ht2

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ m₃ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
h32 : m₃ ≤ m₂
⊢ Indep m₁ m₃ κ μ

Tactic:
fun t1 t2 ht1 ht2 => h_indep t1 t2 ht1 (h32 _ ht2)

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.Kernel.IndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ m₃ m₄ _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
h31 : m₃ ≤ m₁
h42 : m₄ ≤ m₂
⊢ Indep m₃ m₄ κ μ

Tactic:
indep_of_indep_of_le_left (indep_of_indep_of_le_right h_indep h42) h31

Premises used: ProbabilityTheory.Kernel.indep_of_indep_of_le_left, ProbabilityTheory.Kernel.indep_of_indep_of_le_right
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m₁ m₂ : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndep m₂ κ μ
h_le : ∀ (i : ι), m₁ i ≤ m₂ i
⊢ iIndep m₁ κ μ

Tactic:
fun s t ht ↦ h_indep s fun i hi ↦ h_le i (t i) <| ht i hi

Premises used: ProbabilityTheory.Kernel.iIndep, ProbabilityTheory.Kernel.iIndepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
inl :
  ∀ (ht1₁ : t1 ∈ s₁),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
inr :
  ∀ (ht1₂ : t1 ∈ s₂),
    ∀ᵐ (a : α) ∂μ,
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
          ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
rcases (Set.mem_union _ _ _).mp ht1 with ht1₁ | ht1₂

Premises used: Set.mem_union, Iff.mp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
h₁ t1 t2 ht1₁ ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact h₁ t1 t2 ht1₁ ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
h₂ t1 t2 ht1₂ ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ∀ᵐ (a : α) ∂μ,
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)

Tactic:
exact h₂ t1 t2 ht1₂ ht2
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
⊢ IndepSets (s₁ ∪ s₂) s' κ μ ↔ IndepSets s₁ s' κ μ ∧ IndepSets s₂ s' κ μ

Tactic:
⟨fun h =>
    ⟨indepSets_of_indepSets_of_le_left h Set.subset_union_left,
      indepSets_of_indepSets_of_le_left h Set.subset_union_right⟩,
    fun h => IndepSets.union h.left h.right⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left, ProbabilityTheory.Kernel.IndepSets.union
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋃ (n : ι), s n) t1
ht2 : t2 ∈ s'
⊢ ∃ (i : ι), t1 ∈ s i

Tactic:
rw [Set.mem_iUnion] at ht1

Premises used: Set.mem_iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
hyp : ∀ (n : ι), IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : Membership.mem (γ := Set (Set Ω)) (⋃ (n : ι), s n) t1
ht2 : t2 ∈ s'
ht1₁ : ∃ (i : ι), t1 ∈ s i
⊢ t2 ∈ s'

Tactic:
rw [Set.mem_iUnion] at ht1

Premises used: Set.mem_iUnion