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

Goal state before:

Tactic:
∑' a, (rexp (-r) * r ^ a / a ! : ℝ) * cexp ((a * t : ℝ) * I)
  _ = ∑' a, (rexp (-r)) * ((r * cexp (t * I)) ^ a / a !) := by
      congr with a
      push_cast
      rw [mul_pow, ← Complex.exp_nat_mul]
      ring_nf
  _ = (rexp (-r)) * ∑' a, ((r * cexp (t * I)) ^ a / a !) := tsum_mul_left
  _ = (rexp (-r)) * cexp (r * cexp (t * I)) := by
      rw [(NormedSpace.expSeries_div_hasSum_exp (r * cexp (t * I))).tsum_eq, exp_eq_exp_ℂ]
  _ = cexp (r * (cexp (t * I) - 1)) := by
      rw [ofReal_exp, ← Complex.exp_add]
      push_cast
      ring_nf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0
h : p ≤ 1
⊢ (∑ a, bif a then ↑p else 1 - ↑p) = 1

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < poissonPMFReal r n

Tactic:
by
  rw [poissonPMFReal]
  positivity

Goal state after:
Module: Mathlib.Probability.IdentDistribIndep

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst✝ : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
⊢ Measure.map (fun ω ↦ (X ω, Y ω)) μ = Measure.map (fun ω' ↦ (Z ω', W ω')) ν

Tactic:
have : IsFiniteMeasure ν := by
      have : IsFiniteMeasure (ν.map Z) := by rw [← hXZ.map_eq]; infer_instance
      exact Measure.isFiniteMeasure_of_map hXZ.aemeasurable_snd
    rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]

Goal state after:
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case neg.refine_2.inl
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = ∅
⊢ ∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s = ∫ (x : Ω) in t, f x ∂μ.restrict s

Tactic:
simp [h]

Goal state after:
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 ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']

pp: case hf
Ω : 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)
⊢ ∀ (i : ι), Measurable (f i)

Tactic:
swap

Goal state after:
case hf
Ω : 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)
⊢ ∀ (i : ι), Measurable (f i)

Ω : 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 ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ]
          ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

Tactic:
swap

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∑ a, ↑(p ^ ↑a * (1 - p) ^ (↑(Fin.last n) - ↑a) * ↑(n.choose ↑a)) = 1

Tactic:
by
    norm_cast
    convert! (add_pow p (1 - p) n).symm
    · rw [Finset.sum_fin_eq_sum_range]
      apply Finset.sum_congr rfl
      intro i hi
      rw [Finset.mem_range] at hi
      rw [dif_pos hi]
    · rw [add_tsub_cancel_of_le (mod_cast h), one_pow]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
⊢ truncation f A x = f x

Tactic:
by
  simp only [truncation, indicator, id, Function.comp_apply, ite_eq_left_iff]
  intro H
  apply H.elim
  simp [(abs_lt.1 h).1, (abs_lt.1 h).2.le]

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

Goal state before:
pp: case pos
Ω : 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 ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

pp: case neg
Ω : 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 ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
swap

Goal state after:
case neg
Ω : 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 ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

case pos
Ω : 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 ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : 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 κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

pp: case neg
Ω : 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 κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
swap

Goal state after:
case neg
Ω : 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 κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

case pos
Ω : 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 κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : 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))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

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:
swap

Goal state after:
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))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

case pos
Ω : 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))) (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : 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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

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 η (ν ⊗ₘ κ)
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
swap

Goal state after:
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 η (ν ⊗ₘ κ)
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

case pos
Ω : 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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
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 ∂ρ
⊢ ∫ (x : ℝ) in ↑0..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0..↑K, x ∂ρ

pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Tactic:
swap

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

Ω : 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 ∂ρ
⊢ ∫ (x : ℝ) in ↑0..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0..↑K, x ∂ρ
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✝⁷ : Semiring 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
f : ρ.IntertwiningMap σ
g : G
l : U →ₗ[A] V
⊢ (f.toLinearMap ∘ₗ ρ g) ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l

Tactic:
f.2,

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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
f : ρ.IntertwiningMap σ
g : G
l : U →ₗ[A] V
⊢ (σ g ∘ₗ f.toLinearMap) ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map (f.toLinearMap ∘ₗ ρ x) (g.toLinearMap ∘ₗ τ x) =
    (σ.tprod π) x ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
f.2,

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
⊢ TensorProduct.map (σ x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ τ x) =
    (σ.tprod π) x ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap
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) μ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
let s : Set E := Set.range (X 0) ∪ {0}

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}
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
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
π₂✝ : ContRepresentation R G W
π₃✝ : ContRepresentation R G U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ (f.toContinuousLinearMap ∘SL π₂ h) ∘SL g.toContinuousLinearMap =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

Tactic:
f.2,

Goal state after:
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
π₂✝ : ContRepresentation R G W
π₃✝ : ContRepresentation R G U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ (π₃ h ∘SL f.toContinuousLinearMap) ∘SL g.toContinuousLinearMap =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap
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
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
s : S
f : π₁ →ⁱL π₂
g : G
⊢ s • f.toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL (s • f.toContinuousLinearMap)

Tactic:
f.2,

Goal state after:
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
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
s : S
f : π₁ →ⁱL π₂
g : G
⊢ s • π₂ g ∘SL f.toContinuousLinearMap = π₂ g ∘SL (s • f.toContinuousLinearMap)
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f

Tactic:
by exact isIso_of_mono_of_epi f

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → ↑A
h : (ConcreteCategory.hom (d A n)) f = 0
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((inhomogeneousCochains A).d n (n + 1)))) f = 0

Tactic:
simp [h]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → ↑A
h : (ConcreteCategory.hom (d A n)) f = 0
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((inhomogeneousCochains A).d n (n + 1)))) f = 0

Tactic:
simp [h]

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupCohomologyπEven A g hg i hi)) x = 0 ↔ ↑x ∈ (Hom.hom A.norm).range

Tactic:
by
  simp [groupCohomologyπEven, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y / ↑y = x⁻¹
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
use y

Goal state after:
case h
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
H : ∀ (x : L), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
hxinv : (Algebra.norm K) x⁻¹ = 1
y : Lˣ
hy : g ↑y / ↑y = x⁻¹
⊢ ↑y / g ↑y = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ ⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1))) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)

Tactic:
ext g
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₂_comp_inv]
      simpa [← hx] using! congr_fun (congr($((CommSq.vert_inv
        ⟨cochainsMap_f_2_comp_cochainsIso₂ (MonoidHom.id G) X.f⟩).w) x)) g

Goal state after: