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

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

pp: case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ¬↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i

case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : (i : ↥(Iic b)) → X ↑i
i : ↥(Iic b)
hi : ¬↑i ≤ a
⊢ (fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩) ((fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩)) x) i =
    x i
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hb
α : 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)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ (κ a) (univ ×ˢ s) ≠ ∞

pp: case hs
α : 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)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ A ⊆ univ

Tactic:
<;>

Goal state after:
case hb
α : 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)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ (κ a) (univ ×ˢ s) ≠ ∞

case hs
α : 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)
h : (κ a).real (A ×ˢ s) + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ A ⊆ univ
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i

pp: case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : ¬i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i

case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a i : ι
hi : ¬i ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩, invFun := fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i),
        left_inv := ⋯, right_inv := ⋯ }
      c i
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∈ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∉ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∈ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∉ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
h✝ : a ∈ s
⊢ ∫ (b : β), g b ∂κ a = ∫ (b : β), g b ∂κ a

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
h✝ : a ∉ s
⊢ ∫ (b : β), g b ∂η a = ∫ (b : β), g b ∂η a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
h✝ : a ∈ s
⊢ ∫ (b : β), g b ∂κ a = ∫ (b : β), g b ∂κ a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
h✝ : a ∉ s
⊢ ∫ (b : β), g b ∂η a = ∫ (b : β), g b ∂η a
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
t : Set β
h✝ : a ∈ s
⊢ ∫ (b : β) in t, g b ∂κ a = ∫ (b : β) in t, g b ∂κ a

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
t : Set β
h✝ : a ∉ s
⊢ ∫ (b : β) in t, g b ∂η a = ∫ (b : β) in t, g b ∂η a

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
t : Set β
h✝ : a ∈ s
⊢ ∫ (b : β) in t, g b ∂κ a = ∫ (b : β) in t, g b ∂κ a

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → E
t : Set β
h✝ : a ∉ s
⊢ ∫ (b : β) in t, g b ∂η a = ∫ (b : β) in t, g b ∂η a
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1.right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) = ∞ → (κ a) {p | p.1 ∈ countablePartitionSet n x} = ∞

Tactic:
refine fun h_top ↦ eq_top_mono (measure_mono (fun x ↦ ?_)) h_top

Goal state after:
case refine_1.right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h_top : (κ a) (countablePartitionSet n x✝ ×ˢ univ) = ∞
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}
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 κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ((κ.fst a) univ).toReal = ((κ a) univ).toReal

Tactic:
fst_apply' _ _ MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ((κ a) {p | p.1 ∈ univ}).toReal = ((κ a) univ).toReal
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case zero
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
hj : 0 ∈ Iic a
⊢ iterateInduction x ind ↑⟨0, hj⟩ = x ⟨0, hj⟩

pp: case succ
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ iterateInduction x ind ↑⟨j + 1, hj⟩ = x ⟨j + 1, hj⟩

Tactic:
<;>

Goal state after:
case zero
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
hj : 0 ∈ Iic a
⊢ iterateInduction x ind ↑⟨0, hj⟩ = x ⟨0, hj⟩

case succ
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ iterateInduction x ind ↑⟨j + 1, hj⟩ = x ⟨j + 1, hj⟩
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then ↑(toNNReal p) else 0) + if x ∈ s then 0 else ↑(toNNReal (σ p))) =
      if x ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1

Tactic:
<;>

Goal state after:
ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then ↑(toNNReal p) else 0) + if x ∈ s then 0 else ↑(toNNReal (σ p))) =
      if x ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real (⋃ x ∈ {t | t ⊆ u ∧ t.ncard ∈ {k}}, {x}) = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
← this.mem_toFinset

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real (⋃ x ∈ this.toFinset, {x}) = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
s : Set ι
hs : s ⊆ u ∧ s.ncard = k
⊢ setBer(u, p).real {s} = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
setBernoulli_real_singleton _ hs.1 hu,

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
s : Set ι
hs : s ⊆ u ∧ s.ncard = k
⊢ ↑p ^ s.ncard * (1 - ↑p) ^ (u \ s).ncard = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
<;>

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc b c, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ ∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x

pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
<;>

Goal state after:
case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ ∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x

case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a a.succ).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

pp: case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
<;>

Goal state after:
case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a a.succ).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

case inl.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a (n + 1)).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
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
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ (fun x ↦ f a b) =ᶠ[Filter.atTop] fun n ↦ min (f a b) ↑n

Tactic:
rw [Filter.EventuallyEq, Filter.eventually_atTop]

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
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) ↑n
⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → f a b = min (f a b) ↑b_1
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η

Tactic:
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le
  suffices withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
      + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))
      = κ + η by
    ext a s
    have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      simp
    simp only [FunLike.coe_add, Pi.add_apply, Measure.coe_add] at h
    rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h
  simp_rw [ofNNReal_toNNReal, ENNReal.ofReal_sub _ (rnDerivAux_nonneg h_le), ENNReal.ofReal_one]
  rw [withDensity_sub_add_cancel]
  · rw [withDensity_one']
  · exact measurable_const
  · fun_prop
  · intro a
    filter_upwards [rnDerivAux_le_one h_le] with x hx
    simp only [ENNReal.ofReal_le_one]
    exact hx

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable fun x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x

Tactic:
change Measurable ((Function.uncurry fun a b ↦
    ENNReal.ofReal (rnDerivAux κ (κ + η) a b)
    - ENNReal.ofReal (1 - rnDerivAux κ (κ + η) a b) * rnDeriv κ η a b) ∘ (fun b ↦ (a, b)))

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable
    ((Function.uncurry fun a b ↦
        ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b) ∘
      fun b ↦ (a, b))