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

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ map (frestrictLe₂ hba) (Measure.pi fun i ↦ μ ↑i) = Measure.pi fun i ↦ μ ↑i

pp: case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

pp: case inr.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

Tactic:
· exact isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm

Goal state after:
case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

case inr.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
f : α → β → ℝ≥0∞
⊢ (κ + η).withDensity f = κ.withDensity f + η.withDensity f

Tactic:
by_cases hf : Measurable (Function.uncurry f)
  · ext a s
    simp only [Kernel.withDensity_apply _ hf, add_apply, withDensity_add_measure]
  · simp_rw [withDensity_of_not_measurable _ hf]
    rw [zero_add]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
⊢ map (_root_.IicProdIoc a b) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i)) = Measure.pi fun i ↦ μ ↑i

Tactic:
by
  obtain hab | hba := le_total a b
  · refine (Measure.pi_eq fun s ms ↦ ?_).symm
    simp_rw [Measure.map_apply measurable_IicProdIoc (.univ_pi ms), IicProdIoc_preimage hab,
      Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]
    nth_rw 1 [Eq.comm, ← Iic_union_Ioc_eq_Iic hab, prod_union (Iic_disjoint_Ioc le_rfl)]
    congr 1 <;> refine prod_congr rfl fun x hx ↦ ?_
    · rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx),
        frestrictLe₂, restrict₂]
    · rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Iic_self hx),
        restrict₂]
  · rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
    · exact isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm
    all_goals fun_prop

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 α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) +
      ((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a ∪ s \ κ.mutuallySingularSetSlice η a)

Tactic:
simp only [measure_union (Disjoint.mono inter_subset_right le_rfl disjoint_sdiff_right)
    (hs.diff hm)]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ ((η.withDensity (κ.rnDeriv η)) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((η.withDensity (κ.rnDeriv η)) a) (s \ κ.mutuallySingularSetSlice η a) +
      (((κ.singularPart η) a) (s ∩ κ.mutuallySingularSetSlice η a) +
        ((κ.singularPart η) a) (s \ κ.mutuallySingularSetSlice η a)) =
    (κ a) (s ∩ κ.mutuallySingularSetSlice η a) + (κ a) (s \ κ.mutuallySingularSetSlice η a)
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 η
a : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in s, (∂κ a/∂η a) x ∂η a = (κ a) s

Tactic:
← withDensity_apply _ hs,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ((η a).withDensity (∂κ a/∂η a)) s = (κ a) s
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ν ((↑s).pi fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ) = ∏ i, (μ ↑i) (t i)

pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ Measurable s.restrict

pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)

Tactic:
hν,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∏ i ∈ s, (μ i) (if h : i ∈ s then t ⟨i, h⟩ else Set.univ) = ∏ i, (μ ↑i) (t i)

case a
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ ∀ (i : ι), MeasurableSet (if h : i ∈ s then t ⟨i, h⟩ else Set.univ)

case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ Measurable s.restrict

case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
s : Finset ι
t : (i : ↥s) → Set (X ↑i)
ht : ∀ (i : ↥s), MeasurableSet (t i)
⊢ MeasurableSet (Set.univ.pi t)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
⊢ map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i)) = infinitePi μ

Tactic:
refine eq_infinitePi μ fun s t ht ↦ ?_

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i))) ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Tactic:
case =>

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

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x

Tactic:
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _

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

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
⊢ p.toOuterMeasure {a} = p a

Tactic:
refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)
  · classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'
  · classical exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure s = 0 ↔ Disjoint p.support s

Tactic:
rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero]

Goal state after:
α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
case =>

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ ↑(cdf (paretoMeasure t r)) x = (∫⁻ (x : ℝ) in Iic x, paretoPDF t r x).toReal

Tactic:
by
  have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
  rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (pure a).toMeasure s = (Measure.dirac a) s

Tactic:
toMeasure_pure_apply a s hs,

Goal state after:
α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = (Measure.dirac a) s
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ENNReal.ofReal (poissonPMFReal r n) = (poissonPMF r) n

Tactic:
by
  simpa only [poissonPMF] using by rfl

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

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

Tactic:
wlog hXmeas : Measurable[m₀] X

Goal state after:
case inr
Ω : 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 Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [inst : IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1),
    Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]

Ω✝ : 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
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
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

Tactic:
simp only [ite_self, tsum_zero]

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

Goal state before:
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:
simp only [ite_self, tsum_zero]

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ μ[|s] = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))

Tactic:
withDensity_indicator (measurableSet_toMeasurable μ s),

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := toMeasurable μ s
⊢ μ[|s] = (μ.restrict (toMeasurable μ s)).withDensity ((μ t)⁻¹ • 1)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
⊢ IsFiniteMeasure (κ a) → (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
h'

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
h' : IsFiniteMeasure (κ a)
⊢ (κ a) t = 0 ∨ (κ a) t = 1
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
h_indep : iIndep s κ μα
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 η
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
replace h_indep := h_indep.congr η_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.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
hf : ∀ i ∈ s, f i ∈ π i
h' : (fun x ↦ ((condExpKernel μ m') x) (⋂ i ∈ s, f i)) =ᵐ[μ] fun x ↦ ∏ i ∈ s, ((condExpKernel μ m') x) (f i)
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω
⊢ ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i) →
    μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω = (∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ω

Tactic:
h'

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
hf : ∀ i ∈ s, f i ∈ π i
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (⋂ i ∈ s, f i)) =ᵐ[μ] fun x ↦ ∏ i ∈ s, ((condExpKernel μ m') x) (f i)
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)
⊢ μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω = (∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ω
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h' : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
⊢ ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t →
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω

Tactic:
h'

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2) →
    ∃ a_2, ∃ (h : 0 ≤ a_2 ∧ a_2 ≤ 1), (κ e.1).real (Icc 0 ⟨a_2, ⋯⟩) < ↑e.2 ∧ a < ⟨a_2, ⋯⟩

Tactic:
intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ σ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this✝ : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ stoppedValue f σ =ᵐ[μ] μ[f n | hσ.measurableSpace]

Tactic:
exact h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ
      (fun x => (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range

Goal state after: