mathlib-initiative/mathlib-tactics huggingface dataset:
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 α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : γ), κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)

Tactic:
← setIntegral_univ,

Goal state after:
α : 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
⊢ ∫ (x : γ) in univ, κ.density ν a x s ∂ν a = (κ a).real (univ ×ˢ s)
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 Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernel = κ

Tactic:
rw [condKernel_def]; split_ifs with hα <;> exact disintegrate _ _

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

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 α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel

Tactic:
have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a
  simp_rw [Kernel.fst_apply, Kernel.const_apply] at h
  filter_upwards [h] with b hb using hb

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

Goal state before:

Tactic:
setBer(u, p) {s}
    _ = ∏' i, ((if i ∈ u ↔ i ∈ s then (toNNReal p : ℝ≥0∞) else 0) +
          if i ∈ s then 0 else (toNNReal (σ p) : ℝ≥0∞)) := by
      simp [setBernoulli_apply, Set.image_singleton, Set.indicator]
    _ = ∏ i ∈ u, (if i ∈ s then (toNNReal p : ℝ≥0∞) else (toNNReal (σ p) : ℝ≥0∞)) := by
      rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]
    _ = toNNReal p ^ s.ncard * toNNReal (σ p) ^ (↑u \ s).ncard := by
      simp [Finset.prod_ite, ← Set.ncard_coe_finset, Set.ofPred_and,
        Set.inter_eq_right.2 hsu, ← Set.compl_ofPred, Set.sdiff_eq_compl_inter, Set.inter_comm]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x =
    ∏ x ≤ b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x

Tactic:
nth_rw 1 [Eq.comm, ← Iic_union_Ioc_eq_Iic hab, prod_union (Iic_disjoint_Ioc le_rfl)]

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
⊢ (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    (∏ x ≤ a, Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x) *
      ∏ x ∈ Ioc a b, Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 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 α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = (κ a) (κ.mutuallySingularSetSlice η a)ᶜ
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
exact withDensity_rnDeriv_eq_zero_iff_apply_eq_zero κ η a

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ (η.withDensity (κ.rnDeriv η) + κ.singularPart η) ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0

Tactic:
compProd_add_right,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝³ : IsFiniteKernel κ
inst✝² : IsFiniteKernel η
inst✝¹ : MeasurableSpace.CountableOrCountablyGenerated α β
inst✝ : SFinite μ
h : μ ⊗ₘ η.withDensity (κ.rnDeriv η) + μ ⊗ₘ κ.singularPart η ≪ ν ⊗ₘ η
⊢ ∀ᵐ (a : α) ∂μ, (κ.singularPart η) a = 0
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
s' : Finset ↑s
⊢ MeasurableSet ((↑s').pi fun i ↦ t ↑i)

Tactic:
by apply MeasurableSet.pi (countable_toSet _) (by measurability)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ μ.toPMF.toMeasure s = μ s

Tactic:
rw [μ.toPMF.toMeasure_apply hs, ← μ.tsum_indicator_apply_singleton s hs]
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p.toMeasure = μ.toPMF.toMeasure

Tactic:
Measure.toPMF_toMeasure

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p.toMeasure = μ
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toPMF.toMeasure = p.toMeasure ↔ μ = p.toMeasure

Tactic:
Measure.toPMF_toMeasure

Goal state after:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ = p.toMeasure ↔ μ = p.toMeasure
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ ↑(cdf (gammaMeasure a r)) x = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x

Tactic:
rw [cdf_eq_real, gammaMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
⊢ (∫⁻ (a_1 : ℝ) in Iic x, gammaPDF a r a_1).toReal = ∫ (x : ℝ) in Iic x, gammaPDFReal a r x
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), s.indicator (⇑(pure a)) x = 1

Tactic:
refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)

Goal state after:
case pos
α : Type u_1
a : α
s : Set α
ha : a ∈ s
b : α
⊢ s.indicator (⇑(pure a)) b = if b = a then 1 b else 0
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

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

Tactic:
refine ENNReal.tsum_comm.trans (_root_.trans (tsum_congr fun a => ?_) p.tsum_coe)
    simp_rw [ENNReal.tsum_mul_left]
    split_ifs with h
    · simp only [h, zero_mul]
    · rw [(f a h).tsum_coe, mul_one]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
r : ℝ≥0
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∫ (x : R), f x ∂Po(R, r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
integral_map .of_discrete .of_discrete,

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
r : ℝ≥0
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ (Measure.map X μ).prod (Measure.map Y μ) = (Measure.map Z ν).prod (Measure.map W ν)

Tactic:
hXZ.map_eq,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
⊢ (Measure.map Z ν).prod (Measure.map Y μ) = (Measure.map Z ν).prod (Measure.map W ν)
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
MeasurableSpace.comap_id

Goal state after:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ
Module: Mathlib.Probability.Independence.ZeroOne

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

Tactic:
specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
    (measurableSet_generateFrom (Set.mem_singleton t))

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
Module: Mathlib.Probability.Independence.Conditional

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

Tactic:
exact h_eq' s f H

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX)
    (aemeasurable_pi_lambda _ mY)]
  refine eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert! h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: case refine_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        μ[(f ⁻¹' s ∩ g ⁻¹' t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] fun ω ↦
          μ[(f ⁻¹' s).indicator fun ω ↦ 1 | m'] ω * μ[(g ⁻¹' t).indicator fun ω ↦ 1 | m'] ω
s t : Set Ω
⊢ MeasurableSet s →
    MeasurableSet t →
      μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
· rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
    exact h s t hs ht

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
(h_sets i hi).choose_spec.2.symm

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
i : ι
hi : i ∈ s
⊢ f i ⁻¹' Exists.choose ⋯ = f i ⁻¹' g i
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      Measure.map (fun ω ↦ (k ω, g ω)) μ ⊗ₘ Kernel.prodMkRight β' (condDistrib f k μ)

Tactic:
condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hg hf hk,

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      Measure.map (fun ω ↦ (k ω, g ω)) μ ⊗ₘ Kernel.prodMkRight β' (condDistrib f k μ)
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
tilted_mul_apply_eq_ofReal_integral_mgf' hs,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)
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✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation ρ
c : A[G]
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
⊢ c • v ∈ σ.toSubmodule.carrier

Tactic:
by
    induction c using MonoidAlgebra.induction_linear with
    | zero => simp [zero_smul]
    | add x y hx hy => rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy
    | single g a =>
      rw [Representation.single_smul]
      exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)

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)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ (∫ (x : Ω), rexp (t * X x * ↑p) ∂κ ω') ^ (1 / ↑p) * (∫ (x : Ω), rexp (t * Y x * ↑q) ∂κ ω') ^ (1 / ↑q) ≤
    rexp (↑cX * (t * ↑p) ^ 2 / 2) ^ (1 / ↑p) * rexp (↑cY * (t * ↑q) ^ 2 / 2) ^ (1 / ↑q)

Tactic:
mul_right_comm t _ p,

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)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ (∫ (x : Ω), rexp (t * ↑p * X x) ∂κ ω') ^ (1 / ↑p) * (∫ (x : Ω), rexp (t * Y x * ↑q) ∂κ ω') ^ (1 / ↑q) ≤
    rexp (↑cX * (t * ↑p) ^ 2 / 2) ^ (1 / ↑p) * rexp (↑cY * (t * ↑q) ^ 2 / 2) ^ (1 / ↑q)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
⊢ A ∈ Set.Ioi |f x| → f x = truncation f A x

Tactic:
hA

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
hA : A ∈ Set.Ioi |f x|
⊢ f x = truncation f A x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf X μ t * mgf Y μ t ≤ rexp (↑cX * t ^ 2 / 2) * rexp (↑cY * t ^ 2 / 2)

Tactic:
by
      gcongr
      · exact mgf_nonneg
      · exact hX.mgf_le t
      · exact hY.mgf_le t

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
γ : G
⊢ ∀ (v : V), (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ γ) v) = (τ γ) ((f.toLinearMap ∘ₗ g.toLinearMap) v)

Tactic:
v

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
γ : G
v : V
⊢ (f.toLinearMap ∘ₗ g.toLinearMap) ((ρ γ) v) = (τ γ) ((f.toLinearMap ∘ₗ g.toLinearMap) v)
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
g' : G
⊢ ∀ (v : V), (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)

Tactic:
v

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
g' : G
v : V
⊢ (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ ModuleCat.ofHom (W.ρ g) =
    (((Action.forget (FGModuleCat R) G).mapIso i).inv ≫ V.ρ g ≫ ((Action.forget (FGModuleCat R) G).mapIso i).hom).hom

Tactic:
dsimp only [Action.forget_map, Functor.mapIso_hom]

Goal state after:
R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ ModuleCat.ofHom (W.ρ g) = (((Action.forget (FGModuleCat R) G).mapIso i).inv ≫ V.ρ g ≫ i.hom.hom).hom