mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

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

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ (((κ.hom ∥ₖ Kernel.id).map Prod.fst) a✝) s✝ = ((κ.hom.comap Prod.fst ⋯) a✝) s✝

Tactic:
rw [Kernel.map_apply' _ (by fun_prop) _ hs, Kernel.comap_apply' _ (by fun_prop),
      Kernel.parallelComp_apply' <| measurable_fst hs]

Goal state after:
X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ ∫⁻ (b : Y✝.carrier), (Kernel.id a✝.2) (Prod.mk b ⁻¹' Prod.fst ⁻¹' s✝) ∂κ.hom a✝.1 = (κ.hom a✝.1) s✝
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

pp: case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
· exact hm₁

Goal state after:
case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap X.carrier Y.carrier)

Tactic:
Kernel.swap

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.swap Y.carrier X.carrier)

Tactic:
Kernel.swap

Goal state after:
X Y : SFinKer
⊢ IsSFiniteKernel (Kernel.deterministic Prod.swap ⋯)
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Goal state after:
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by
    filter_upwards [this] with ω hω
    simpa [hX.p_pos, not_lt_of_gt hX.p_pos] using hω

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
⊢ Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ σ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)

Tactic:
hτω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ Tendsto (fun x ↦ σ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
⊢ (Monotone fun x ↦ τ x ω) → (Monotone fun x ↦ σ x ω) → Monotone fun x ↦ (τ ⊓ σ) x ω

Tactic:
hτω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
ω : Ω
hτω : Monotone fun x ↦ τ x ω
⊢ (Monotone fun x ↦ σ x ω) → Monotone fun x ↦ (τ ⊓ σ) x ω
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
this : (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
ω : Ω
hTop : Tendsto (fun x ↦ σ n x ω) atTop (𝓝 ⊤)
⊢ ω ∉ ⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)}

Tactic:
hmem

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
this : (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
ω : Ω
hTop : Tendsto (fun x ↦ σ n x ω) atTop (𝓝 ⊤)
hmem : ω ∈ ⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)}
⊢ False
Module: Mathlib.Probability.StrongLaw

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

Tactic:
by
  apply integral_mono_of_nonneg
    (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)
  · exact truncation_nonneg _ (h'f x)
  · calc
      truncation f A x ≤ |truncation f A x| := le_abs_self _
      _ ≤ |f x| := abs_truncation_le_abs_self _ _ _
      _ = f x := abs_of_nonneg (h'f x)

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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ Integrable (fun y ↦ rexp (↑q * X y)) (κ ω') →
    (∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)) →
      Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
        mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)

Tactic:
hX_int

Goal state after:
Ω : 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 κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
⊢ (∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)) →
    Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω') →
      mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case insert.refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ X i ⟂ᵢ[μ] fun ω ↦ ∑ c ∈ s, X c ω

Tactic:
convert! h_indep'
      rw [Finset.sum_apply]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑n * ↑c))

Tactic:
have h := (sum_of_iIndepFun h_indep (c := fun _ ↦ c)
    (s := Finset.range n) (by simpa)).measure_ge_le hε
  simpa [← mul_assoc] using h

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
f : σ.IntertwiningMap τ
x✝¹ : A
x✝ : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝¹ • x✝).toLinearMap) ⋯ =
    (RingHom.id A) x✝¹ • LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝.toLinearMap) ⋯

Tactic:
ext; simp [toLinearMap_apply]

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
x✝¹ x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ + x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝¹.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp [toLinearMap_apply]

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
x✝¹ : A
x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ • x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ •
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp [toLinearMap_apply]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at hX ⊢

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ Kernel.HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Kernel.const Unit (Measure.map Function.diag μ))
    (Measure.dirac ())
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)

Tactic:
by
  rw [FDRep.isoToLinearEquiv, ← hom_hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj,
    Iso.conj_apply, ← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff]
  dsimp only [Action.forget_map, Functor.mapIso_hom]
  rw [i.hom.comm g]
  cat_disch

Goal state after:
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
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬↑(u n) * ε ≤ |(∑ i ∈ range (u n), Y i) ω - ∫ (a : Ω), (∑ i ∈ range (u n), Y i) a|
⊢ ∀ᶠ (n : ℕ) in atTop,
    |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊

Tactic:
not_le,

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
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, |(∑ i ∈ range (u n), Y i) ω - ∫ (a : Ω), (∑ i ∈ range (u n), Y i) a| < ↑(u n) * ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ ((↑(Nat.card G))⁻¹ʳ * ↑(Fintype.card G)) • v = v

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ ((↑(Nat.card G))⁻¹ʳ * ↑(Nat.card G)) • v = v
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mpr
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
⊢ Simple V

Tactic:
have eq := V.scalar_product_char_eq_finrank_equivariant V
    rw [h, inv_mul_cancel_of_invertible] at eq
    rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

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)
A : Rep.{w, u, v} k ↥S
g g₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
x✝ : (QuotientGroup.rightRel S) (↑s * g₁) g
s₁ : ↥S
hs₁ : (fun m ↦ m • g) s₁ = ↑s * g₁
⊢ (fun m ↦ m • g) (s⁻¹ * s₁) = g₁

Tactic:
simp_all [S.1.smul_def, mul_assoc]

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)
A : Rep.{w, u, v} k ↥S
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
x✝ : (QuotientGroup.rightRel S) g₂ (↑s * g₁)
s₁ : ↥S
hs₁ : (fun m ↦ m • (↑s * g₁)) s₁ = g₂
⊢ (fun m ↦ m • g₁) (s₁ * s) = g₂

Tactic:
simp_all [S.1.smul_def, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g : G
⊢ TensorProduct.lift
        (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g =
    TensorProduct.lift
      (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k))

Tactic:
ext h x
      simp only [LinearMap.coe_comp, Function.comp_apply, MonoidAlgebra.lsingle_apply]
      simp [ofMulAction_single, mul_inv_rev, hom_comm_apply f g]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 1 ≫
      ((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).d 1 0 =
    0

Tactic:
exact comp_zero

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 y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1)) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + (y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))) =
    (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1)) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))

Tactic:
add_sub_assoc

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1)) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + (y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))) =
    (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1)) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + (y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1)))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G × G → A
hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₂ f

Tactic:
by
  rcases hf with ⟨a, rfl⟩
  exact ⟨a, fun _ _ => rfl⟩

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₀ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 1 0)) ((ConcreteCategory.hom (chainsIso₁ X.X₂).inv) y)) x✝

Tactic:
conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
      simp [chainsIso₀, ← hx]

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

Goal state before:
pp: case h.refine_3.H.H
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
g h : G
⊢ ↑(Quotient.liftOn' (↑g * ↑h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) =
    ↑(((A.quotientToInvariants S).ρ ↑g) (Quotient.liftOn' (↑h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
        Quotient.liftOn' (↑g) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯)

Tactic:
simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

Tactic:
rw [Submodule.restrictScalars_pow hn]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯) ^ n =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ ∀ x ∈ I, C (constantCoeff x) ∈ I