mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ π.IsProper ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
by
  calc
    _ ↔ ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
          π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A := by
      simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
    _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

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

Tactic:
Kernel.deterministic_parallelComp_deterministic

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.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)

Tactic:
Kernel.deterministic_parallelComp_deterministic

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.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:
Kernel.deterministic_parallelComp_deterministic

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

Tactic:
Kernel.deterministic_parallelComp_deterministic

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

Tactic:
Kernel.deterministic_parallelComp_deterministic

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 ⋯ ∘ₖ 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:
Kernel.deterministic_parallelComp_deterministic

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 : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯) ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
Kernel.deterministic_parallelComp_deterministic

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

Tactic:
Kernel.deterministic_parallelComp_deterministic

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

Tactic:
Kernel.deterministic_parallelComp_deterministic

Goal state after:
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 id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
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 id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
Kernel.deterministic_parallelComp_deterministic

Goal state after:
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 id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
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 id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
Kernel.deterministic_parallelComp_deterministic

Goal state after:
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 Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
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 Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
Kernel.deterministic_parallelComp_deterministic

Goal state after:
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) ⋯)
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:
Kernel.deterministic_parallelComp_deterministic

Goal state after:
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) ⋯)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ f ⟂ᵢ[k, hk; μ] g ↔
    Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ

Tactic:
rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ Measure.map (fun ω ↦ (ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k inferInstance)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k inferInstance)).map g)) ∘ₘ
        μ.trim ⋯ ↔
    Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ Measure.map k μ
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a

Tactic:
have hκg : IsMarkovKernel (κ.map g) := IsMarkovKernel.map κ hg.measurable

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by
  suffices (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0 by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω
  rw [← lintegral_eq_zero_iff' (hX.aemeasurable_edist.pow_const p), ← nonpos_iff_eq_zero]
  calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ M * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp [h, hX.q_pos]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case e_s
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
i : ι
ω✝ ω : Ω
⊢ ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω ↔ ({ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω} ∩ {ω | ⊥ < τ n ω}) ω

Tactic:
exact ⟨fun h ↦ ⟨h, lt_of_lt_of_le h <| (iInf_le _ n).trans (iInf_le _ le_rfl)⟩, fun h ↦ h.1⟩

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
        · norm_cast
        · exact (continuous_id.add continuous_const).intervalIntegrable _ _

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ (∫ (a : Ω), rexp (↑q * X a) ∂κ ω') * rexp (↑cY * ↑q ^ 2 / 2) ≤ rexp ((↑c * ↑q ^ 2 + ↑cY * ↑q ^ 2) / 2)

Tactic:
add_div,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ (∫ (a : Ω), rexp (↑q * X a) ∂κ ω') * rexp (↑cY * ↑q ^ 2 / 2) ≤ rexp (↑c * ↑q ^ 2 / 2 + ↑cY * ↑q ^ 2 / 2)
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝³ : Monoid G
V : Type v'
inst✝² : AddCommMonoid V
k : Type u
inst✝¹ : CommSemiring k
inst✝ : Module k V
σ : Representation k G V
α : Type w'
i : α
g : G
r : k
f : α → V
⊢ (σ.freeLift f) (single i (MonoidAlgebra.single g r)) = r • (σ g) (f i)

Tactic:
by
  simp [freeLift]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V✝ : Type u_3
W✝ : Type u_4
U : Type u_5
inst✝¹³ : Semiring A
inst✝¹² : Monoid G
inst✝¹¹ : AddCommMonoid V✝
inst✝¹⁰ : AddCommMonoid W✝
inst✝⁹ : AddCommMonoid U
inst✝⁸ : Module A V✝
inst✝⁷ : Module A W✝
inst✝⁶ : Module A U
ρ✝ : Representation A G V✝
σ✝ : Representation A G W✝
τ✝ : Representation A G U
f✝¹ : V✝ →ₗ[A] W✝
V : Type u_6
W : Type u_7
P : Type u_8
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup P
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f✝ : V →ₗ[A] W
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (-f.toLinearMap) ∘ₗ ρ g = σ g ∘ₗ (-f.toLinearMap)

Tactic:
by simp [LinearMap.neg_comp, f.2]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
⊢ ∀ᵐ (ω : Ω),
    (fun n ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
          ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
      fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
obtain ⟨v, -, v_pos, v_lim⟩ :
      ∃ v : ℕ → ℝ, StrictAnti v ∧ (∀ n : ℕ, 0 < v n) ∧ Tendsto v atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have := fun i => strong_law_aux1 X hint hindep hident hnonneg c_one (v_pos i)
  filter_upwards [ae_all_iff.2 this] with ω hω
  apply Asymptotics.isLittleO_iff.2 fun ε εpos => ?_
  obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
  filter_upwards [hω i] with n hn
  simp only [Real.norm_eq_abs, Nat.abs_cast]
  exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
a✝ b✝ : V
hv : a✝ ∈ {v | ∀ (g : G), (ρ g) v = v}
hw : b✝ ∈ {v | ∀ (g : G), (ρ g) v = v}
g : G
⊢ (ρ g) (a✝ + b✝) = a✝ + b✝

Tactic:
by simp only [hv g, hw g, map_add]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Finite G
inst✝¹ : Group G
inst✝ : NeZero ↑(Nat.card G)
V : Rep k G
⊢ Injective V

Tactic:
by
  rw [← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff,
    ← Module.injective_iff_injective_object]
  exact Module.injective_of_isSemisimpleRing _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
f : M ⟶ N
r : k
g : N ⟶ O
x✝ : ↑M
⊢ (Hom.hom (f ≫ (r • g))).toLinearMap x✝ = (Hom.hom (r • f ≫ g)).toLinearMap x✝

Tactic:
simp [smul_hom, Representation.IntertwiningMap.smul_comp]

Goal state after: