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

Goal state before:
pp: case pos
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ logRatio c * normThreshold a (n + 1) ^ 2 * a⁻¹ ^ 2 ≤ 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Tactic:
simp only [ha, inv_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero,
      Nat.ofNat_pos, pow_pos, mul_nonneg_iff_of_pos_right, inv_pos, mul_nonneg_iff_of_pos_left]
    refine Real.log_nonneg ?_
    rw [one_le_div]
    · refine (ENNReal.toReal_le_toReal (by finiteness) (by finiteness)).mpr ?_
      refine tsub_le_iff_left.mpr ?_
      rw [← two_mul]
      rw [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt
      exact hc_gt.le
    · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
      finiteness

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: case refine_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
x : StrongDual ℝ E
⊢ 0 ≤
    ((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
            (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap).toBilinForm
        x)
      x

Tactic:
simpa using hf.eq ..

Goal state after:
case refine_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
x : StrongDual ℝ E
⊢ 0 ≤ (f ((InnerProductSpace.toDual ℝ E).symm x)) ((InnerProductSpace.toDual ℝ E).symm x)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: case refine_6
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        (↑(L m) * I -
          ↑(((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
                    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap)
                  L)
                L) /
            2)

Tactic:
simpa using hf.eq ..

Goal state after:
case refine_6
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp (↑(L m) * I - ↑((f ((InnerProductSpace.toDual ℝ E).symm L)) ((InnerProductSpace.toDual ℝ E).symm L)) / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
this : MemLp (fun x ↦ ‖x‖ ^ 2) (p / 2) μ
⊢ MemLp (fun x ↦ ‖id x‖ ^ ENNReal.toReal 2) (p / 2) μ

Tactic:
simpa using this

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: case refine_6
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ ∀ (L : StrongDual ℝ E),
    charFunDual μ L =
      cexp
        (↑(L m) * I -
          ↑(((f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
                    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap)
                  L)
                L) /
            2)

Tactic:
simp [← charFun_toDual_symm_eq_charFunDual, h]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map Y P)

Tactic:
rw [← Measure.map_congr h]

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map X P)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

Tactic:
by
  let g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
    f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
      (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
  have : ∀ L : StrongDual ℝ E, charFunDual μ L = exp (L m * I - g L L / 2) := by
    simp [← charFun_toDual_symm_eq_charFunDual, h, g]
  have hg : g.toBilinForm.IsPosSemidef :=
    ⟨⟨fun x y ↦ by simpa [g] using hf.eq ..⟩, ⟨fun x ↦ by simpa [g] using hf.nonneg _⟩⟩
  have := gaussian_charFunDual_congr hg this
  refine ⟨this.1, ?_⟩
  ext
  simp [covarianceBilin, ← this.2, g, ← InnerProductSpace.toDual_apply_eq_toDualMap_apply,
    -InnerProductSpace.toContinuousLinearMap_toDualMap]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
⊢ cov[fun x ↦ x.ofLp i, fun x ↦ x.ofLp j; multivariateGaussian μ S] = S i j

Tactic:
have (i : ι) : (fun x : EuclideanSpace ℝ ι ↦ x i) =
      fun x ↦ ⟪EuclideanSpace.basisFun ι ℝ i, x⟫ := by ext; simp [PiLp.inner_apply]
  rw [this, this, ← covarianceBilin_apply_eq_cov, covarianceBilin_multivariateGaussian hS]
  · simp
  · exact IsGaussian.memLp_two_id

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
⊢ HasGaussianLaw X P

Tactic:
by
    refine ⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩
    rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
    all_goals fun_prop

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: ⊢ IsProjectiveMeasureFamily projectiveFamily

Tactic:
by
  intro I J hJI
  nth_rw 2 [projectiveFamily]
  rw [Measure.map_map]
  · have : (Finset.restrict₂ (π := fun _ ↦ ℝ) hJI ∘ (MeasurableEquiv.toLp 2 (I → ℝ)).symm) =
        ofLp ∘ (EuclideanSpace.restrict₂ hJI) := by ext; simp
    rw [this, ((measurePreserving_ofLp_multivariateGaussian J).comp
        (measurePreserving_restrict₂_multivariateGaussian (posSemidef_covMatrix I) hJI)).map_eq]
  · exact Finset.measurable_restrict₂ _ -- fun_prop fails
  · fun_prop

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

Goal state before:
pp: case neg.refine_1
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ 0 ≤ᵐ[μ] fun x ↦ rexp (1 * ‖x‖ ^ 2)

pp: case neg.refine_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ (fun x ↦ rexp (1 * ‖x‖ ^ 2)) ≤ᵐ[μ] fun x ↦ rexp (b ^ 2)

Tactic:
· exact ae_of_all _ fun _ ↦ by positivity

Goal state after:
case neg.refine_2
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
hb' : ∀ᵐ (x : E) ∂μ, ‖x‖ ≤ b
⊢ (fun x ↦ rexp (1 * ‖x‖ ^ 2)) ≤ᵐ[μ] fun x ↦ rexp (b ^ 2)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
⊢ ↑(min s t) = cov[Function.eval ⟨s, ⋯⟩, fun x ↦ x ⟨t, ⋯⟩; projectiveFamily {s, t}]

Tactic:
rw [covariance_eval_projectiveFamily]

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

Goal state before:
pp: ⊢ ∃ a, ∀ (b : ℚ), a ≤ b → 1 = defaultRatCDF b

Tactic:
exact ⟨0, fun q hq => (if_neg (not_lt.mpr hq)).symm⟩

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ stieltjesFunctionAux f a r

Tactic:
rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' // r < ↑r' }
⊢ 0 ≤ ⨅ q, f a ↑q
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (x_1 : β) in univ, ↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x ∂ν a = (κ a).real (univ ×ˢ Iic x)

Tactic:
setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ (κ a).real (univ ×ˢ Iic x) = (κ a).real (univ ×ˢ Iic x)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
⊢ (∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q) → Monotone (f (a, t)) → IsRatStieltjesPoint f (a, t)

Tactic:
ht_iInf

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
ht_iInf : ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q
⊢ Monotone (f (a, t)) → IsRatStieltjesPoint f (a, t)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
⊢ cov[fun ω ↦ ↑s * B (1 / s) ω, fun ω ↦ ↑t * B (1 / t) ω; P] = ↑s

Tactic:
have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval]
    obtain rfl | hs := eq_or_ne s 0
    · simp
    have : 0 < t := (pos_of_ne_zero hs).trans_le hst
    rw [min_eq_right]
    · norm_cast
      field_simp
    exact one_div_le_one_div_of_le (pos_of_ne_zero hs) hst

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

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

Tactic:
rw [← Real.iUnion_Iic_rat, prod_iUnion]
  have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) := by
    refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
    exact mod_cast hrr'
  have h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ s ×ˢ Iic (q : ℝ) := by
    refine Monotone.directed_le fun i j hij ↦ ?_
    refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
    exact mod_cast hij
  simp_rw [h_dir.measure_iUnion, h_dir_prod.measure_iUnion]
  rw [lintegral_iSup_directed]
  · simp_rw [setLIntegral_toKernel_Iic hf _ _ hs]
  · refine fun q ↦ Measurable.aemeasurable ?_
    exact (Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left
  · refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)
    exact mod_cast hij

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)

Tactic:
have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by
    congr; exact (κ.disintegrate _).symm

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hs
α : 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
⊢ ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ seq i) (κ a)

pp: case hm
α : 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
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m

pp: case hf
α : 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
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞

Tactic:
· measurability

Goal state after:
case hm
α : 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
⊢ Antitone fun m ↦ countablePartitionSet n x ×ˢ seq m

case hf
α : 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
⊢ ∃ i, (κ a) (countablePartitionSet n x ×ˢ seq i) ≠ ∞
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 α (γ × β)
ν : Kernel α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable fun x ↦ κ.density ν a x s

Tactic:
by
  change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))
  exact (measurable_density κ ν hs).comp measurable_prodMk_left

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 μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

Tactic:
by
  by_cases hX : AEMeasurable X μ
  swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]
  refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
  calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    simp [Function.comp_def]
  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]

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

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

Tactic:
measure_sdiff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),

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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
let f := embeddingReal Ω
  have hf := measurableEmbedding_embeddingReal Ω
  set ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) with hρ'def
  have hρ' : ρ'.fst = ρ.fst := by
    ext s hs
    rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply]
    exacts [rfl, Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd,
      measurable_fst hs, hs, hs]
  have hρ'' : ∀ᵐ x ∂ρ.fst, Kernel.map κ f x = ρ'.condKernel x := by
    rw [← hρ']
    refine eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_
    ext s hs
    conv_lhs => rw [hρ'def, hκ]
    rw [Measure.map_apply (measurable_id.prodMap hf.measurable) hs, hρ',
      Measure.compProd_apply hs, Measure.compProd_apply (measurable_id.prodMap hf.measurable hs)]
    congr with a
    rw [Kernel.map_apply' _ hf.measurable]
    exacts [rfl, measurable_prodMk_left hs]
  suffices ∀ᵐ x ∂ρ.fst, ∀ s, MeasurableSet s → ρ'.condKernel x s = ρ.condKernel x (f ⁻¹' s) by
    filter_upwards [hρ'', this] with x hx h
    rw [Kernel.map_apply _ hf.measurable] at hx
    ext s hs
    rw [← Set.preimage_image_eq s hf.injective,
      ← Measure.map_apply hf.measurable <| hf.measurableSet_image.2 hs, hx,
      h _ <| hf.measurableSet_image.2 hs]
  suffices ρ.map (Prod.map id f) = (ρ.fst ⊗ₘ (Kernel.map ρ.condKernel f)) by
    rw [← hρ'] at this
    have heq := eq_condKernel_of_measure_eq_compProd_real _ this
    rw [hρ'] at heq
    filter_upwards [heq] with x hx s hs
    rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]
  ext s hs
  conv_lhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [Measure.compProd_apply hs, Measure.map_apply (measurable_id.prodMap hf.measurable) hs,
    Measure.compProd_apply]
  · congr with a
    rw [Kernel.map_apply' _ hf.measurable]
    exacts [rfl, measurable_prodMk_left hs]
  · exact measurable_id.prodMap hf.measurable hs

Goal state after: