mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs,

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSets m' hm' (fun i ↦ {s i}) μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.deterministic id ⋯) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
]

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic ⇑prodAssoc ⋯ ∥ₖ Kernel.deterministic id ⋯) =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map (⇑prodAssoc) id) ⋯ =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯

Tactic:
]

Goal state after:
W X Y Z : SFinKer
⊢ Kernel.deterministic (Prod.map id ⇑prodAssoc) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map (⇑prodAssoc) id) ⋯ =
    Kernel.deterministic ⇑prodAssoc ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m'] ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s : Finset ι) {f_1 : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f_1 i)) →
        μ[(⋂ i ∈ s, f_1 i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f_1 i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']

pp: case hm
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ

Tactic:
]

Goal state after:
case hm
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.snd ∘ id) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    (Kernel.deterministic id ⋯).map Prod.fst ∥ₖ Kernel.deterministic id ⋯

Tactic:
]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.snd ∘ id) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    (Kernel.deterministic id ⋯).map Prod.fst ∥ₖ Kernel.deterministic id ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
            μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω

Tactic:
]

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ (∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
            μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.snd ∘ id) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯

Tactic:
]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.snd ∘ id) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯

Tactic:
]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.fst ∘ id) ⋯ ∥ₖ Kernel.deterministic id ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.map (Prod.fst ∘ id) id) ⋯

Tactic:
]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic (Prod.map id (Prod.snd ∘ id)) ⋯ ∘ₖ Kernel.deterministic ⇑prodAssoc ⋯ =
    Kernel.deterministic (Prod.map (Prod.fst ∘ id) id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)

Tactic:
]

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ (∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

pp: case hf
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : ι), Measurable (f i)

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ (∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

case hf
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : ι), Measurable (f i)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀ =
    g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀ + g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀

pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x

Tactic:
]

Goal state after:
case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc) ⋯ =
    Kernel.deterministic ((Prod.map id Prod.swap ∘ ⇑MeasurableEquiv.prodAssoc) ∘ Prod.map Prod.swap id) ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
i : ι
hi : i ∈ s
⊢ f i ⁻¹' Exists.choose ⋯ = f i ⁻¹' g i

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
i : ι
hi : i ∈ s
⊢ f i ⁻¹' Exists.choose ⋯ = f i ⁻¹' g i
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic (⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ iCondIndepFun m' hm' f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

Tactic:
rw [iCondIndepFun_iff]
  swap
  · exact hf
  refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
  · refine h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)
    exact ⟨sets i, h_sets i hi, rfl⟩
  · classical
    let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
    specialize h s (sets := g) (fun i hi ↦ ?_)
    · simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1
    · have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
      convert! h with i hi i hi <;> exact hg i hi

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
⊢ iCondIndepFun m' hm' f μ ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

Tactic:
by
  rw [iCondIndepFun_iff]
  swap
  · exact hf
  refine ⟨fun h s sets h_sets ↦ ?_, fun h s sets h_sets ↦ ?_⟩
  · refine h s (g := fun i ↦ f i ⁻¹' (sets i)) (fun i hi ↦ ?_)
    exact ⟨sets i, h_sets i hi, rfl⟩
  · classical
    let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
    specialize h s (sets := g) (fun i hi ↦ ?_)
    · simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1
    · have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
      convert! h with i hi i hi <;> exact hg i hi

Goal state after:
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), g' n a * f a ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀

Tactic:
]

Goal state after:
case refine_3
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g' : ℕ → X → ℝ≥0∞
hg'_meas : ∀ (n : ℕ), Measurable (g' n)
hg'_mono : Monotone g'
hg' : ∀ (n : ℕ), ∫⁻ (x : X), g' n x * f x ∂π x₀ = g' n x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ ⨆ n, ∫⁻ (a : X), g' n a * f a ∂π x₀ = ⨆ i, g' i x₀ * ∫⁻ (x : X), f x ∂π x₀
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯