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

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (a : Ω), μ[X ^ 2 | m] a ∂μ - ∫ (a : Ω), (μ[X | m] ^ 2) a ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ

Tactic:
integral_condExp hm,

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (a : Ω), (μ[X | m] ^ 2) a ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (μ[X | m] ^ 2) μ
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : ¬Measurable (Function.uncurry f)
⊢ κ.withDensity f = 0

Tactic:
exact dif_neg hf

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
⊢ ∃ f, ∃ (hf : Measurable f), κ = deterministic f hf

Tactic:
refine ⟨f, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
⊢ Measurable f

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝² : StandardBorelSpace β
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
inst✝ : IsDeterministic κ
f : α → β
hf : ∀ (a : α), κ a = Measure.dirac (f a)
⊢ κ = deterministic f ?refine_1
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
⊢ μ ⊗ₘ κ ≪ μ.prod (⇑κ ∘ₘ μ)

Tactic:
by
    rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
    exact this.map measurable_swap

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
h𝓨 : Nonempty 𝓨
P : Kernel Θ 𝓧
π : Measure Θ
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
⊢ bayesRisk ℓ P π ≤ ↑C * P.bound * π Set.univ

Tactic:
refine (bayesRisk_le_avgRisk ℓ P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π).trans ?_
  refine (avgRisk_le_mul' P (Kernel.const 𝓧 (Measure.dirac h𝓨.some)) π hℓC).trans ?_
  rcases isEmpty_or_nonempty 𝓧 <;> simp

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
⊢ bayesRisk ℓ P π = ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

Tactic:
rcases isEmpty_or_nonempty 𝓧 with hX | hX

Goal state after:
case inl
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : IsEmpty 𝓧
⊢ bayesRisk ℓ P π = ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π

case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Subsingleton 𝓧
inst✝ : Nonempty 𝓨
hX : Nonempty 𝓧
⊢ bayesRisk ℓ P π = ⨅ μ, ⨅ (_ : IsProbabilityMeasure μ), avgRisk ℓ P (Kernel.const 𝓧 μ) π
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f x y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f (frestrictLe b x) x ∂(traj κ a) x₀

Tactic:
have hf' := hf

Goal state after:
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf hf' : Integrable (uncurry f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
⊢ ∫ (x : (i : ↥(Iic b)) → X ↑i), ∫ (y : (n : ℕ) → X n), f x y ∂(traj κ b) x ∂(partialTraj κ a b) x₀ =
    ∫ (x : (n : ℕ) → X n), f (frestrictLe b x) x ∂(traj κ a) x₀
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ Bin(R, n, p).real {↑k} = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)

Tactic:
rw [map_measureReal_apply (by fun_prop) (by measurability)]

Goal state after:
R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
inst✝¹ : MeasurableSingletonClass R
inst✝ : CharZero R
n k : ℕ
p : ↑I
⊢ Bin(n, p).real (Nat.cast ⁻¹' {↑k}) = ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r x : ℝ
⊢ ENNReal.ofReal (gammaPDFReal 1 r x) = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)

Tactic:
gammaPDFReal

Goal state after:
r x : ℝ
⊢ ENNReal.ofReal (if 0 ≤ x then r ^ 1 / Gamma 1 * x ^ (1 - 1) * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case hfm
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ AEStronglyMeasurable (fun x ↦ r * t ^ r * x ^ (-(r + 1))) (volume.restrict (Ici t))

Tactic:
· apply (measurable_paretoPDFReal t r).aestronglyMeasurable.congr
    refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_
    simp_rw [paretoPDFReal, eq_true_intro hx, ite_true]

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

Goal state before:
pp: case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᵐ[volume.restrict (Iic x)] paretoPDFReal t r

Tactic:
exact ae_of_all _ fun _ ↦ by simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Po(R, r₁) ∗ Po(R, r₂) = Po(R, r₁ + r₂)

Tactic:
rw [← Nat.coe_castAddMonoidHom, ← Measure.map_conv_addMonoidHom _ (by fun_prop),
    poissonMeasure_conv_poissonMeasure]

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

Goal state before:
pp: case neg.refine_1
Ω : 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
⊢ ∀ (s_1 : Set Ω),
    MeasurableSet s_1 → (μ.restrict s) s_1 < ∞ → IntegrableOn (fun x ↦ ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)

Tactic:
rintro t - -
      rw [integrableOn_const_iff]
      exact Or.inr <| measure_lt_top (μ.restrict s) t

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ μ[|s].real t

Tactic:
← integral_indicator_one ht

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : p = 0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)

Tactic:
· simpa [hp] using hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _)

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)
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 κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp (↑p * t * X x)) ∂κ ω' < ∞
ω : Ω
⊢ ‖rexp (t * X ω)‖ₑ ^ ↑p = ENNReal.ofReal (rexp (↑p * t * X ω))

Tactic:
rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
      ← exp_mul, mul_comm, ← mul_assoc]

Goal state after:
Ω : 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 : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp (↑p * t * X x)) ∂κ ω' < ∞
ω : Ω
⊢ 0 ≤ ↑p
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n

Tactic:
rw [add_tsub_cancel_of_le (mod_cast h), one_pow]

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * Y ω)) (⇑κ ∘ₘ ν)

Tactic:
refine (integrable_congr ?_).mpr (h.integrable_exp_mul t)
    filter_upwards [h'] with ω hω using by rw [hω]

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 κ ν
r : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (fun ω ↦ r * X ω) (κ ω') t ≤ rexp (↑(NNReal.mk (r ^ 2) ⋯ * c) * t ^ 2 / 2)

Tactic:
by
    filter_upwards [h.mgf_le] with ω hω t
    rw [mgf_const_mul, mul_comm]
    refine (hω (t * r)).trans_eq ?_
    congr 1
    simp only [NNReal.coe_mul, NNReal.coe_mk]
    ring

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
hY : HasSubgaussianMGF Y cY κ ν
hX0✝ : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
ω : Ω
hX0 : X ω = 0 ω
⊢ Y ω = X ω + Y ω

Tactic:
simp [hX0]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂Measure.map f μ

Tactic:
by
  simpa using moment_truncation_eq_intervalIntegral_of_nonneg hf one_ne_zero h'f

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✝⁷ : 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
τ : Representation A G U
f : V →ₗ[A] W
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ ↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv) ∘ₗ ρ g = τ g ∘ₗ ↑(φ.toLinearEquiv ≪≫ₗ ψ.toLinearEquiv)

Tactic:
LinearEquiv.coe_trans,

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
τ : Representation A G U
f : V →ₗ[A] W
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ (↑ψ.toLinearEquiv ∘ₗ ↑φ.toLinearEquiv) ∘ₗ ρ g = τ g ∘ₗ ↑ψ.toLinearEquiv ∘ₗ ↑φ.toLinearEquiv
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ x ∈ range N, ((↑(u x))⁻¹ * ε⁻¹) ^ 2 * Var[S (u x); ℙ] ≤ ε⁻¹ ^ 2 * C

Tactic:
mul_comm _ (ε⁻¹),

Goal state after:
Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ x ∈ range N, (ε⁻¹ * (↑(u x))⁻¹) ^ 2 * Var[S (u x); ℙ] ≤ ε⁻¹ ^ 2 * C
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        v i * ↑⌊c ^ n⌋₊
ε : ℝ
εpos : 0 < ε
i : ℕ
hi : v i < ε
n : ℕ
hn :
  |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
    v i * ↑⌊c ^ n⌋₊
⊢ |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| ≤
    ε * ↑⌊c ^ n⌋₊

Tactic:
exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ average k G * single g 1 = average k G

Tactic:
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]
  set f : G → k[G] := fun x => .single x 1
  change ⅟(Fintype.card G : k) • ∑ x : G, f (x * g) = ⅟(Fintype.card G : k) • ∑ x : G, f x
  rw [Function.Bijective.sum_comp (Group.mulRight_bijective g) _]

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
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : 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 0 (0 + 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_1_comp_cochainsIso₁ (MonoidHom.id G) X.f⟩).w) x)) g

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : Fin 0 → G
a : ↑A
y : G
⊢ (A.ρ y) (Pi.single x a default) - Pi.single x a default =
    (A.ρ y) (Pi.single x a fun i ↦ y) - Pi.single x a (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) (uniqueElim y))

Tactic:
← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y),

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : Fin 0 → G
a : ↑A
y : G
⊢ (A.ρ y) (Pi.single x a default) - Pi.single x a default =
    (A.ρ y) (Pi.single x a default) - Pi.single x a (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) (uniqueElim y))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 1).leftHomologyIso.hom

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
h :
  (shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousChains A) 1).leftHomologyIso.hom
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
let z : G × G →₀ A := lmapDomain _ k (Prod.map s s) y

Goal state after:
case h
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
fg : I.FG
x : AdicCompletion I R
⊢ x ∈ (eval I R 1).ker ↔ x ∈ Ideal.map (algebraMap R (AdicCompletion I R)) I

Tactic:
· simp [← pow_smul_top_eq_ker_eval fg]

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

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : ↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S)))
hy : (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) ((A.toCoinvariants S).resOfQuotientIso S).inv)) y = x
Y : G →₀ ↑A
hY : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Y = ↑y
h' :
  (ConcreteCategory.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₂ ≫ (shortComplexH1 (A.toCoinvariants S)).g))
      Y =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₃)) Y
⊢ (ConcreteCategory.hom (d₁₀ A)) Y ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)

Tactic:
simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ ⊤ ≤ p.contentIdeal

Tactic:
calc
  ⊤ = (p * q).contentIdeal := h.symm
  _ ≤ p.contentIdeal * q.contentIdeal := contentIdeal_mul_le_mul_contentIdeal p q
  _ ≤ p.contentIdeal := mul_le_left

Goal state after:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N

Tactic:
convert! map_mono ∘ (isSMulRegular_on_quot_iff_lsmul_comap_le N r).mp using 2
  exact Eq.trans (congrArg (· ⊓ N) (map_top _)) (map_comap_eq _ _).symm

Goal state after: