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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ ∫ (y : (i : ι) → X i), f (s.restrict y) ∂infinitePi μ = ∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

Tactic:
rw [← integral_map, infinitePi_map_restrict]
  · fun_prop
  · rwa [infinitePi_map_restrict]

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

Goal state before:
pp: α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

Tactic:
exact mul_pos (mul_pos (one_div_pos.2 (beta_pos hα hβ)) (Real.rpow_pos_of_pos hx1 (α - 1)))
    (Real.rpow_pos_of_pos (by linarith) (β - 1))

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) =
    ((traj κ b) x) ((fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' (fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

Tactic:
congr 1 with y

Goal state after:
case e_f.e_6
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
y : (i : ℕ) → X i
⊢ y ∈ (fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s ↔
    y ∈ (fun x_1 ↦ updateFinset x_1 (Iic b) x) ⁻¹' (fun x ↦ (frestrictLe b x, x)) ⁻¹' s
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ cauchyPDFReal x₀ γ x = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

Tactic:
cauchyPDFReal_def

Goal state after:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
x : ℝ
⊢ 0 < cauchyPDFReal x₀ γ x

Tactic:
cauchyPDFReal_def

Goal state after:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
x : ℝ
⊢ 0 < π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝⁵ : MeasurableSpace R
inst✝⁴ : AddMonoidWithOne R
n : ℕ
p : ↑I
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∫ (x : ℕ), f ↑x ∂Bin(n, p) = ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f ↑k

Tactic:
integral_binomial

Goal state after:
R : Type u_1
inst✝⁵ : MeasurableSpace R
inst✝⁴ : AddMonoidWithOne R
n : ℕ
p : ↑I
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f ↑k =
    ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f ↑k
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ∞
a : α
⊢ a ∈ (normalize f hf0 hf).support ↔ a ∈ Function.support f

Tactic:
simp [hf, mem_support_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
⊢ (p.bindOnSupport fun a ha ↦ q.bindOnSupport (f a ha)) =
    q.bindOnSupport fun b hb ↦ p.bindOnSupport fun a ha ↦ f a ha b hb

Tactic:
apply PMF.ext; rintro c
  simp only [bindOnSupport_apply, ← tsum_dite_right,
    ENNReal.tsum_mul_left.symm]
  refine _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => ?_)
  split_ifs with h1 h2 h2 <;> ring

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

Goal state before:
pp: case inr.hm.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 ↦ x1 ⊆ x2) (ns a) (ns c) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c

Tactic:
· exact hc.2 hn

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst✝ : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ (⇑κ ∘ₘ π) s = ∫⁻ (x : α), (κ x) s ∂π

Tactic:
by rw [Measure.bind_apply hs (Kernel.aemeasurable _)]

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Ω
m : ι → MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔ iCondIndepSets m' hm' (fun x ↦ {s | MeasurableSet s}) μ

Tactic:
simp only [iCondIndep, iCondIndepSets, Kernel.iIndep]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
haX : ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t
haT : ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u
⊢ s.indicator 1 (k a) * (((condDistrib f k μ) (k a)) t * ((condDistrib g k μ) (k a)) u) =
    (Measure.dirac a) (k ⁻¹' s) *
      ((((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t *
        (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u)

Tactic:
rw [@Measure.dirac_apply' _ (mγ.comap k) _ _ (hk_meas hs)]

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
haX : ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t
haT : ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u
⊢ s.indicator 1 (k a) * (((condDistrib f k μ) (k a)) t * ((condDistrib g k μ) (k a)) u) =
    (k ⁻¹' s).indicator 1 a *
      ((((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t *
        (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u)
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_3
Ω : 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ ∀ x ∉ {ω | τ ω ≤ σ ω}, {ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ) x = 0

Tactic:
· intro x hx
      simp only [hx, Set.indicator_of_notMem, not_false_iff]

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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ μ[{ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ) | hσ.measurableSpace] =ᵐ[μ]
    {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)

Tactic:
have h_meas : AEStronglyMeasurable[hσ.measurableSpace]
      ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ := by
    refine StronglyMeasurable.aestronglyMeasurable ?_
    refine StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
      (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
    · intro t ht
      rw [Set.inter_comm _ t] at ht ⊢
      rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
      exact ht.2
    · refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
      refine Measurable.stronglyMeasurable ?_
      exact measurable_stoppedValue h.stronglyAdapted.isStronglyProgressive_of_discrete hτ
    · intro x hx
      simp only [hx, Set.indicator_of_notMem, not_false_iff]

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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
h_meas : AEStronglyMeasurable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ μ[{ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ) | hσ.measurableSpace] =ᵐ[μ]
    {ω | τ ω ≤ σ ω}.indicator (stoppedValue f τ)
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case «0»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [binomial_apply, bernoulli_apply]

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

Goal state before:
pp: case «1»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [binomial_apply, bernoulli_apply]

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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), cgf X (κ ω') t ≤ ↑c * t ^ 2 / 2

Tactic:
by
  filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul] with ω' h h_int t
  calc cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]

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 : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a = ∑' (a : ↑p.support), (p ↑a).toReal • f ↑a

Tactic:
congr with x; congr 2
    apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Tactic:
have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ rexp (↑cX * (t * ↑p) ^ 2 / 2) ^ (1 / ↑p) * rexp (↑cY * (t * ↑q) ^ 2 / 2) ^ (1 / ↑q) =
    rexp ((↑(NNReal.sqrt cX) + ↑(NNReal.sqrt cY)) ^ 2 * t ^ 2 / 2)

Tactic:
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.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
z : A[G]
hz : z ∈ Submonoid.center A[G]
x✝ : G
⊢ ρ.asAlgebraHom z ∘ₗ ρ x✝ = ρ x✝ ∘ₗ ρ.asAlgebraHom z

Tactic:
by simp_rw [← ρ.asAlgebraHom_of, ← Module.End.mul_eq_comp,
    ← map_mul, Submonoid.mem_center_iff.1 hz]

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

Goal state before:
pp: case succ.succ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
a✝ :
  ((∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ) →
    (∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
hn : HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ Measurable fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω

Tactic:
refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable

Goal state after:
case succ.succ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
a✝ :
  ((∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ) →
    (∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
hn : HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
m : ℕ
hm : m ∈ Finset.range (n + 1)
⊢ m ≤ n
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inl
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)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : IsEmpty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

pp: case inr
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)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
· rw [card_inv_mul_sum_char_mul_char_eq_finrank]
    simpa [finrank_eq_zero_of_subsingleton]

Goal state after:
case inr
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)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ ↑(of ρ) = X

Tactic:
with_reducible rfl

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

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ (of ρ).ρ = ρ

Tactic:
with_reducible rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B : TopRep k G
f : A ⟶ B
g : G
a : ↑A
⊢ (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

Tactic:
simpa using! congr($(f.hom.2 g) a)

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ ↑(of ρ) = X

Tactic:
with_reducible rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : Semiring k
inst✝² : Monoid G
X : Type w
inst✝¹ : AddCommGroup X
inst✝ : Module k X
ρ : Representation k G X
⊢ (of ρ).ρ = ρ

Tactic:
with_reducible rfl

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

Goal state before:
pp: case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - X.d (n + 1) ≫ (coind₁Functor k G).map (X.d (n + 1)) = 0

Tactic:
nth_rw 2 [d_succ]

Goal state after:
case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)) ≫
        (coind₁Functor k G).map (X.d (n + 1)) =
    0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

Tactic:
rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]
    exact mt (fun ⟨s₁, hs₁⟩ => ⟨s⁻¹ * s₁, by simp_all [S.1.smul_def, mul_assoc]⟩) h

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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
⊢ cochainsMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) = cochainsMap φ f ≫ cochainsMap ψ g

Tactic:
by
  ext i v x
  exact congr($(resolutionMap_comp φ ψ f g (i + 1)).hom v.1 x)

Goal state after:
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
y : G → ↑X.X₂
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ x ∈ cocycles₂ X.X₁

Tactic:
by
  apply Function.Injective.comp_left ((Rep.mono_iff_injective X.f).1 hX.2)
  have := congr($((mapShortComplexH2 (MonoidHom.id G) X.f).comm₂₃.symm) x)
  simp_all [shortComplexH2, LinearMap.compLeft]

Goal state after: