mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
h_univ : Set.univ = ⋃ a, {x | ‖x‖ ≤ ↑a}
⊢ Monotone fun a ↦ {x | ‖x‖ ≤ ↑a}

Tactic:
intro a

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
h_univ : Set.univ = ⋃ a, {x | ‖x‖ ≤ ↑a}
a : ℕ
⊢ ∀ ⦃b : ℕ⦄, a ≤ b → (fun a ↦ {x | ‖x‖ ≤ ↑a}) a ⊆ (fun a ↦ {x | ‖x‖ ≤ ↑a}) b
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: case inr
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
⊢ ∀ᵐ (a : α) ∂P,
    (η a) (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i)) =
      ∏ i ∈ I, (η a) ((fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i))

Tactic:
filter_upwards [(h I (fun i ↦ J i)).measure_inter_preimage_eq_mul _ _ .univ h',
    η_eq] with ω hω hη

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη✝ : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
this :
  ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
h' : ∀ i ∈ Finset.univ, MeasurableSet ((↑Finset.univ).pi fun j ↦ t ↑i ↑j)
ω : α
hω :
  (κ ω) (⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j) =
    ∏ i, (κ ω) ((fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j)
hη : κ ω = η ω
⊢ (η ω) (⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i)) =
    ∏ i ∈ I, (η ω) ((fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i))
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ ⨅ b, ∫⁻ (a_1 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) ↑↑b) ∂ν a = (κ a) (s ×ˢ Iic x)

case neg.hf_int
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ ∀ (b : { r' // x < ↑r' }), ∫⁻ (a_1 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) ↑↑b) ∂ν a ≠ ∞

case neg.h_directed
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun r b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r)

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
q : { r' // x < ↑r' }
⊢ Measurable fun b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑q)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case neg.h_directed
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun r b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r)

Tactic:
refine Monotone.directed_ge fun i j hij b ↦ ?_
    simp_rw [← measure_stieltjesOfMeasurableRat_Iic]
    refine measure_mono (Iic_subset_Iic.mpr ?_)
    exact mod_cast hij

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
nth_rewrite 2 [← ρ.disintegrate ρCond]

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this : IsSFiniteKernel ρCond
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * (ρ.fst ⊗ₘ ρCond) ({x} ×ˢ s)
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
⊢ TendstoInDistribution (fun n ω ↦ (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) atTop Y
    (fun x ↦ P) P'

Tactic:
by
  obtain h | h := eq_or_ne Var[X 0; P] 0
  · have : ∀ᵐ ω ∂P, ∀ n, X n ω = P[X 0] := by
      refine ae_all_iff.2 fun n ↦ ?_
      convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
      · rw [(hident n).integral_eq]
      · rwa [(hident n).variance_eq]
    have mX (n : ℕ) := (hident n).aemeasurable_fst
    refine tendstoInDistribution_of_identDistrib 0 (fun n ↦ ?_) ?_
    · refine ⟨by fun_prop, by fun_prop, Measure.map_congr ?_⟩
      filter_upwards [this] with ω hω
      simp [hω]
    · exact ⟨by fun_prop, by fun_prop, by simp [hY.map_eq, h]⟩
  have : HasLaw (fun ω ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P' := by
    convert! gaussianReal_div_const hY _
    · simp
    · ext; simp [h]
  convert!
    (tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub this h hindep hident).continuous_comp (g :=
      (√Var[X 0; P] * ·)) (by fun_prop)
  · simp [field] -- simp [field, hX] triggers the unused simp arguments linter
    field_simp [h]
  · ext
    simp [field] -- simp [field, hX] triggers the unused simp arguments linter
    field_simp [h]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
a : α
ha : ρ.fst {a} ≠ 0
⊢ (ρ.fst {a})⁻¹ * ρ ({a} ×ˢ univ) = 1

Tactic:
prod_univ,

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
a : α
ha : ρ.fst {a} ≠ 0
⊢ (ρ.fst {a})⁻¹ * ρ (Prod.fst ⁻¹' {a}) = 1
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂ν a =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) t₂ ∂ν a
⊢ ∀ x ∈ t₁ᶜ, ((IsCondKernelCDF.toKernel f hf) (a, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂ν a✝ =
    ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a✝, x)) t₂ ∂ν a✝
a : β
⊢ a ∈ t₁ᶜ → ((IsCondKernelCDF.toKernel f hf) (a✝, a)) (Prod.mk a ⁻¹' t₁ ×ˢ t₂) = 0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' s) ∂ν a = (κ a) s

Tactic:
induction s, hs
    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s s' : Set β
h : s ⊆ s'
h₀ : (ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤
    ((κ a) (countablePartitionSet n x ×ˢ s') / (ν a) (countablePartitionSet n x)).toReal

Tactic:
simp [h₀]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (Aᶜ ×ˢ s)

Tactic:
have h := integral_add_compl hA (integrable_density hκν a hs)
    rw [hA_eq, integral_density hκν a hs] at h
    have : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s := by
      rw [prod_sdiff_prod, compl_eq_univ_sdiff]
      simp
    rw [this, measureReal_def,
      measure_sdiff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),
      ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]
    rw [eq_tsub_iff_add_eq_of_le, add_comm]
    · exact h
    · gcongr <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ) (t ×ˢ s) = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs),

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ ((fun x ↦ (X x, Y x)) ⁻¹' t ×ˢ s) = μ (X ⁻¹' t ∩ Y ⁻¹' s)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
⊢ (κ.fst a) {a_1 | ¬κ.densityProcess κ.fst n a a_1 univ = 1} = 0

Tactic:
refine measure_mono_null this ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
⊢ (κ.fst a) {x | (κ.fst a) (countablePartitionSet n x) = 0} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (κ.fst a) {x | (κ.fst a) (countablePartitionSet n x) = 0} = 0

Tactic:
refine measure_mono_null this ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (κ.fst a) (⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u) = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (κ.fst a) (⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u) = 0

Tactic:
measure_biUnion

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ ∑' (p : ↑(countablePartition γ n)), (κ.fst a) (⋃ (_ : (κ.fst a) ↑p = 0), ↑p) = 0

case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (countablePartition γ n).Countable

case hd
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u

case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ ∀ b ∈ countablePartition γ n, MeasurableSet (⋃ (_ : (κ.fst a) b = 0), b)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
x : (n : ℕ) → X n
n : ℕ
h : k + 1 < a n
⊢ lmarginalPartialTraj κ k (a n) (f n) x =
    lmarginalPartialTraj κ k (k + 1) (lmarginalPartialTraj κ (k + 1) (a n) (f n)) x

Tactic:
rw [← lmarginalPartialTraj_self k.le_succ h.le (mf n)]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Defs

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsEmpty 𝓨
⊢ minimaxRisk ℓ P = ∞

Tactic:
by
  have : IsEmpty (Subtype (@IsMarkovKernel 𝓧 𝓨 m𝓧 m𝓨)) := by
    simp only [isEmpty_subtype]
    exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero
  simp [minimaxRisk, iInf_subtype']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
a : α
⊢ ∀ (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
a : α
⊢ ∀ (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0