mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y Z : SFinKer
⊢ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ Kernel.deterministic Prod.swap ⋯ ∘ₖ
      Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ =
    Kernel.deterministic (Prod.map Prod.swap id) ⋯ ∘ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
      Kernel.deterministic (Prod.map id Prod.swap) ⋯
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
⊢ ‖if ω ∈ X ⁻¹' s then 1 ω else 0‖ ≤ 1

Tactic:
split_ifs with h <;> simp

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

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯) ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ (Kernel.deterministic Prod.swap ⋯ ∥ₖ Kernel.deterministic id ⋯)) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.map Prod.swap id) ⋯) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (Prod.map Prod.swap id) ⋯) ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯) ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic Function.diag ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ
        (Kernel.deterministic Function.diag ⋯ ∥ₖ Kernel.deterministic id ⋯))

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)

Tactic:
rw [Kernel.deterministic_parallelComp_deterministic]

Goal state after:
X Y : SFinKer
⊢ Kernel.deterministic Function.diag ⋯ =
    Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ
              Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc) ⋯ ∘ₖ
            Kernel.deterministic (Prod.map id (Prod.map Prod.swap id)) ⋯ ∘ₖ
          Kernel.deterministic (Prod.map id ⇑MeasurableEquiv.prodAssoc.symm) ⋯ ∘ₖ
        Kernel.deterministic ⇑MeasurableEquiv.prodAssoc ⋯ ∘ₖ
      (Kernel.deterministic (Prod.map id Function.diag) ⋯ ∘ₖ Kernel.deterministic (Prod.map Function.diag id) ⋯)
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
⊢ (Measure.map (f a) volume) (Iic x) = (κ a) (Iic x)

Tactic:
simp_rw [volume.map_apply measurable_f.of_uncurry_left measurableSet_Iic, preimage,
    mem_Iic, Iic_to_Icc, ← ofReal_measureReal (measure_ne_top (κ a) _), ← volume_Iic ⟨_, κ_in_I⟩]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
⊢ volume {x_1 | f a x_1 ≤ x} = volume (Iic ⟨(κ a).real (Icc 0 x), κ_in_I⟩)
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
⊢ κ = (κ.map g).map hg.invFun

Tactic:
rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
ω' : Ω'
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) ((κ.map Y) ω')
h_mgf : ∀ (t : ℝ), mgf X ((κ.map Y) ω') t ≤ rexp (↑c * t ^ 2 / 2)
t✝ t : ℝ
⊢ Measure.map Y (κ ω') = (κ.map Y) ω'

Tactic:
map_apply _ hY

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
ω' : Ω'
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) ((κ.map Y) ω')
h_mgf : ∀ (t : ℝ), mgf X ((κ.map Y) ω') t ≤ rexp (↑c * t ^ 2 / 2)
t✝ t : ℝ
⊢ Measure.map Y (κ ω') = Measure.map Y (κ ω')
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : ¬IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
simp [FunLike.coe_zero, hκ]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ((linearizeMap (α_ X Y Z).hom).comp (μ (X ⊗ Y) Z)).comp (rTensor (linearize k G Z) (μ X Y)) =
    ((μ X (Y ⊗ Z)).comp (lTensor (linearize k G X) (μ Y Z))).comp
      ↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))

Tactic:
by
  ext x y z : 9
  -- experiment with monoidal structure of `Action` on `Type`
  simp only [Action.tensorObj_V, types_tensorObj_def, comp_toLinearMap, μ_toLinearMap,
    toLinearMap_rTensor, LinearMap.coe_comp, Function.comp_apply,
    TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self,
    TensorProduct.curry_apply, LinearEquiv.coe_coe, LinearMap.rTensor_tmul, toLinearMap_apply,
    toLinearMap_lTensor, toLinearMap_assoc, TensorProduct.assoc_tmul, LinearMap.lTensor_tmul]
  -- after fixing the defeq problems in `Action` and in the monoidal category structure of `types`
  -- this line should close the goal so this is left as an indicator.
  convert dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)
  all_goals with_reducible simp

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
x✝³ x✝² : Rep k G
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (resFunctor f).map (x✝¹ + x✝) = (resFunctor f).map x✝¹ + (resFunctor f).map x✝

Tactic:
ext : 2; simp [add_hom]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_5.hg
Ω : 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
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ Integrable (⇑ψ ∘ X 0) μ

Tactic:
exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Goal state after:
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, ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ

Tactic:
Pi.sub_apply,

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, ∫ (ω : Ω), ‖X 0 ω - Y k 0 ω‖ ∂μ < δ
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 ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
⊢ ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero] at 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
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 ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
k : ℕ
hω : Tendsto (fun e ↦ ‖(↑e)⁻¹ • ∑ i ∈ Finset.range e, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖) atTop (𝓝 0)
hk : ∫ (ω : Ω), ‖(X 0 - Y k 0) ω‖ ∂μ < δ
this : ‖∫ (x : Ω), Y k 0 x ∂μ - ∫ (x : Ω), X 0 x ∂μ‖ < δ
I : ∀ᶠ (n : ℕ) in atTop, (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n < δ
⊢ ∀ᶠ (n : ℕ) in atTop, ‖(↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω - ∫ (x : Ω), Y k 0 x ∂μ‖ < δ
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

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
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : (Hom.hom (X.d (0 + 1))) ↑⟨x, hx'⟩ = ↑0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g

Tactic:
simp only [Nat.reduceAdd, d_succ, d_zero, ConcreteCategory.hom_ofHom, hom_sub,
      ContIntertwiningMap.sub_apply, coind₁ι_toFun, coind₁Map_toFun, ZeroMemClass.coe_zero,
      sub_eq_zero, ContinuousMap.const_apply] at hx ⊢

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
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
g : G
hx : ContinuousMap.const G x = (↑X.ρ.coind₁ι).comp x
⊢ x 1 = x g
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
have nat := η.hom.hom.naturality mulRepHom
  have tensor (X Y) : η.hom.hom.app (X ⊗ Y) = (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y) :=
    η.hom.isMonoidal.tensor X Y
  rw [tensor] at nat
  exact ConcreteCategory.congr_hom ((CategoryTheory.forget _).congr_map nat) (f ⊗ₜ[k] g)

Goal state after: