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

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ᵐ (a : 𝓧) ∂⇑κ ∘ₘ μ, ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i a = (∂κ i/∂⇑κ ∘ₘ μ) a
x : 𝓧
hx : (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
⊢ (∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i x = (∂κ i/∂⇑κ ∘ₘ μ) x) →
    (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x

Tactic:
hx_all

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ᵐ (a : 𝓧) ∂⇑κ ∘ₘ μ, ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i a = (∂κ i/∂⇑κ ∘ₘ μ) a
x : 𝓧
hx : (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
hx_all : ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i x = (∂κ i/∂⇑κ ∘ₘ μ) x
⊢ (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ᵐ (a : 𝓧) ∂⇑κ ∘ₘ μ, ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i a = (∂κ i/∂⇑κ ∘ₘ μ) a
x : 𝓧
hx : (κ†μ) x = μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
hx_all : ∀ (i : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) i x = (∂κ i/∂⇑κ ∘ₘ μ) x
⊢ (μ.withDensity fun ω ↦ κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x) = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x

Tactic:
hx_all

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ avgRisk ℓ P hf.kernel π ≤ bayesRisk ℓ P π

Tactic:
hf.avgRisk_eq_lintegral_iInf hl

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤ bayesRisk ℓ P π
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
f : 𝓧 → 𝓨
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hf : IsArgminEstimator ℓ P π f
hl : Measurable (Function.uncurry ℓ)
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π ≤ bayesRisk ℓ P π

Tactic:
exact lintegral_iInf_posterior_le_bayesRisk hl _ _

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
zero_add

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
E : Type u_1
inst✝² : NormedAddCommGroup E
f : ℕ → E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hp : p ≠ 0
hf : Integrable f (geometricMeasure p)
⊢ HasSum (fun n ↦ ((1 - ↑p) ^ n * ↑p) • f n) (∫ (n : ℕ), f n ∂geometricMeasure p)

Tactic:
have : (fun n ↦ ((1 - p : ℝ) ^ n * p) • f n) =
      fun n ↦ (ENNReal.ofReal ((1 - p) ^ n * p)).toReal • f n := by
    ext n; rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]
  rw [this, geometricMeasure_eq hp]
  apply hasSum_integral_sum_dirac (by simp)
  convert! (integrable_geometricMeasure_iff hp).1 hf with n
  rw [ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (b : β), if b ∈ s then ∑' (a : α), p a * (f a) b else 0

Tactic:
simp [toOuterMeasure_apply, Set.indicator_apply]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω ↦ (((condExpKernel μ m) ω) s).toReal) =ᵐ[μ.trim hm] μ[s.indicator fun ω ↦ 1 | m]

Tactic:
rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm
    stronglyMeasurable_condExp]

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun x ↦ (((condExpKernel μ m) x) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m]
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
by
  specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
    (measurableSet_generateFrom (Set.mem_singleton t))
  filter_upwards [h_indep] with a ha
  by_cases h0 : κ a t = 0
  · exact Or.inl h0
  by_cases h_top : κ a t = ∞
  · exact Or.inr (Or.inr h_top)
  rw [← one_mul (κ a (t ∩ t)), Set.inter_self, ENNReal.mul_left_inj h0 h_top] at ha
  exact Or.inr (Or.inl ha.symm)

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

Goal state before:
pp: X✝ Y✝ : Stoch
κ✝ : X✝ ⟶ Y✝
X Y : Stoch
κ : Kernel X.obj.carrier Y.obj.carrier
inst✝¹ : IsDeterministic κ
inst✝ : IsMarkovKernel κ
⊢ { hom := { hom := κ, property := ⋯ }, property := ⋯ } ≫ Δ =
    Δ ≫ ({ hom := { hom := κ, property := ⋯ }, property := ⋯ } ⊗ₘ { hom := { hom := κ, property := ⋯ }, property := ⋯ })

Tactic:
ext : 1; dsimp
    exact Deterministic.copy_natural _

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
⊢ (∀ ⦃A : Set X⦄,
      MeasurableSet A →
        ∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A) ↔
    ∀ ⦃A : Set X⦄,
      MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
congr! 5 with A hA B hB x

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            ((condExpKernel μ m') a) (t1 ∩ t2) = ((condExpKernel μ m') a) t1 * ((condExpKernel μ m') a) t2) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩ <;> specialize h s t hs ht

Goal state after:
case refine_1
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

case refine_2
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
⊢ ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
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}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ e ∈ {x | a < f x.1 x.2} ↔ e ∈ ⋃ q, ⋃ (hqI : ↑q ∈ I), ⋃ (_ : ↑a < ↑q), {e | (κ e.1).real (Icc 0 ⟨↑q, hqI⟩) < ↑e.2}

Tactic:
simp_all only [lt_sSup_iff, mem_ofPred_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]

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}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ a_1, ∃ (h : 0 ≤ a_1 ∧ a_1 ≤ 1), (κ e.1).real (Icc 0 ⟨a_1, ⋯⟩) < ↑e.2 ∧ a < ⟨a_1, ⋯⟩) ↔
    ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
⊢ f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

Tactic:
rw [Set.indicator_apply]
    split_ifs <;> simp_all

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
ω : Ω
⊢ f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω

Tactic:
rw [Set.indicator_apply]
    split_ifs <;> simp_all

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
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∫ (a : α), f a ∂p.toMeasure = ∑ a, (p a).toReal • f a

Tactic:
by
  rw [integral_fintype .of_finite]
  congr with x
  rw [measureReal_def]
  congr 2
  exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

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 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) + ↑cY * (t * ↑q) ^ 2 / 2 * (1 / ↑q)) =
    rexp ((↑(NNReal.sqrt cX) + ↑(NNReal.sqrt cY)) ^ 2 * t ^ 2 / 2)

Tactic:
simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]

Goal state after:
Ω : 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 : ℝ
⊢ ↑cX * (t * ((√↑cX + √↑cY) / √↑cX)) ^ 2 / 2 * (√↑cX / (√↑cX + √↑cY)) +
      ↑cY * (t * ((√↑cX + √↑cY) / √↑cY)) ^ 2 / 2 * (√↑cY / (√↑cX + √↑cY)) =
    (√↑cX + √↑cY) ^ 2 * t ^ 2 / 2
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
⊢ ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm ∘ₗ (trivial k G k) g =
    (linearize k G (𝟙_ (Action (Type w) G))) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm

Tactic:
by ext1; simp [linearize_single _]

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
⊢ Module.finrank k V = 1

Tactic:
obtain hU | hU := eq_bot_or_eq_top U

Goal state after:
case inl
A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
hU : U = ⊥
⊢ Module.finrank k V = 1

case inr
A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
U : Submodule A V :=
  let __src := k ∙ v;
  { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := ⋯ }
hU : U = ⊤
⊢ Module.finrank k V = 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet X μ)

Tactic:
simp [integrableExpSet_eq_univ hX]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
⊢ 0 ∈ interior (integrableExpSet X μ)

Tactic:
simp [integrableExpSet_eq_univ hX]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case zero
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
f : ρ.IntertwiningMap σ
v : ρ.asModule
⊢ f.toLinearMap (0 • v) = (RingHom.id A[G]) 0 • f.toLinearMap v

Tactic:
simp [f.toLinearMap.map_zero]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) ((‖b - a‖₊ / 2) ^ 2) μ

Tactic:
← sub_sub_sub_cancel_right b a μ[X]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) ((‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) ^ 2) μ
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁴ : Monoid G
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρ : Representation k G V
⊢ ρ.character 1 = ↑(finrank k V)

Tactic:
simp only [character, map_one, trace_one]

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✝⁷ : Monoid 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
⊢ (ρ.tprod σ).character = ρ.character * σ.character

Tactic:
ext g; convert! trace_tensorProduct' (ρ g) (σ g)

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)
⊢ ↑(finrank k ↥(ρ.linHom σ).invariants) = ↑(finrank k (ρ.IntertwiningMap σ))

Tactic:
(invariantsEquivIntertwiningMap ρ σ).finrank_eq

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V : FDRep k G
⊢ V.character 1 = ↑(finrank k ↑V.V)

Tactic:
simp only [character, map_one, trace_one]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
have : IsProbabilityMeasure μ := MemLp.isProbabilityMeasure_of_indepFun
    (X 0) (X 1) (zero_lt_one.trans_le hp).ne' hp' hℒp h (hindep zero_ne_one)

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
r : k
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom ((r • f) ≫ g) = Hom.hom (r • f ≫ g)

Tactic:
simp [smul_hom, Representation.IntertwiningMap.comp_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case hx
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
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) ⊆
    MulAction.orbit (↥S) g

Tactic:
intro x hx
    contrapose hx
    simpa using indToCoindAux_of_not_rel g x a hx

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ ((resIndAdjunction k S).homEquiv B A) f = (resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f ≫ A.indCoindIso.inv

Tactic:
rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_apply]
  simp [resCoindHomEquiv]

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 : ℕ
⊢ (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫
        (𝟙 (((barComplex k G).linearYonedaObj k A).X (n + 1)) ≫
            ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)) ≫
          (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0

Tactic:
slice_lhs 2 4 => rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      0 ≫ (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0