mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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
hu : IsUniform X s ℙ μ
⊢ Measure.map X ℙ ≪ μ

Tactic:
rw [hu]; exact ProbabilityTheory.cond_absolutelyContinuous

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 ℙ μ
A : Set E
hA : MeasurableSet A
⊢ ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s

Tactic:
by
  rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply',
    ENNReal.div_eq_inv_mul]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ a ∉ s, (if a ∈ s then (↑(#s))⁻¹ else 0) = 0

Tactic:
· exact fun x hx => by simp only [hx, if_false]

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

Goal state before:
pp: case refine_1
Ω : 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σ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this✝ : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ stoppedValue f σ =ᵐ[μ] μ[f n | hσ.measurableSpace]

pp: case refine_2
Ω : 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σ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this✝ : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ hσ.measurableSpace ≤ hτ.measurableSpace

Tactic:
· exact h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ
      (fun x => (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range

Goal state after:
case refine_2
Ω : 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σ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this✝ : SigmaFinite (μ.trim ⋯)
this : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ] μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace]
⊢ hσ.measurableSpace ≤ hτ.measurableSpace
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ

Tactic:
setIntegral_tilted,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
⊢ ∫ (x : Ω) in s, (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ =
    ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g 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 ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ μ[stoppedValue f τ | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
rw [h1]

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 ⋯)
h1 : μ[stoppedValue f τ | hτ.measurableSpace] = stoppedValue f τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[stoppedValue f τ | hσ.measurableSpace]
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ HasSubgaussianMGF X c 0 ν

Tactic:
by
  constructor
  · simp [FunLike.coe_zero]
  · simp [exp_nonneg]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ

Tactic:
apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable
  exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Tactic:
exact hf.memLp_truncation

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: case e'_2
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle y) 1) ⊗ₜ[k]
        (MonoidAlgebra.lsingle z) 1) =
    MonoidAlgebra.single ((x, y), z) 1

Tactic:
with_reducible simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: case e'_3
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k]
        (MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle y) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle z) 1)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (α_ X Y Z).hom.hom) ((x, y), z)) 1

Tactic:
with_reducible simp

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∑ k ∈ range K, ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ

Tactic:
by
      gcongr with k
      have Ik : (k : ℝ) ≤ (k + 1 : ℕ) := by simp
      rw [← intervalIntegral.integral_const_mul, intervalIntegral.integral_of_le Ik,
        intervalIntegral.integral_of_le Ik]
      refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · apply Continuous.integrableOn_Ioc (by fun_prop)
      · calc
          2 / (↑k + 1) * x ^ 2 = x / (k + 1) * (2 * x) := by ring
          _ ≤ 1 * (2 * x) := by
              have : 0 < x := k.cast_nonneg.trans_lt hx.1
              gcongr
              exact (div_le_one <| by positivity).2 <| mod_cast hx.2
          _ = 2 * x := by rw [one_mul]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
⊢ HasSubgaussianMGF id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, fun t ↦ ?_⟩⟩
  · rw [← Function.id_comp X]
    exact .of_map hX h
  · rw [integrable_map_measure (by fun_prop) hX]
    exact h.integrable_exp_mul t
  · rw [mgf_id_map hX]
    exact h.mgf_le t

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

Goal state before:
pp: case hf
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ StronglyMeasurable fun ω ↦ rexp (t * X ω)

Tactic:
· exact Measurable.stronglyMeasurable <| by fun_prop

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
⊢ ∀ᵐ (ω : Ω),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊

Tactic:
have I1 : ∀ K, ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * Var[Y j] ≤ 2 * 𝔼[X 0] := by
    intro K
    calc
      ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * Var[Y j] ≤
          ∑ j ∈ range K, ((j : ℝ) ^ 2)⁻¹ * 𝔼[truncation (X 0) j ^ 2] := by
        gcongr with j
        rw [(hident j).truncation.variance_eq]
        exact variance_le_expectation_sq (hX 0).truncation
      _ ≤ 2 * 𝔼[X 0] := sum_variance_truncation_le hint (hnonneg 0) K

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
⊢ ∀ᵐ (ω : Ω),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : IsProbabilityMeasure μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h =>
    simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
    have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
    refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
    · exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)
    · convert! h_indep'
      rw [Finset.sum_apply]

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

Goal state before:

Tactic:
_ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]

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
ω : Ω
⊢ X ω ∈ Set.Icc a b → X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)

Tactic:
hab

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
ω : Ω
hab : X ω ∈ Set.Icc a b
⊢ X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        v i * ↑⌊c ^ n⌋₊
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a‖ ≤
      ε * ‖↑⌊c ^ x⌋₊‖

Tactic:
obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        v i * ↑⌊c ^ n⌋₊
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a‖ ≤
      ε * ‖↑⌊c ^ x⌋₊‖
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
⊢ ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε

Tactic:
have : ‖μ[Y k 0] - μ[X 0]‖ < δ := by
    rw [norm_sub_rev, ← integral_sub hint]
    · exact (norm_integral_le_integral_norm _).trans_lt hk
    · exact ((φ k).comp (X 0) h'.measurable).integrable_of_isFiniteMeasure

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝¹ : SeparableSpace ↑s
this✝ : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
⊢ ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < ε
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ ↑(of ρ) = X

Tactic:
by with_reducible rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ (of ρ).ρ = ρ

Tactic:
by with_reducible rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext; simp [hom_smul, ContIntertwiningMap.comp_smul]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ ↑(of ρ) = X

Tactic:
by with_reducible rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ (of ρ).ρ = ρ

Tactic:
by with_reducible rfl

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

Goal state before:
pp: 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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d i (i + 1))) σ) = (Hom.hom (X.d (i + 1))) ↑σ

Tactic:
homogeneousCochains.d_eq

Goal state after:
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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom ((invariantsFunctor k G).map (X.d (i + 1)))) σ) = (Hom.hom (X.d (i + 1))) ↑σ
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Tactic:
simp [indToCoindAux_of_not_rel (h := h)]

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

Goal state before:
pp: case refine_1.succ
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α) ∈ ↑(ρ g - LinearMap.id).range

Tactic:
use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _

Goal state after: