mathlib-initiative/mathlib-tactics huggingface dataset:
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 Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : β), ((condDistrib Y X μ) a) s ∂Measure.map X (μ.restrict (X ⁻¹' t)) = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
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 β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : β), ((Measure.map (fun a ↦ (X a, Y a)) μ).condKernel a) s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    μ (X ⁻¹' t ∩ Y ⁻¹' s)
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂(κ.restrict hs) a = ∫ (x : β) in t ∩ s, f x ∂κ a

Tactic:
restrict_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
a : α
s : Set β
hs : MeasurableSet s
t : Set β
⊢ ∫ (x : β) in t, f x ∂(κ a).restrict s = ∫ (x : β) in t ∩ s, f x ∂κ a
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (y : β) in t, ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂(Measure.map (fun a ↦ (X a, Y a)) μ).fst =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
condDistrib,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (y : β) in t,
      ∫ (y_1 : Ω),
        f (y, y_1) ∂(Measure.map (fun a ↦ (X a, Y a)) μ).condKernel y ∂(Measure.map (fun a ↦ (X a, Y a)) μ).fst =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ (map Set.ncard setBer(u, p)) s = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}

Tactic:
map_apply (by fun_prop) .of_discrete,

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ setBer(u, p) (Set.ncard ⁻¹' s) = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (↑n + 1) = f a b ∧ min (f a b) ↑n = f a b
⊢ f a b - f a b = 0

Tactic:
tsub_self (f a b)

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)
s : Finset ℕ
S : Set ((i : ↥s) → X ↑i)
mS : MeasurableSet S
hA : cylinder s S ∈ measurableCylinders X
⊢ (piContent μ) (cylinder s S) = (infinitePiNat μ) (cylinder s S)

Tactic:
piContent_cylinder _ mS,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
s : Finset ℕ
S : Set ((i : ↥s) → X ↑i)
mS : MeasurableSet S
hA : cylinder s S ∈ measurableCylinders X
⊢ (Measure.pi fun i ↦ μ ↑i) S = (infinitePiNat μ) (cylinder s 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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
n : ℕ
| (Measure.pi fun i ↦ μ ↑i) (S n)

Tactic:
← pi_map_piCongrLeft (aux n),

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
n : ℕ
| (Measure.map (⇑(piCongrLeft (fun i ↦ X ↑i) (aux n))) (Measure.pi fun i ↦ μ ↑((aux n) i))) (S 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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η a).withDensity (∂κ a/∂η a)) s ≤ (κ a) s

Tactic:
exact (κ a).withDensity_rnDeriv_le _ _

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

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c✝ : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
⊢ lmarginalPartialTraj κ b c f = lmarginalPartialTraj κ b d f

Tactic:
rw [hf.lmarginalPartialTraj_of_le c mf (hac.trans hcb),
      hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)]

Goal state after:
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ (trajContent κ x₀).IsSigmaSubadditive

Tactic:
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)
  refine addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (trajContent κ x₀) (fun _ _ ↦ trajContent_ne_top) ?_ hf hf_Union hf'
  exact fun s hs anti_s inter_s ↦ trajContent_tendsto_zero hs anti_s inter_s x₀

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

Goal state before:
pp: case compl
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht : Measurable fun x₀ ↦ (trajFun κ a x₀) t
this : ∀ (x₀ : (i : ↥(Iic a)) → X ↑i), IsProbabilityMeasure (trajFun κ a x₀)
⊢ Measurable fun x₀ ↦ (trajFun κ a x₀) tᶜ

Tactic:
simpa [measure_compl mt (measure_ne_top _ _)] using Measurable.const_sub ht _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (b : β) in t, (η b) s ∂κ a ≤ ∫⁻ (a : β) in t, 1 ∂κ a

Tactic:
refine lintegral_mono ?_
        intro b
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case h₁
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
y : 𝓨
θ : Θ
⊢ ∫⁻ (y : 𝓨), ℓ θ y ∂Measure.dirac y ≤ ℓ θ y

Tactic:
rw [lintegral_dirac' _ (by fun_prop)]

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

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x

Tactic:
have h_rnDeriv ω := Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := Kernel.const Ω (κ ∘ₘ μ))
    (a := ω)
  simp only [Filter.EventuallyEq, Kernel.const_apply] at h_rnDeriv
  rw [← ae_all_iff] at h_rnDeriv
  filter_upwards [posterior_eq_withDensity Measure.absolutelyContinuous_comp_of_countable,
    h_rnDeriv] with x hx hx_all
  simp_rw [hx, hx_all]

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

Goal state before:
pp: y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, z ≤ b ∧ b ≤ y → a ≠ b

Tactic:
intros

Goal state after:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a✝² : ℝ
a✝¹ : a✝² < z
b✝ : ℝ
a✝ : z ≤ b✝ ∧ b✝ ≤ y
⊢ a✝² ≠ b✝
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

pp: case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
· classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Goal state after:
case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
this : (fun n ↦ ↑(n.choose k) * p n ^ k) ~[atTop] fun n ↦ (↑n * p n) ^ k / ↑k.factorial
⊢ Tendsto (fun n ↦ ↑(n.choose k) * p n ^ k) atTop (𝓝 (r ^ k / ↑k.factorial))

Tactic:
refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_

Goal state after:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
this : (fun n ↦ ↑(n.choose k) * p n ^ k) ~[atTop] fun n ↦ (↑n * p n) ^ k / ↑k.factorial
⊢ Tendsto (fun n ↦ (↑n * p n) ^ k / ↑k.factorial) atTop (𝓝 (r ^ k / ↑k.factorial))
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ Tendsto (fun n ↦ ↑(n.choose k) * p n ^ k) atTop (𝓝 (r ^ k / ↑k.factorial))

Tactic:
have : (fun n => n.choose k * (p n) ^ k) ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
    calc
    _ ~[atTop] (fun n => (n ^ k / k.factorial) * (p n) ^ k) :=
      (isEquivalent_choose k).mul IsEquivalent.refl
    _ ~[atTop] (fun n ↦ ((n * p n) ^ k) / k.factorial) :=
      EventuallyEq.isEquivalent (.of_eq (by ext; field))
  refine (IsEquivalent.tendsto_nhds_iff this).mpr ?_
  simpa [div_eq_mul_inv] using (hr.pow k).mul_const ((k.factorial : ℝ)⁻¹)

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 : Measure.map X ℙ = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False

Tactic:
rw [map_of_not_aemeasurable h] at hu

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 : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ False
Module: Mathlib.Probability.Distributions.Uniform

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

Tactic:
by_cases hx : x ∈ t

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

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

Goal state before:
pp: α : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ a, ⨆ n ∈ ns a, s n = ⨆ n, s n

Tactic:
rw [iSup_comm]

Goal state after:
α : 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)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
⊢ ⨆ j, ⨆ i, ⨆ (_ : j ∈ ns i), s j = ⨆ n, s n
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
restrict_apply,

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π x).restrict B) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']) →
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
intros

Goal state after:
case mp
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
a✝ :
  ∀ (s_1 : Finset ι) {f : ι → Set Ω},
    (∀ i ∈ s_1, f i = s i) →
      μ[(⋂ i ∈ s_1, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ x ∈ s_1, μ[(s x).indicator fun ω ↦ 1 | m']
S✝ : Finset ι
⊢ μ[(⋂ i ∈ S✝, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S✝, μ[(s 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Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = s
⊢ MeasurableSet s'

Tactic:
rwa [hs']

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = t
⊢ MeasurableSet s'

Tactic:
rwa [hs']

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

Goal state before:
pp: Ω : 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τ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
hi : i ∈ Set.range τ
h_top : i ≠ ⊤
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]

Tactic:
lift i to ι using h_top with i

Goal state after:
Ω : 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τ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i✝ : WithTop ι
i : ι
hi : ↑i ∈ Set.range τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) 0 = (1 - ↑p) ^ n

Tactic:
simp [binomial_apply]

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) (Fin.last n) = ↑p ^ n

Tactic:
simp [binomial_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
inst✝³ : Semiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid W
inst✝ : Module A W
ρ : Representation A G W
⊢ Function.Injective toSubmodule

Tactic:
rintro ⟨_, _⟩

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
inst✝³ : Semiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid W
inst✝ : Module A W
ρ : Representation A G W
toSubmodule✝ : Submodule A W
apply_mem_toSubmodule✝ : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule✝ → (ρ g) v ∈ toSubmodule✝
⊢ ∀ ⦃a₂ : Subrepresentation ρ⦄,
    { toSubmodule := toSubmodule✝, apply_mem_toSubmodule := apply_mem_toSubmodule✝ }.toSubmodule = a₂.toSubmodule →
      { toSubmodule := toSubmodule✝, apply_mem_toSubmodule := apply_mem_toSubmodule✝ } = a₂
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ₁ ρ₂ : Subrepresentation ρ
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule → (ρ g) v ∈ ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

Tactic:
by
      simp only [Submodule.forall_mem_sup, map_add]
      intro g x₁ hx₁ x₂ hx₂
      exact Submodule.mem_sup.mpr
        ⟨ρ g x₁, ρ₁.apply_mem_toSubmodule g hx₁, ρ g x₂, ρ₂.apply_mem_toSubmodule g hx₂, rfl⟩

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
⊢ (∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)) →
    (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')) →
      (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')) →
        ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
hmY

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')) →
    (∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')) →
      ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)