mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
Kernel.parallelComp_apply

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✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom (prodAssoc a✝).1).prod ((κ₂.hom ∥ₖ η.hom) (prodAssoc a✝).2)) s✝
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 ∥ₖ η.hom) (prodAssoc a✝).2)) s✝

Tactic:
Kernel.parallelComp_apply

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✝
⊢ (((κ₁.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✝
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:
Kernel.parallelComp_apply

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✝
⊢ (((κ₁.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✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
a✝¹ : X.carrier × Y.carrier
s✝ : Set PUnit.{u + 1}
a✝ : MeasurableSet s✝
⊢ ((Kernel.discard (X.carrier × Y.carrier)) a✝¹) s✝ =
    (Measure.map Prod.snd ((Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) a✝¹)) s✝

Tactic:
Kernel.parallelComp_apply

Goal state after:
X Y : SFinKer
a✝¹ : X.carrier × Y.carrier
s✝ : Set PUnit.{u + 1}
a✝ : MeasurableSet s✝
⊢ ((Kernel.discard (X.carrier × Y.carrier)) a✝¹) s✝ =
    (Measure.map Prod.snd (((Kernel.discard X.carrier) a✝¹.1).prod ((Kernel.discard Y.carrier) a✝¹.2))) s✝
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case neg.refine_1
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
ξ : ↑I
hξ : f a ξ ≤ x
hx : ¬x = 1
g : ↑I → ℝ := fun y ↦ (κ a).real (Icc 0 y)
nebot : (𝓝[>] x).NeBot := nhdsGT_neBot_of_exists_gt (Exists.intro 1 (lt_of_le_of_ne x.property.right hx))
⊢ Tendsto g (𝓝[>] x) (𝓝 ((κ a).real (Icc 0 x)))

Tactic:
let h := cdf ((κ a).map Subtype.val)
      have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
      simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]
      exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy)

Goal state after:
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:
by simpa

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

Goal state before:
pp: case right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
by_cases hp : p = 0
    · simp [hp]
    rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),
      ENNReal.coe_toReal]
    have hf := (hi (p * t)).lintegral_lt_top
    convert! hf using 3 with ω
    rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
      ← exp_mul, mul_comm, ← mul_assoc]
    positivity

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α), f a ∂p.toMeasure = ∫ (a : α) in p.support, f a ∂p.toMeasure

Tactic:
by rw [restrict_toMeasure_support p]

Goal state after:
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
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable fun ω ↦ (X s ω, X t ω)

Tactic:
suffices Measurable (fun ω ↦ (X s ω, X t ω)) by
      rwa [Prod.borelSpace.measurable_eq] at this

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
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable fun ω ↦ (X s ω, X t ω)
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:
by simpa

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:
by
  apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable
  exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

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

Goal state before:

Tactic:
(κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg)

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

Goal state before:
pp: case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
have h2 := h.mgf_le

Goal state after:
case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂⇑κ ∘ₘ ν, ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
rw [intervalIntegral.integral_add]

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

case hg
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ IntervalIntegrable (fun x ↦ 1) ρ 0 ↑N
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 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (Y j ^ 2) a = ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ

Tactic:
simp_rw [Y2]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ↑(rid k (linearize k G X)) =
    ((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp (lTensor (linearize k G X) (ε k G))

Tactic:
ext x; simp [types_tensorObj_def, types_tensorUnit_def, Action.tensorObj_V, linearizeMap,
    Action.rightUnitor_hom_hom]

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
⊢ ((↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))).comp (rTensor (linearize k G Z) (δ X Y))).comp
      (δ (X ⊗ Y) Z) =
    ((lTensor (linearize k G X) (δ Y Z)).comp (δ X (Y ⊗ Z))).comp (linearizeMap (α_ X Y Z).hom)

Tactic:
ext
  -- TODO : try not to `simp` with `δ` and `linearizeMap` directly here
  simp [linearizeMap, δ, MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
⊢ ↑(lid k (linearize k G X)).symm =
    ((rTensor (linearize k G X) (η k G)).comp (δ (𝟙_ (Action (Type u) G)) X)).comp (linearizeMap (λ_ X).inv)

Tactic:
ext
  -- TODO : try not to `simp` with `δ` and `linearizeMap` directly here
  simp [linearizeMap, δ, MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝³ : Monoid G
V : Type v'
inst✝² : AddCommMonoid V
k : Type u
inst✝¹ : CommSemiring k
inst✝ : Module k V
σ : Representation k G V
α : Type w'
i : α
g : G
r : k
f : α → V
⊢ (σ.freeLift f) (single i (MonoidAlgebra.single g r)) = r • (σ g) (f i)

Tactic:
simp [freeLift]

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:
by 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:
by 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:
by simpa

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

Goal state before:
pp: case e'_7
Ω : 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 μ
hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m) (⇑(Kernel.const Unit (μ.trim hm)) ∘ₘ Measure.dirac ())
e_3✝ : m.prod mΩ = Prod.instMeasurableSpace
a✝ : Unit
⊢ (Kernel.const Unit (Measure.map Function.diag μ)) a✝ =
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m)) a✝

Tactic:
rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
U : Type u_5
inst✝¹⁵ : CommSemiring A
inst✝¹⁴ : Monoid G✝
inst✝¹³ : AddCommMonoid V✝
inst✝¹² : AddCommMonoid W✝
inst✝¹¹ : AddCommMonoid U
inst✝¹⁰ : Module A V✝
inst✝⁹ : Module A W✝
inst✝⁸ : Module A U
ρ✝ : Representation A G✝ V✝
σ✝ : Representation A G✝ W✝
τ : Representation A G✝ U
f : V✝ →ₗ[A] W✝
G : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : FiniteDimensional k V
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ ↑(dualTensorHomEquiv k V W) ∘ₗ (ρ.dual.tprod σ) g = (ρ.linHom σ) g ∘ₗ ↑(dualTensorHomEquiv k V W)

Tactic:
by
    ext v' w v; simp [Module.Dual.transpose_apply]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω - ↑⌊c ^ x⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ x⌋₊)⁻¹

Tactic:
(ext1 n; field [(H n).ne'])

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_8
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun _x ↦ 1) = fun x ↦ ↑⌊c ^ x⌋₊ * (↑⌊c ^ x⌋₊)⁻¹

Tactic:
(ext1 n; field [(H n).ne'])

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Group G
inst✝⁸ : Field k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : FiniteDimensional k V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ x, ρ.character x⁻¹ * σ.character x = ↑(finrank k (ρ.IntertwiningMap σ))

Tactic:
← char_linHom,

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Group G
inst✝⁸ : Field k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : FiniteDimensional k V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ x, (ρ.linHom σ).character x = ↑(finrank k (ρ.IntertwiningMap σ))
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * Finset.univ.sum (of (linHom V.ρ W.ρ)).character = ↑(finrank k (V ⟶ W))

Tactic:
rw [FDRep.average_char_eq_finrank_invariants, ← LinearEquiv.finrank_eq
    (Representation.linHom.invariantsEquivFDRepHom V W), of_ρ']

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

Goal state before:
pp: case succ
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) (i + 1) = 𝟙 (X.resolutionX (i + 1))

Tactic:
rw [resolutionMap_succ, ih]
    ext F x
    rfl

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

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ (d k G n) (r • MonoidAlgebra.single c 1) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r • 1 * (-1) ^ ↑p)

Tactic:
map_smul,

Goal state after:
k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ r • (d k G n) (MonoidAlgebra.single c 1) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r • 1 * (-1) ^ ↑p)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)

Tactic:
map_smul,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ r • (A.ρ g) x - r • x = r • ((A.ρ g) x - x)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) (r • x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)

Tactic:
map_smul,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

Tactic:
rw [Set.mem_preimage, SetLike.mem_coe, ← C_mul_leadingCoeff_monomial_degree]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1 ∈
    span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : Prime z
⊢ (∀ b ∈ {z}, Prime b) ∧ Associated {z}.prod z

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
simp only [add_le_add_iff_right]
    refine le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_
    rw [FG.generators_ncard hfg]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: case mul
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z₁ z₂ : R
hz₁ : z₁ ∈ closure {r | IsUnit r ∨ Prime r}
hz₂ : z₂ ∈ closure {r | IsUnit r ∨ Prime r}
h₁ : ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z₁
h₂ : ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod z₂
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod (z₁ * z₂)

Tactic:
obtain ⟨S₁, hS₁pri, hS₁⟩ := h₁
      obtain ⟨S₂, hS₂pri, hS₂⟩ := h₂
      refine ⟨S₁ + S₂, by grind, ?_⟩
      rw [Multiset.prod_add]
      exact hS₁.mul_mul hS₂

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
u : ℕ → R
hu : CauchySeq u
N : ℕ → ℕ
hN : ∀ (i m : ℕ), N i ≤ m → ∀ (n : ℕ), N i ≤ n → u n - u m ∈ I ^ i
m✝ n✝ : ℕ
x✝ : m✝ ≤ n✝
⊢ m✝ ∈ Finset.Iic n✝

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
p q : MvPowerSeries (Option σ) R
k : ℕ
x : σ →₀ ℕ
m n : ℕ
u v : σ →₀ ℕ
h : ⟨(m, n), (u, v)⟩ ∈ (antidiagonal k).sigma fun a ↦ antidiagonal x
this : ∃ a b, (a none = m ∧ b none = n) ∧ a.some = u ∧ a + b = optionElim k x ∧ b.some = v
⊢ ∃ a, ∃ (_ : a ∈ antidiagonal (optionElim k x)), ⟨(a.1 none, a.2 none), (a.1.some, a.2.some)⟩ = ⟨(m, n), (u, v)⟩

Tactic:
by simpa

Goal state after: