mathlib-initiative/mathlib-tactics huggingface dataset:
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)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ) (cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)) = (Measure.pi μ) s

Tactic:
dsimp [e]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ)
      (cylinder univ
        (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }) ⁻¹' s)) =
    (Measure.pi μ) s
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ (((κ a).withDensity fun x ↦ ↑(f a x)).withDensity fun x ↦ g a x) =
    ((κ.withDensity fun a x ↦ ↑(f a x)).withDensity g) a

Tactic:
rw [Kernel.withDensity_apply _ hg, Kernel.withDensity_apply]

Goal state after:
case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (Function.uncurry fun a x ↦ ↑(f a x))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ if hα : Countable α then ((∂κ a/∂η a) x).toReal else (κ.map fun a ↦ (a, ())).density η a x univ

Tactic:
split_ifs with hα

Goal state after:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : Countable α
⊢ 0 ≤ ((∂κ a/∂η a) x).toReal

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
⊢ 0 ≤ (κ.map fun a ↦ (a, ())).density η a x univ
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
⊢ (if hα : Countable α then ((∂κ a/∂η a) x).toReal else (κ.map fun a ↦ (a, ())).density η a x univ) ≤ 1 x

Tactic:
split_ifs with hα

Goal state after:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : Countable α
⊢ ((∂κ a/∂η a) x).toReal ≤ 1 x

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
x : γ
hx_le_one : (∂κ a/∂η a) x ≤ 1 x
hα : ¬Countable α
⊢ (κ.map fun a ↦ (a, ())).density η a x univ ≤ 1 x
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p ↦
    if hα : Countable α then ((∂κ p.1/∂η p.1) p.2).toReal else (κ.map fun a ↦ (a, ())).density η p.1 p.2 univ

Tactic:
split_ifs with hα

Goal state after:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : Countable α
⊢ Measurable fun p ↦ ((∂κ p.1/∂η p.1) p.2).toReal

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
hα : ¬Countable α
⊢ Measurable fun p ↦ (κ.map fun a ↦ (a, ())).density η p.1 p.2 univ
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
h_le : κ ≤ κ + η
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (if hα : Countable α then ((∂κ a/∂(κ + η) a) x).toReal
        else (κ.map fun a ↦ (a, ())).density (κ + η) a x univ) ∂(κ + η) a =
    (κ a) s

Tactic:
split_ifs with hα

Goal state after:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal ∂(κ + η) a = (κ a) s

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((κ.map fun a ↦ (a, ())).density (κ + η) a x univ) ∂(κ + η) a = (κ a) s
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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
⊢ ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) = η

Tactic:
by
    ext a s
    have h : (withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x))
          + withDensity (κ + η) (fun a x ↦ Real.toNNReal (rnDerivAux κ (κ + η) a x))) a s
        = κ a s + η a s := by
      rw [this]
      simp
    simp only [FunLike.coe_add, Pi.add_apply, Measure.coe_add] at h
    rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj κ a (a + 1) f x₀ = ∫⁻ (x : X (a + 1)), f (update x₀ (a + 1) x) ∂(κ a) (frestrictLe a x₀)

Tactic:
by
  rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
  · congrm ∫⁻ x, f (fun i ↦ ?_) ∂_
    simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, piSingleton,
      MeasurableEquiv.coe_mk, update]
    split_ifs with h1 h2 h3 <;> try rfl
    all_goals lia
  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 : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a = (κ a) s

Tactic:
by
  rw [setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
    ← withDensity_apply _ hs, (κ a).withDensity_rnDeriv_eq _ h]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = (κ a) s
⊢ (κ a) s = 0 ∨ (κ a) s = 1

pp: case mp.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s

pp: case mp.ht
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s

Tactic:
· by_cases hκ : κ a s = 0
      · simp [hκ]
      · exact Or.inr <| (ENNReal.mul_eq_left hκ (by simp)).mp this

Goal state after:
case mp.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s

case mp.ht
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s
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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
k : ℕ
hk : n ≤ k
⊢ Measure.map (frestrictLe k) (η x) = inducedFamily (fun n ↦ (partialTraj κ a n) x) (Iic k)

Tactic:
rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]

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

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {false} = π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (((Kernel.boolKernel μ ν)†π) x) {false} = π {false} * (∂μ/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
⊢ ∀ᵐ (x : 𝓧) ∂⇑(Kernel.boolKernel μ ν) ∘ₘ π,
    (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x

Tactic:
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
π : Measure Bool
inst✝ : IsFiniteMeasure π
x : 𝓧
hx : ((Kernel.boolKernel μ ν)†π) x = π.withDensity fun ω ↦ (∂(Kernel.boolKernel μ ν) ω/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
⊢ (((Kernel.boolKernel μ ν)†π) x) {true} = π {true} * (∂ν/∂⇑(Kernel.boolKernel μ ν) ∘ₘ π) x
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hl : Measurable (Function.uncurry ℓ)
h : HasArgminEstimator ℓ P π
⊢ bayesRisk ℓ P π = ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π

Tactic:
rw [← h.isArgminEstimator_argminEstimator.isBayesEstimator hl,
    h.isArgminEstimator_argminEstimator.avgRisk_eq_lintegral_iInf hl]

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

Goal state before:
pp: p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal = (1 - ↑p) ^ n * ↑p

Tactic:
ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)

Goal state after:
p : ↑unitInterval
hp : p ≠ 0
n : ℕ
⊢ (1 - ↑p) ^ n * ↑p = (1 - ↑p) ^ n * ↑p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal = (1 - ↑p) ^ n * ↑p

Tactic:
ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → E
hp : p ≠ 0
n : ℕ
⊢ (1 - ↑p) ^ n * ↑p = (1 - ↑p) ^ n * ↑p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
n : ℕ
⊢ ((1 - ↑p) ^ n * ↑p) • f n = (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n

Tactic:
ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
n : ℕ
⊢ ((1 - ↑p) ^ n * ↑p) • f n = ((1 - ↑p) ^ n * ↑p) • f n
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
⊢ HasSum (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)

Tactic:
have : (fun n ↦ ((1 - p : ℝ) ^ n * p) • f n) =
      fun n ↦ (ENNReal.ofReal ((1 - p) ^ n * p)).toReal • f n := by
    ext n; rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
⊢ HasSum (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal = (1 - ↑p) ^ n * ↑p

Tactic:
ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)

Goal state after:
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
this : (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) = fun n ↦ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n
n : ℕ
⊢ (1 - ↑p) ^ n * ↑p = (1 - ↑p) ^ n * ↑p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: case e_f
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
n : ℕ
⊢ (ENNReal.ofReal ((1 - ↑p) ^ n * ↑p)).toReal • f n = ((1 - ↑p) ^ n * ↑p) • f n

Tactic:
ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)

Goal state after:
case e_f
p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
hp : p ≠ 0
f : ℕ → E
n : ℕ
⊢ ((1 - ↑p) ^ n * ↑p) • f n = ((1 - ↑p) ^ n * ↑p) • f n
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ b ∈ ⋃ a ∈ p.support, (f a).support

Tactic:
simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ ∫ (n : ℕ), f n ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
by
  rw [poissonMeasure, integral_sum_dirac (by simp)]
  congr with n
  rw [ENNReal.toReal_ofReal (by positivity)]

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

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

Tactic:
by split_ifs with ha <;> simp only [ite_self, tsum_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ ∑' (x : β), s.indicator (⇑(p.bindOnSupport f)) x =
    ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), s.indicator (⇑(f a ⋯)) x

Tactic:
classical
  calc
    (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
        ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      tsum_congr fun b => by split_ifs with hbs <;> simp only [tsum_zero]
    _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
      (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
    _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
      tsum_congr fun a => by split_ifs with ha <;> 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 ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ μ (s ∩ Set.univ) / μ s = 1

Tactic:
Set.inter_univ,

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 ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ μ s / μ s = 1
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg.refine_2.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ.restrict s

pp: case neg.refine_2.inr.inl.ha
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s ≠ 0

Tactic:
Measure.restrict_restrict hs,

Goal state after:
case neg.refine_2.inr.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s ∩ s, f x ∂μ

case neg.refine_2.inr.inl.ha
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s ≠ 0
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeSup ι
inst✝¹ : NoMaxOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure (κ a)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2.refine_1
Ω : 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 : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']
hf : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet (⋂ i ∈ s, f i)

Tactic:
exact .biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))

Goal state after: