mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ avgRisk ℓ P κ π ≤ ↑C

Tactic:
refine (avgRisk_le_mul' P κ π hℓC).trans ?_

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C
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)
n : ℕ
x : (i : ↥(Iic n)) → X ↑i
x✝¹ : (i : ℕ) → X i
x✝ : ℕ
⊢ updateFinset x✝¹ (Iic n) x x✝ = (⇑(IicProdIoi n) ∘ Prod.mk x ∘ (Set.Ioi n).domRestrict) x✝¹ x✝

Tactic:
simp [IicProdIoi, updateFinset]

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

Goal state before:
pp: Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst✝ : SFinite π
⊢ bayesRisk ℓ (Kernel.discard Θ) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π

Tactic:
Kernel.discard_eq_const,

Goal state after:
Θ : Type u_1
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
π : Measure Θ
inst✝ : SFinite π
⊢ bayesRisk ℓ (Kernel.const Θ (Measure.dirac PUnit.unit)) π = ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: case refine_2
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
h2 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
hs : MeasurableSet s
t : Set 𝓧
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) =
    ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ)

Tactic:
rw [h1 hs ht, h2 hs ht]

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
Measure.ae_ae_comm

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (y : Ω) ∂μ, ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x y = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) y x

Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ MeasurableSet {x | (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.1 x.2 = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.2 x.1}
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
b : α
⊢ ((if b = a then p b else 0) + if b = a then 0 else p b) = p b

Tactic:
split_ifs <;> simp only [zero_add, add_zero]

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

Goal state before:
pp: case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
rw [← ht0] at h

Goal state after:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))
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✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
integrable_map_cast_poissonMeasure_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
⊢ (p.bindOnSupport fun a x ↦ f a) = p.bind f

Tactic:
ext b
  have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b :=
    fun a => ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)
  simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite,
    mul_zero, this]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ Y =ᵐ[μ] X

Tactic:
by filter_upwards [hXY] with ω hω; simp [hω]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ 1 - Y =ᵐ[μ] 1 - X

Tactic:
by filter_upwards [hXY] with ω hω; simp [hω]

Goal state after:
Module: Mathlib.Probability.HasCondDistrib

Goal state before:

Tactic:
P.map (fun a ↦ ((X a, Y a), Z a))
  _ = (P.map X ⊗ₘ (κ ⊗ₖ η)).map MeasurableEquiv.prodAssoc.symm := by
      rw [← h.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
      rfl
  _ = P.map X ⊗ₘ κ ⊗ₘ η := Measure.compProd_assoc
  _ = P.map (fun a ↦ (X a, Y a)) ⊗ₘ η := by simp [h.fst.map_eq]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s))) / ↑s.card

Tactic:
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]

Goal state after:
α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ∑' (x : α), t.indicator (⇑(ofMultiset s hs)) x =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x ↦ x ∈ t) s)) * (↑s.card)⁻¹
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ κ ≫ ε = ε

Tactic:
ext : 2; simp

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 : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Tactic:
by
  by_cases hin : i ≤ n
  · refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
    refine condExp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_le hτ_le)
      (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_
    rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
  · suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
    ext1 x
    simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false]
    contrapose hin
    exact_mod_cast hin ▸ hτ_le x

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
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Tactic:
Filter.EventuallyEq,

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
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | τ x = ↑i}, stoppedValue f τ x = f i x
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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
Filter.EventuallyEq,

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✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ.restrict {x | τ x ≤ σ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)

Tactic:
have eq0 : k % (b + 1) = k := by simpa using Order.lt_add_one_iff.mpr hb

Goal state after:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) = (binomial x h b) (Fin.ofNat (b + 1) k)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
⊢ IsStable 𝓕 fun Y ↦ Locally p 𝓕 Y P

Tactic:
refine fun X hX τ hτ ↦ ⟨hX.localSeq, hX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩
  simp_rw [← stoppedProcess_indicator_comm', Set.indicator_indicator, Set.inter_comm,
    ← Set.indicator_indicator, stoppedProcess_stoppedProcess, inf_comm,
    stoppedProcess_indicator_comm', ← stoppedProcess_stoppedProcess]
  exact hp _ (hX.stoppedProcess_localSeq n) τ hτ

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 : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ X =ᵐ[⇑κ ∘ₘ ν] 0

Tactic:
Filter.EventuallyEq,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ ν, X x = 0 x
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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 ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • v ∈ σ.toSubmodule.carrier
hy : y • v ∈ σ.toSubmodule.carrier
⊢ (x + y) • v ∈ σ.toSubmodule.carrier

Tactic:
rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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 (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ (x + y) • m ∈ σ.toSubmodule.carrier

Tactic:
rw [add_smul]; exact σ.toSubmodule.add_mem' hx hy

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
j : ℕ
hj : j ∈ range K
k : ℕ
a✝ : k ∈ Set.Ico j N
⊢ IntervalIntegrable (fun x ↦ 1) ρ ↑k ↑(k + 1)

Tactic:
exact continuous_const.intervalIntegrable _ _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ IntervalIntegrable (fun x ↦ 1) ρ 0 ↑N

Tactic:
exact continuous_const.intervalIntegrable _ _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} = ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ)

Tactic:
simp_rw [B]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) ((‖b - a‖₊ / 2) ^ 2) μ

Tactic:
by
  rw [← sub_sub_sub_cancel_right b a μ[X]]
  apply hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (hm.sub_const _)
  · filter_upwards [hb] with ω hab using by simpa using hab
  · simp [integral_sub (Integrable.of_mem_Icc a b hm hb) (integrable_const _)]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V : FDRep k G
this : Invertible ↑(Fintype.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g = ↑(finrank k ↥(invariants V.ρ))

Tactic:
← (isProj_averageMap V.ρ).trace

Goal state after:
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V : FDRep k G
this : Invertible ↑(Fintype.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g = (trace k ↑V.V) (averageMap V.ρ)
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
h : H
⊢ ↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h = (Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)

Tactic:
by ext; simp [homEquiv]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
f : M ⟶ N
r : k
g : N ⟶ O
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext
  simp [smul_hom, Representation.IntertwiningMap.smul_comp]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - X.d (n + 1) ≫ (coind₁Functor k G).map (X.d (n + 1)) = 0

Tactic:
d_succ

Goal state after:
case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
inst✝² : CommRing k
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
x : ↑A
y : ↑B
⊢ (ConcreteCategory.hom (coinvariantsTensorIndHom φ A B))
      ((((ind φ A).coinvariantsTensorMk B) ((IndV.mk φ A.ρ h) x)) y) =
    ((A.coinvariantsTensorMk (res φ B)) x) ((B.ρ h) y)

Tactic:
by
  simp [coinvariantsTensorIndHom, coinvariantsTensorMk]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x =
      (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x -
        (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom A.norm).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x =
      (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x y : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x -
        (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ Function.Injective ⇑(algebraMap A L)

Tactic:
IsScalarTower.algebraMap_eq A K L

Goal state after:
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))