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

Goal state before:
pp: case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      ((traj κ a) x₀) s < ∞ →
        ∫ (x : (i : ℕ) → X i) in s,
            ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
          ∫ (x : (i : ℕ) → X i) in s, f x ∂(traj κ a) x₀

pp: case refine_2
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)

Tactic:
<;>

Goal state after:
case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      ((traj κ a) x₀) s < ∞ →
        ∫ (x : (i : ℕ) → X i) in s,
            ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
          ∫ (x : (i : ℕ) → X i) in s, f x ∂(traj κ a) x₀

case refine_2
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
x : ℝ
hx : 0 ≤ x
⊢ gammaPDFReal a r x = (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) x

Tactic:
simp_rw [gammaPDFReal, eq_true_intro hx, ite_true]

Goal state after:
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0

Tactic:
by
  rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
  · rw [lintegral_zero, ← ENNReal.ofReal_zero]
  · intro a (_ : a < _)
    simp only [paretoPDF_eq, ENNReal.ofReal_eq_zero]
    rw [if_neg (by linarith)]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∈ s
⊢ ∑' (a : α), p a * (f a) b = ∑' (a : α), p a * (f a) b

pp: case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∉ s
⊢ 0 = ∑' (a : α), p a * 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∈ s
⊢ ∑' (a : α), p a * (f a) b = ∑' (a : α), p a * (f a) b

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h✝ : b ∉ s
⊢ 0 = ∑' (a : α), p a * 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ (f a) b = (f a) b

pp: case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∉ s
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ (f a) b = (f a) b

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h✝ : b ∉ s
⊢ 0 = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0

pp: case neg
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : ¬a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0

case neg
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : ¬a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else (f a' h) b) =
    if a' = a then (f a ⋯) b else 0
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ a ∈ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support

Tactic:
Classical.not_not

Goal state after:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ a ∈ s ∧ a ∈ p.support ↔ a ∈ s ∧ a ∈ p.support
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : q b = 0
⊢ p a * 0 = q b * 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : ¬q b = 0
⊢ p a * 0 = q b * (p a * 0)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : q b = 0
⊢ p a * (q b * 0) = q b * 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : ¬q b = 0
⊢ p a * (q b * (f a h1 b h2) c) = q b * (p a * (f a h1 b ⋯) c)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : q b = 0
⊢ p a * 0 = q b * 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : ¬q b = 0
⊢ p a * 0 = q b * (p a * 0)

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : q b = 0
⊢ p a * (q b * 0) = q b * 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : ¬q b = 0
⊢ p a * (q b * (f a h1 b h2) c) = q b * (p a * (f a h1 b ⋯) c)
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∈ s
⊢ (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b) = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b

pp: case neg
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∉ s
⊢ 0 = ∑' (a : α), 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∈ s
⊢ (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b) = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
hbs : b ∉ s
⊢ 0 = ∑' (a : α), 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then 0 else 0) = p a * 0

pp: case neg
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : ¬p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0) = p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then 0 else 0) = p a * 0

case neg
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
ha : ¬p a = 0
⊢ (p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0) = p a * ∑' (b : β), if b ∈ s then (f a ha) b else 0
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[Y | m] =ᵐ[μ] μ[X | m]

pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[1 - Y | m] =ᵐ[μ] μ[1 - X | m]

Tactic:
<;>

Goal state after:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[Y | m] =ᵐ[μ] μ[X | m]

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[1 - Y | m] =ᵐ[μ] μ[1 - X | m]
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case inl
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 0
⊢ ‖X ω‖ ≤ 1

pp: case inr
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 1
⊢ ‖X ω‖ ≤ 1

Tactic:
<;>

Goal state after:
case inl
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 0
⊢ ‖X ω‖ ≤ 1

case inr
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 1
⊢ ‖X ω‖ ≤ 1
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[X ^ 2 | m] - μ[X | m] ^ 2 =ᵐ[μ] μ[X | m] - μ[X | m] ^ 2

Tactic:
refine .sub ?_ ae_eq_rfl

Goal state after:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
⊢ μ[X ^ 2 | m] =ᵐ[μ] μ[X | m]
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case inl
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 0
⊢ (X ^ 2) ω = X ω

pp: case inr
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 1
⊢ (X ^ 2) ω = X ω

Tactic:
<;>

Goal state after:
case inl
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 0
⊢ (X ^ 2) ω = X ω

case inr
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
hXmeas : Measurable X
ω : Ω
hω : X ω = 1
⊢ (X ^ 2) ω = X ω
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∈ t
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹

pp: case neg
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∉ t
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∈ t
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹

case neg
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
hx : x ∉ t
⊢ t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω ↦ ((condExpKernel μ m) ω).real s) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ]

Tactic:
rcases isEmpty_or_nonempty Ω with h | h
  · have : μ = 0 := Measure.eq_zero_of_isEmpty μ
    simpa [this] using! trivial
  have h := condDistrib_ae_eq_condExp (μ := μ)
    (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
  simp only [id_eq, MeasurableSpace.comap_id, preimage_id_eq] at h
  simp_rw [condExpKernel_apply_eq_condDistrib]
  exact h

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[s.indicator fun ω ↦ 1 | m ⊓ mΩ] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m]

Tactic:
inf_of_le_left hm

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ μ[s.indicator fun ω ↦ 1 | m] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m]
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᵐ[μ] μ[f | m]

Tactic:
inf_of_le_left hm

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m] =ᵐ[μ] μ[f | m]
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case inr
α : 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 η μα
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
apply Indep.congr (Filter.EventuallyEq.symm η_eq)

Goal state after:
case inr
α : 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 η μα
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) η μα
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: 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)

pp: 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)

Tactic:
<;>

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.Kernel.Proper

Goal state before:
pp: case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
x✝ : π.IsProper
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x

pp: case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
x✝ : π.IsProper
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x

case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
h : ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
⊢ ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x ↦ 1) x • π x
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable (A.indicator 1)

pp: case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x

Tactic:
<;>

Goal state after:
case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable (A.indicator 1)

case refine_1.hf
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
c : ℝ≥0∞
A : Set X
hA : MeasurableSet A
⊢ Measurable fun x ↦ B.indicator 1 x * A.indicator 1 x