mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Integrable (fun x ↦ ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)) (volume.restrict (Ioc 0 1))

Tactic:
convert! betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Integrable (fun x ↦ ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)) (volume.restrict (Ioc 0 1)) ↔
    IntervalIntegrable (fun x ↦ ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)) volume 0 1
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∑' (x : α), s.indicator (⇑p) x = 1

Tactic:
classical suffices ∀ (x) (_ : x ∉ s), p x = 0 from
      _root_.trans (tsum_congr
        fun a => (Set.indicator_apply s p a).trans
          (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe

Goal state after:
case refine_2
α : Type u_1
p : PMF α
s : Set α
h : p.support ⊆ s
⊢ ∀ x ∉ s, p x = 0
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
⊢ Measure.map (fun a ↦ ((f ∘ Z) a, Y a)) P = Measure.map (Prod.map f id) (Measure.map (fun a ↦ (Z a, Y a)) P)

Tactic:
by
        rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
        rfl

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

Goal state before:
pp: case neg.left
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ AEStronglyMeasurable (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

pp: case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ HasFiniteIntegral (fun x ↦ x * (pdf X ℙ volume x).toReal) volume

Tactic:
· exact aestronglyMeasurable_id.mul
      (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable

Goal state after:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
⊢ HasFiniteIntegral (fun x ↦ x * (pdf X ℙ volume x).toReal) volume
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
let f₁ := fun (x : X) ↦ (PUnit.unit, x)

Goal state after:
X : SFinKer
f₁ : X.carrier → PUnit.{?u.96 + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
⊢ { carrier := { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier × X.carrier,
      str := Prod.instMeasurableSpace } ≅
    X
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = (⇑π ∘ₘ μ) (A ∩ B)

Tactic:
Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), (π a) (A ∩ B) ∂μ
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ { carrier := X.carrier × { carrier := PUnit.{u + 1}, str := PUnit.instMeasurableSpace }.carrier,
      str := Prod.instMeasurableSpace } ≅
    X

Tactic:
by
    let f₁ := fun (x : X) ↦ (x, PUnit.unit)
    have hf₁ : Measurable f₁ := by fun_prop
    have hf₂ : Measurable (Prod.fst : X × PUnit → X) := by fun_prop
    refine ⟨⟨Kernel.id.map Prod.fst, by infer_instance⟩,
      ⟨Kernel.id.map f₁, by infer_instance⟩, ?_, ?_⟩
    · ext : 1; dsimp
      rw [Kernel.id_map hf₁, Kernel.deterministic_comp_eq_map hf₁, Kernel.id_map hf₂,
        Kernel.deterministic_map hf₂ hf₁]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]
    · ext : 1; dsimp
      rw [Kernel.id_map hf₂, Kernel.deterministic_comp_eq_map hf₂, Kernel.id_map hf₁,
        Kernel.deterministic_map hf₁ hf₂]
      ext : 1
      simp [Kernel.deterministic_apply, Kernel.id_apply, f₁]

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

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h✝ : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
h_ne_top : ((condExpKernel μ m') ω) (s ∩ t) ≠ ∞
⊢ ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t

Tactic:
rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq,
      ← ENNReal.toReal_mul, ENNReal.ofReal_toReal]

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h✝ : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
h_ne_top : ((condExpKernel μ m') ω) (s ∩ t) ≠ ∞
⊢ ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t ≠ ∞
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_4.f
Ω : 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']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
exact hg i hi

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

Goal state before:
pp: case e'_5.a
Ω : 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']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
exact hg i hi

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 ι
i : ι
hi : ↑i ∈ Set.range τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f n | hτ.measurableSpace]

Tactic:
exact stoppedValue_ae_eq_restrict_eq h _ hτ_le i

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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : ∀ (n : ℤ), ∀ᵐ (ω' : Ω') ∂ν, Integrable (fun ω ↦ rexp (↑n * X ω)) (κ ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')

Tactic:
rw [← ae_all_iff] at h_int

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), Integrable (fun ω ↦ rexp (↑i * X ω)) (κ a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
filter_upwards [this] with ω hω

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
ω : Ω
hω : edist (X s ω) (X t ω) ^ p = 0 ω
⊢ edist (X s ω) (X t ω) = 0
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
filter_upwards [this] with ω hω

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
ω : Ω
hω : edist (X s ω) (X t ω) ^ p = 0 ω
⊢ edist (X s ω) (X t ω) = 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') {ω | 0 < X ω} = 0

Tactic:
have hs : {ω | 0 < X ω} = ⋃ ε : {ε : ℚ // 0 < ε}, {ω | ε ≤ X ω} := by
    ext ω
    simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Subtype.exists, exists_prop]
    constructor
    · intro hp
      obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
      exact ⟨q, (q.cast_pos.1 h1), h2.le⟩
    · intro ⟨q, h1, h2⟩
      exact lt_of_lt_of_le (q.cast_pos.2 h1) h2
  have hb (ε : ℚ) : ∀ᵐ ω' ∂ν, 0 < ε → (κ ω') {ω | ε ≤ X ω} = 0 := by
    filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
    simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm
    suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
    have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
    apply le_antisymm
    · exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)
    · exact measureReal_nonneg
  /- `ν`-almost everywhere, `{ω | 0 < X ω}` is a countable union of `κ ω'`-null sets. -/
  filter_upwards [ae_all_iff.2 hb] with ω' hn
  simp only [hs, measure_iUnion_null_iff, Subtype.forall]
  exact fun _ ↦ hn _

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ IntegrableOn (fun x ↦ (↑i + 1) * 1) (Set.Ioc ↑i ↑(i + 1)) ρ

pp: case h.hg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ IntegrableOn (fun x ↦ x + 1) (Set.Ioc ↑i ↑(i + 1)) ρ

pp: case h.hs
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ MeasurableSet (Set.Ioc ↑i ↑(i + 1))

pp: case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ ∀ x ∈ Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ≤ x + 1

Tactic:
· exact continuous_const.integrableOn_Ioc

Goal state after:
case h.hg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ IntegrableOn (fun x ↦ x + 1) (Set.Ioc ↑i ↑(i + 1)) ρ

case h.hs
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ MeasurableSet (Set.Ioc ↑i ↑(i + 1))

case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ ∀ x ∈ Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ≤ x + 1
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ Tendsto (fun N ↦ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))

Tactic:
refine tendsto_finsetSum _ fun i _ => ?_

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ Tendsto (fun N ↦ ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ {ω | X ω ∈ Set.Ioi ↑i}))
Module: Mathlib.Probability.StrongLaw

Goal state before:

Tactic:
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.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝⁸ : Semiring k
G : Type v
inst✝⁷ : Monoid G
V : Type v'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module k V
W : Type w'
inst✝⁴ : AddCommMonoid W
inst✝³ : Module k W
H : Type w
inst✝² : Subsingleton H
inst✝¹ : MulOneClass H
inst✝ : MulAction G H
g : G
a : H
⊢ ((↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g) ∘ₗ MonoidAlgebra.lsingle a) 1 =
    (((trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)) ∘ₗ MonoidAlgebra.lsingle a) 1

Tactic:
simp [Subsingleton.elim (g • a) a]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω), (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n

Tactic:
filter_upwards [B] with ω hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S✝ : Subgroup G
inst✝¹ : S✝.Normal
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ (X.ρ.quotientToInvariants S) ↑g =
    (Y.ρ.quotientToInvariants S) ↑g ∘ₗ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
ext; simp [hom_comm_apply]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
      (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))

Tactic:
filter_upwards [this] with ω hω

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
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, s.indicator (Function.const E c) (X i ω)) atTop
    (𝓝 (∫ (x : Ω), s.indicator (Function.const E c) (X 0 x) ∂μ))
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
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ Hom.hom f = Hom.hom g

Tactic:
by ext1; dsimp; ext h; simpa using hfg h

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x : (ρ.tprod (leftRegular k G)).Coinvariants
⊢ ρ.coinvariantsTprodLeftRegularLEquiv x = ρ.ofCoinvariantsTprodLeftRegular x

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : (coinvariantsFunctor k G).obj X ⟶ Y
⊢ (Hom.hom (((coinvariantsAdjunction k G).homEquiv X Y) f)).toLinearMap =
    ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ f)

Tactic:
by
  rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
      ((X.toCoinvariants S).ρ.ofQuotient S) ↑g =
    ((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
      ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
ext; simp [hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
x : (A ⊗ free k G α).ρ.Coinvariants
⊢ (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x

Tactic:
by
  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
f : A ⟶ B
r : k
g : B ⟶ C
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by
  ext; simp [hom_smul, ContIntertwiningMap.smul_comp]

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ π₂ : ContRepresentation R G V
x✝ : (fun π ↦ ⇑π.toMonoidHom) π₁ = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ π₁ = π₂

Tactic:
cases π₁; cases π₂; simp_all

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

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
⊢ A.applyAsHom g ≫ f = f ≫ B.applyAsHom g

Tactic:
ext; simp [hom_comm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max (max u v) w, u, v} k G
f : coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B
⊢ ((coindResAdjunction k S).homEquiv A B) f = (indResHomEquiv S.subtype A B) (A.indCoindIso.hom ≫ f)

Tactic:
by
  rfl

Goal state after: