mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Indep (limsup s atBot) (limsup s atBot) κ μα

Tactic:
refine indep_limsup_self h_le h_indep ?_ ?_ hnsp ?_

Goal state after:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot

case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) ns

case refine_3
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
⊢ ∀ (n : ι), ∃ a, n ∈ ns a
Module: Mathlib.Probability.Kernel.Invariance

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ ⇑(κ ∘ₖ η) ∘ₘ μ = μ

Tactic:
← Measure.comp_assoc,

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ ⇑κ ∘ₘ ⇑η ∘ₘ μ = μ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s_1 ∈ {s i}, MeasurableSet s_1

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom (prodAssoc a✝).1).prod ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2))) s✝

Tactic:
rw [Measure.prod_apply hs, Measure.prod_apply (by measurability), lintegral_prod]

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ ∫⁻ (x : Y₁✝.carrier),
      ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (x, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 ∂κ₁.hom a✝.1.1 =
    ∫⁻ (x : Y₁✝.carrier),
      ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2)) (Prod.mk x ⁻¹' s✝) ∂κ₁.hom (prodAssoc a✝).1

case hf
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ AEMeasurable (fun x ↦ (η.hom a✝.2) (Prod.mk x ⁻¹' ⇑prodAssoc ⁻¹' s✝)) ((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2))
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
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✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P

Tactic:
convert! h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩) g

Goal state after:
case e'_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
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✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x✝ =
    ((∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝) * g (U x✝)

case e'_3
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
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✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ s, ⇑(f s) ∘ X s) x✝ =
    (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝
Module: Mathlib.Probability.Independence.Conditional

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

Tactic:
condIndepFun_iff_condIndep,

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
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 ∈ s, sets i = f i ⁻¹' g i

Tactic:
intro i hi

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
⊢ sets i = f i ⁻¹' g i
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_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
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
⊢ ∀ i ∈ Set.range τ, stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]

Tactic:
intro i hi

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
ι : Type u_3
inst✝⁶ : LinearOrder ι
inst✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
hi : i ∈ Set.range τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: Y : Type u_2
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
μ : Measure Y
inst✝ : IsProbabilityMeasure μ
f : Unit → ↑I → Y
hf_meas : Measurable (uncurry f)
hf_map : map (f ()) volume = (Kernel.const Unit μ) ()
⊢ map (f ()) volume = μ

Tactic:
simpa

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✝⁹ : 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 ⋯)
⊢ μ[stoppedValue f τ | hσ.measurableSpace ⊓ hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
    μ[stoppedValue f τ | ⋯.measurableSpace]

Tactic:
IsStoppingTime.measurableSpace_min hτ hσ,

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

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1),
    (if h : x < n + 1 then p ^ ↑⟨x, h⟩ * (1 - p) ^ (n - ↑⟨x, h⟩) * ↑(n.choose ↑⟨x, h⟩) else 0) =
      p ^ x * (1 - p) ^ (n - x) * ↑(n.choose x)

Tactic:
intro i hi

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
⊢ binomial p h 1 = map (fun x ↦ bif x then 1 else 0) (bernoulli p h)

Tactic:
ext i; fin_cases i <;> simp [binomial_apply, bernoulli_apply]

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
⊢ 1 - ↑x ≥ 0

Tactic:
simpa

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 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

Tactic:
by_cases h0 : κ ω' = 0

Goal state after:
case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : κ ω' = 0
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : ¬κ ω' = 0
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(deterministic X hX ∘ₖ κ) ∘ₘ ν)

Tactic:
← Measure.comp_assoc,

Goal state after:
case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(deterministic X hX) ∘ₘ ⇑κ ∘ₘ ν)
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Ω
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : Zero E
hp : p X
⊢ ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < (fun n x ↦ ⊤) n ω}.indicator (X i)) ((fun n x ↦ ⊤) n))

Tactic:
simpa

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ |f a|

Tactic:
filter_upwards with A
    filter_upwards with x
    rw [Real.norm_eq_abs]
    exact abs_truncation_le_abs_self _ _ _

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : HasSubgaussianMGF X c μ
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
h2 : ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
simpa

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : HasSubgaussianMGF X c μ
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
h2 : ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
simpa

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ X =ᵐ[⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ()] Y

Tactic:
simpa

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
⊢ ∀ i ∈ Finset.range n, HasSubgaussianMGF (X i) c μ

Tactic:
simpa

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m) (⇑(Kernel.const Unit (μ.trim hm)) ∘ₘ Measure.dirac ())

Tactic:
simpa

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
⊢ ∀ᵐ (ω : Ω),
    (fun n ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
          ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
      fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
by
  obtain ⟨v, -, v_pos, v_lim⟩ :
      ∃ v : ℕ → ℝ, StrictAnti v ∧ (∀ n : ℕ, 0 < v n) ∧ Tendsto v atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
  have := fun i => strong_law_aux1 X hint hindep hident hnonneg c_one (v_pos i)
  filter_upwards [ae_all_iff.2 this] with ω hω
  apply Asymptotics.isLittleO_iff.2 fun ε εpos => ?_
  obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
  filter_upwards [hω i] with n hn
  simp only [Real.norm_eq_abs, Nat.abs_cast]
  exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))

Goal state after:
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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
this : (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1)) = (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1)
⊢ (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1) = (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1))

Tactic:
← this

Goal state after:
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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
this : (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1)) = (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1)
⊢ (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1)) = (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1))
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✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
i : α
x : ↑A
⊢ (A.coinvariantsTensorFreeToFinsupp α ∘ₗ A.finsuppToCoinvariantsTensorFree α) (single i x) = LinearMap.id (single i x)

Tactic:
simp [finsuppToCoinvariantsTensorFree_single,
        coinvariantsTensorFreeToFinsupp_mk_tmul_single]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X Y : Rep k G
f g : X ⟶ Y
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (f + g) =
    (forget₂ (Rep k G) (ModuleCat k)).map f + (forget₂ (Rep k G) (ModuleCat k)).map g

Tactic:
by ext1; simp [add_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mp
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
symm; simpa [Nonempty.intro (Iso.refl V), inv_mul_eq_one₀] using char_orthonormal V V

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (x✝¹ + x✝) = X✝ ◁ x✝¹ + X✝ ◁ x✝

Tactic:
by ext1; simp [add_hom]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ (x✝¹ + x✝) ▷ X✝ = x✝¹ ▷ X✝ + x✝ ▷ X✝

Tactic:
by ext1; simp [add_hom]

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i j : ℕ
hij : i + 1 = j
⊢ invariantsResMap (↑φ) (resolutionMap φ f (i + 1)) ≫ Y.homogeneousCochains.d i j =
    X.homogeneousCochains.d i j ≫ invariantsResMap (↑φ) (resolutionMap φ f (j + 1))

Tactic:
by
    subst hij
    rw [homogeneousCochains.d_eq, homogeneousCochains.d_eq, ← invariantsResMap_comp,
      resolutionMap_comp_d, invariantsResMap_map_comp]

Goal state after: