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

Goal state before:
pp: case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b : β
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) a) ((fun i ↦ ⨆ n ∈ ns i, s n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) b) ((fun i ↦ ⨆ n ∈ ns i, s n) z)

Tactic:
obtain ⟨c, hc⟩ := hns a b

Goal state after:
case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 ↦ x1 ⊆ x2) (ns a) (ns c) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (ns b) (ns c)
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) a) ((fun i ↦ ⨆ n ∈ ns i, s n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) b) ((fun i ↦ ⨆ n ∈ ns i, s n) z)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 ↦ x1 ⊆ x2) (ns a) (ns c) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (ns b) (ns c)
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) a) ((fun i ↦ ⨆ n ∈ ns i, s n) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) b) ((fun i ↦ ⨆ n ∈ ns i, s n) z)

Tactic:
refine ⟨c, ?_, ?_⟩

Goal state after:
case inr.hm.refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 ↦ x1 ⊆ x2) (ns a) (ns c) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (ns b) (ns c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) a) ((fun i ↦ ⨆ n ∈ ns i, s n) c)

case inr.hm.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 ↦ x1 ⊆ x2) (ns a) (ns c) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (ns b) (ns c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ ⨆ n ∈ ns i, s n) b) ((fun i ↦ ⨆ n ∈ ns i, s n) c)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ False

Tactic:
suffices ∀ i ∈ t, i < c from lt_irrefl c (this c hct)

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Iic
hnsp : ∀ (i : ι), BddAbove (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → a ≤ x}
b : ι
hb : a < b
c : ι
hc : b ≤ c
hct : c ∈ t
⊢ ∀ i ∈ t, i < c
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 μ
⊢ CondIndepSet m' hm' s t μ ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
rw [condIndepSet_iff_condIndepSets_singleton _ _ hs ht μ, condIndepSets_singleton_iff _ _ hs ht]

Goal state after:
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:
rw [Kernel.deterministic_comp_deterministic]

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) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ =
    Kernel.deterministic (Prod.map id Prod.swap) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map Prod.swap id) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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.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:
rw [Kernel.deterministic_comp_deterministic]

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.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:
rw [Kernel.deterministic_comp_deterministic]

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.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:
rw [Kernel.deterministic_comp_deterministic]

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) ⋯
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:
rw [Kernel.deterministic_comp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id ∘ ⇑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) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ((⇑MeasurableEquiv.prodAssoc.symm ∘ Prod.swap) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ 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) ∘ ⇑MeasurableEquiv.prodAssoc.symm) ⋯ =
    Kernel.deterministic ((Prod.map Prod.swap id ∘ ⇑MeasurableEquiv.prodAssoc.symm) ∘ Prod.map id Prod.swap) ⋯

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Goal state before:
pp: X : SFinKer
⊢ Δ ≫ (β_ X X).hom = Δ

Tactic:
by ext : 1; dsimp; exact Kernel.swap_copy

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

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

Tactic:
rw [Kernel.deterministic_comp_deterministic]

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

Goal state before:
pp: case refine_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
c : ℝ
ω : Ω
⊢ ‖c * ∏ s, (g s) (X s ω)‖ ≤ ‖c‖ * ∏ s, ‖g s‖

Tactic:
norm_mul,

Goal state after:
case refine_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
c : ℝ
ω : Ω
⊢ ‖c‖ * ‖∏ s, (g s) (X s ω)‖ ≤ ‖c‖ * ∏ s, ‖g s‖
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: a✝¹ : PUnit.{u + 1}
s✝ : Set (PUnit.{u + 1} × PUnit.{u + 1})
a✝ : MeasurableSet s✝
⊢ ((Kernel.copy PUnit.{u + 1}) a✝¹) s✝ = ((Kernel.deterministic (fun x ↦ (PUnit.unit, x)) ⋯) a✝¹) s✝

Tactic:
simp [Kernel.copy_apply, Kernel.deterministic_apply]

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun ω s ↦ X s ω

Tactic:
refine indepFun_pi_of_prod_bcf
    ((aemeasurable_indicator_const_iff 1).2 mA) mX fun f g ↦ ?_
  have h1 ω : f (A.indicator 1 ω) * ∏ s, g s (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, g s (X s ω)) ω +
      f 0 * ∏ s, g s (X s ω) - A.indicator (fun ω ↦ f 0 * ∏ s, g s (X s ω)) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
  have h2 ω : f (A.indicator 1 ω) =
      A.indicator (fun _ ↦ f 1) ω + Aᶜ.indicator (fun _ ↦ f 0) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
  have hg {c : ℝ} : Integrable (fun ω ↦ c * ∏ s, g s (X s ω)) P := by
    refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)
    · exact (Finset.aestronglyMeasurable_fun_prod _ fun s _ ↦
        (g s).continuous.aestronglyMeasurable.comp_aemeasurable (mX s)).const_mul _
    · rw [norm_mul, norm_prod]
      gcongr with s
      exact (g s).norm_coe_le_norm _
  simp_rw [Pi.mul_apply, Finset.prod_apply, Function.comp_apply, h1, h2]
  rw [integral_sub, integral_add, integral_indicator₀ mA, integral_indicator₀ mA,
    integral_const_mul, integral_const_mul, integral_const_mul, integral_add,
    integral_indicator₀ mA, integral_indicator₀ mA.compl, integral_const, integral_const, h]
  · simp [measureReal_compl₀ mA]
    ring
  · exact (integrable_const _).indicator₀ mA
  · exact (integrable_const _).indicator₀ mA.compl
  · exact hg.indicator₀ mA
  · exact hg
  · exact (hg.indicator₀ mA).add hg
  · exact hg.indicator₀ mA

Goal state after: