mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
have := hXY.isProbabilityMeasure
  refine IndepFun.process_indepFun_process₀ mX mY fun I J ↦
    HasGaussianLaw.indepFun_of_covariance_strongDual ?_ fun L₁ L₂ ↦ ?_
  · let L : (I.disjSum J → E) →L[ℝ] (I → E) × (J → E) :=
      { toFun x := (fun s ↦ x ⟨Sum.inl s, inl_mem_disjSum.2 s.2⟩,
          fun t ↦ x ⟨Sum.inr t, inr_mem_disjSum.2 t.2⟩)
        map_add' x y := by ext <;> simp
        map_smul' c x := by ext <;> simp }
    exact (hXY.hasGaussianLaw _).map L
  classical
  have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
  · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
  · exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
⊢ Monotone I.orderEmbOfFinWithBot

Tactic:
intro i j hij

Goal state after:
T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
⊢ I.orderEmbOfFinWithBot i ≤ I.orderEmbOfFinWithBot j
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
C : ℝ≥0 → Ω → ℝ
hB : IsPreBrownianReal B P
h : ∀ (t : ℝ≥0), B t =ᵐ[P] C t
I : Finset ℝ≥0
⊢ HasLaw (fun ω ↦ I.restrict fun x ↦ C x ω) (projectiveFamily I) P

Tactic:
by
    refine (hB.hasLaw I).congr ?_
    have : ∀ᵐ ω ∂P, ∀ i : I, B i ω = C i ω := ae_all_iff.2 fun _ ↦ h _
    filter_upwards [this] with ω hω using funext fun i ↦ (hω i).symm

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p ↦ f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ } =
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF f) a, mono' := ⋯, right_continuous' := ⋯ }

Tactic:
← IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod a

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p ↦ f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ } =
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun p ↦ toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
η : Kernel α ℝ
inst✝ : IsMarkovKernel η
a : α
⊢ ((piecewise ⋯ η (deterministic (fun x ↦ Exists.choose ⋯) ⋯)) a) (range (embeddingReal Ω)) = 1

Tactic:
rw [piecewise_apply]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
η : Kernel α ℝ
inst✝ : IsMarkovKernel η
a : α
⊢ (if a ∈ (fun a ↦ (η a) (range (embeddingReal Ω))ᶜ) ⁻¹' {0} then η a
      else (deterministic (fun x ↦ Exists.choose ⋯) ⋯) a)
      (range (embeddingReal Ω)) =
    1
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)).toReal) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)).toReal)

Tactic:
refine (ENNReal.tendsto_toReal ?_).comp ?_

Goal state after:
case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x) ≠ ∞

case neg.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (ν a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ ∅) / (ν a) (countablePartitionSet n x)))
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

Tactic:
← setIntegral_condKernel hs MeasurableSet.univ hf

Goal state after:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
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 β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
⊢ condDistrib Y X μ = condDistrib Y' X' μ

Tactic:
rw [condDistrib, condDistrib]

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 β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).condKernel = (Measure.map (fun a ↦ (X' a, Y' a)) μ).condKernel
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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x ↦ (X x, Y x)) μ).fst
⊢ Measure.map (fun a ↦ (X a, Y a)) μ = (Measure.map (fun a ↦ (X a, Y a)) μ).fst ⊗ₘ κ

Tactic:
convert! hκ

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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x ↦ (X x, Y x)) μ).fst
⊢ (Measure.map (fun a ↦ (X a, Y a)) μ).fst = Measure.map X μ
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
κ : Kernel Unit (α × Ω)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitBorel = κ

Tactic:
rw [condKernelUnitBorel, compProd_fst_borelMarkovFromReal _ _ (disintegrate _ _)]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hba : b ≤ a
⊢ IicProdIoc a b = frestrictLe₂ hba ∘ Prod.fst

Tactic:
ext x i
  simp [IicProdIoc, (mem_Iic.1 i.2).trans hba]

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 Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ

Tactic:
by
  refine integrable_toReal_of_lintegral_ne_top ?_ ?_
  · exact Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX
  · refine ne_of_lt ?_
    calc
      ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
      _ = μ univ := lintegral_one
      _ < ∞ := measure_lt_top _ _

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ a
⊢ x.1 ⟨i, ⋯⟩ = if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩

Tactic:
dif_pos hi

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ a
⊢ x.1 ⟨i, ⋯⟩ = x.1 ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
μ : Measure β
s : Set β
⊢ ∫ (x : β) in s, f x ∂(const α μ) a = ∫ (x : β) in s, f x ∂μ

Tactic:
by rw [const_apply]

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

Goal state before:
pp: case refine_3
α : 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 Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ (∫⁻ (a : α) in t, ((condDistrib Y X μ) (X a)) s ∂μ).toReal = μ.real (t ∩ Y ⁻¹' s)

Tactic:
setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,

Goal state after:
case refine_3
α : 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 Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ (μ (t ∩ Y ⁻¹' s)).toReal = μ.real (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 α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ Tendsto (fun m ↦ ((κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)).toReal) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal)

Tactic:
refine (ENNReal.tendsto_toReal ?_).comp ?_

Goal state after:
case refine_1
α : 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) / (κ.fst a) (countablePartitionSet n x) ≠ ∞

case refine_2
α : 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
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ IsProjectiveLimit ν μ ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
rw [isProjectiveLimit_nat_iff' hμ _ 0]
  simp

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
⊢ setBer(∅, p) = dirac ∅

Tactic:
by
  ext s hs
  rw [setBernoulli_apply_eq_apply_subsets]
  by_cases h : ∅ ∈ s
  · have : {t | t ∈ s ∧ t ⊆ ∅} = {∅} := by grind
    simp_all
  · have : {t | t ∈ s ∧ t ⊆ ∅} = ∅ := by grind
    rw [this]
    simp_all

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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ map (IocProdIoc a b c) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i)) = Measure.pi fun i ↦ μ ↑i

Tactic:
refine (Measure.pi_eq fun s ms ↦ ?_).symm
  simp_rw [Measure.map_apply measurable_IocProdIoc (.univ_pi ms), IocProdIoc_preimage hab hbc,
    Measure.prod_prod, Measure.pi_pi, prod_eq_prod_extend]
  nth_rw 1 [Eq.comm, ← Ioc_union_Ioc_eq_Ioc hab hbc, prod_union (Ioc_disjoint_Ioc_of_le le_rfl)]
  congr 1 <;> refine prod_congr rfl fun x hx ↦ ?_
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_right hbc hx),
      restrict₂]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (Ioc_subset_Ioc_left hab hx),
      restrict₂]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:

Tactic:
Var[c • X; μ | m]
    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]
    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
⊢ Measurable (Function.uncurry (∑' (n : ι), f n))

Tactic:
have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) := by
      ext1 p
      simp only [Function.uncurry_def]
      rw [tsum_apply h_sum, tsum_apply (h_sum_a _), tsum_apply]
      exact Pi.summable.mpr fun p => ENNReal.summable
    rw [this]
    fun_prop

Goal state after:
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
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a a.succ).map (restrict₂ ⋯)) x₀ =
    (const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)) x₀

Tactic:
rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply,
        const_apply, Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod,
        measure_univ, one_smul]

Goal state after:
case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable ⇑(piSingleton a)

case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1))

case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a (a + 1))

case inl.refine_1.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
n : ℕ
⊢ Measurable ((A n).indicator 1)

Tactic:
A_eq

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
n : ℕ
⊢ Measurable ((cylinder (Iic (a n)) (S n)).indicator 1)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
n : ℕ
⊢ DependsOn ((A n).indicator 1) ↑(Iic (a n))

Tactic:
A_eq

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
n : ℕ
⊢ DependsOn ((cylinder (Iic (a n)) (S n)).indicator 1) ↑(Iic (a n))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) *
        ENNReal.ofReal ((1 - κ.rnDerivAux (κ + η) a x)⁻¹ * κ.rnDerivAux (κ + η) a x) =
    0 x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
← ENNReal.ofReal_mul,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) -
      ENNReal.ofReal ((1 - κ.rnDerivAux (κ + η) a x) * ((1 - κ.rnDerivAux (κ + η) a x)⁻¹ * κ.rnDerivAux (κ + η) a x)) =
    0 x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x