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

Goal state before:
pp: case inr.h_le
α : 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 η μα
⊢ ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0

pp: case inr.h_le'
α : 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 η μα
⊢ limsup s f ≤ m0

pp: case inr.hm
α : 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 η μα
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ⨆ n ∈ ns i, s n

Tactic:
· exact fun a => iSup₂_le fun n _ => h_le n

Goal state after:
case inr.h_le'
α : 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 η μα
⊢ limsup s f ≤ m0

case inr.hm
α : 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 η μα
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ⨆ n ∈ ns i, s n
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
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

Tactic:
rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩

Goal state after:
case mp
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
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem : (κ e.1).real (Icc 0 ⟨y, ⋯⟩) < ↑e.2
hy : ↑a < y
⊢ ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ ε = (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ SFinKer)).hom

Tactic:
by
    ext : 1; dsimp
    simp only [Kernel.id_parallelComp_comp_parallelComp_id]
    rw [Kernel.id_map (by fun_prop), Kernel.deterministic_comp_eq_map]
    ext
    rw [Kernel.map_apply _ (by fun_prop), Kernel.parallelComp_apply]
    simp [Kernel.discard_apply]

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

Goal state before:
pp: case a
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
a✝ : IsFiniteMeasure (κ ω')
hε : 0 < ε
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-(t * ↑ε))
hl : Filter.Tendsto (fun t ↦ rexp (-(t * ↑ε))) Filter.atTop (𝓝 0)
⊢ (κ ω').real {ω | ↑ε ≤ X ω} ≤ 0

Tactic:
exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)

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
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) (⇑κ ∘ₘ ν)

Tactic:
convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)

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
t : ℝ
⊢ (↑2).HolderTriple (↑2) 1
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid W
inst✝ : Module A W
ρ : Representation A G W
σ : Subrepresentation ρ
v : W
⊢ v ∈ σ.asSubmodule ↔ v ∈ σ

Tactic:
by rfl

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hqX.localSeq n ⊓ hpX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω

Tactic:
rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, Set.ofPred_and,
    Set.inter_comm]

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess
      (fun i ↦
        ({a | ⊥ < hqX.localSeq n a} ∩ {a | ⊥ < hpX.localSeq n a}).indicator (stoppedProcess X (hpX.localSeq n) i))
      (hqX.localSeq n) i ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
M : Type u_4
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
m : M
⊢ m ∈ σ.asSubmodule' ↔ m ∈ σ

Tactic:
by rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
M : Type u_4
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] M
m : M
⊢ m ∈ ofSubmodule N ↔ m ∈ N

Tactic:
by rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
⊢ ∀ {a b : Subrepresentation ρ},
    { toFun := asSubmodule, invFun := ofSubmodule', left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := asSubmodule, invFun := ofSubmodule', left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
⊢ ∀ {a b : Submodule A[G] M},
    { toFun := ofSubmodule, invFun := asSubmodule', left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := ofSubmodule, invFun := asSubmodule', left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by rfl

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
i : ι
ω : Ω
⊢ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i) ω =
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n) i) ω

Tactic:
rw [stoppedProcess_indicator_comm', Set.indicator_indicator]

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
i : ι
ω : Ω
⊢ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i) ω =
    ({ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω} ∩ {ω | ⊥ < τ n ω}).indicator (stoppedProcess X (τ n) i) ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ ‖truncation f A x‖ ≤ |f x|

Tactic:
Real.norm_eq_abs

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f 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
Ω'' : 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)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ ∫ (x : Ω), rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x) ∂κ ω' ≤
    ∫ (x : Ω), rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2) ∂κ ω'

Tactic:
by
    refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
    · exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))
    · filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 μ
⊢ X =ᵐ[μ] 0

Tactic:
by
  simpa using (HasSubgaussianMGF_iff_kernel.1 h).ae_eq_zero_of_hasSubgaussianMGF_zero

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ (↑2).HolderTriple (↑2) 1
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ rexp (-(∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) ^ 2 / (2 * ↑(cX + cY))) =
    rexp (-(∫ (x : Ω), Y x ∂μ - ∫ (x : Ω), X x ∂μ) ^ 2 / (2 * (↑cX + ↑cY)))

Tactic:
congr 2
      grind

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 y : ρ.IntertwiningMap ρ),
    (equivLinearMapAsModule ρ ρ) (x * y) = (equivLinearMapAsModule ρ ρ) x * (equivLinearMapAsModule ρ ρ) y

Tactic:
intro f g; rfl

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
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ (comm σ ρ).symm = comm ρ σ

Tactic:
by rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
v : V
⊢ v ∈ ρ.invariants ↔ ∀ (g : G), (ρ g) v = v

Tactic:
by rfl

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 ω
⊢ ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
obtain ⟨c, -, cone, clim⟩ :
      ∃ c : ℕ → ℝ, StrictAnti c ∧ (∀ n : ℕ, 1 < c n) ∧ Tendsto c atTop (𝓝 1) :=
    exists_seq_strictAnti_tendsto (1 : ℝ)
  have : ∀ k, ∀ᵐ ω,
      Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ⌊c k ^ n⌋₊) atTop (𝓝 𝔼[X 0]) :=
    fun k => strong_law_aux6 X hint hindep hident hnonneg (cone k)
  filter_upwards [ae_all_iff.2 this] with ω hω
  apply tendsto_div_of_monotone_of_tendsto_div_floor_pow _ _ _ c cone clim _
  · intro m n hmn
    exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω
  · exact hω

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
x : (ρ.finsupp α).Coinvariants
⊢ (ρ.coinvariantsFinsuppLEquiv α) x = (ρ.coinvariantsToFinsupp α) x

Tactic:
by rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
by
  let A := k[G]
  let : Module k W := .compHom W (algebraMap k A)
  let : Module k V := .compHom V (algebraMap k A)
  have := IsScalarTower.of_compHom k A W
  have := IsScalarTower.of_compHom k A V
  set φ := (f.restrictScalars k).leftInverse
  have hφ : ∀ (x : V), φ (f x) = x := by
    apply LinearMap.leftInverse_apply_of_inj
    simp [hf]
  have _ : Fintype G := Fintype.ofFinite G
  refine ⟨φ.equivariantProjection G, LinearMap.ext ?_⟩
  exact φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| hφ

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B C : Rep k G
A : Action (ModuleCat k) G
g : G
⊢ ((RepToAction k G).obj ((ActionToRep k G).obj A)).ρ g ≫ 𝟙 ((RepToAction k G).obj ((ActionToRep k G).obj A)).V =
    𝟙 ((RepToAction k G).obj ((ActionToRep k G).obj A)).V ≫ A.ρ g

Tactic:
by rfl

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B C : Rep k G
A : Action (ModuleCat k) G
g : G
⊢ A.ρ g ≫ 𝟙 A.V = 𝟙 A.V ≫ ((RepToAction k G).obj ((ActionToRep k G).obj A)).ρ g

Tactic:
by rfl

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹⁴ : Monoid G
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : IsTopologicalAddGroup V
inst✝⁹ : Module R V
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : IsTopologicalAddGroup W
inst✝⁵ : Module R W
inst✝⁴ : AddCommGroup U
inst✝³ : Module R U
inst✝² : TopologicalSpace U
inst✝¹ : IsTopologicalAddGroup U
H : Type u_6
inst✝ : Monoid H
π : ContRepresentation R G V
π' : ContRepresentation R G W
φ : H →* G
f : π →ⁱL π'
h : H
⊢ f.toContinuousLinearMap ∘SL (π.restrict φ) h = (π'.restrict φ) h ∘SL f.toContinuousLinearMap

Tactic:
by
    ext; simp [f.toContinuousLinearMap_apply, f.isIntertwining]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom (α_ X Y Z).hom).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] z) = (↑(assoc X.ρ Y.ρ Z.ρ)).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] z)

Tactic:
by rfl

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
⊢ (Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g)) = x

Tactic:
ext γ

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
γ : G
⊢ ((Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g))).coeff γ = x.coeff γ
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: 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
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (X.d 1)) ↑σ = ↑0
⊢ ↑σ 1 ∈ X.ρ.invariants

Tactic:
simp only [mem_invariants]

Goal state after:
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
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (X.d 1)) ↑σ = ↑0
⊢ ∀ (g : G), (X.ρ g) (↑σ 1) = ↑σ 1
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero.left
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
      X₁ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
      X₂ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
      X₃ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
      f :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).f,
      g :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
      zero := ⋯ }.Exact

Tactic:
apply (forget₂ _ (ModuleCat k)).reflects_exact_of_faithful
        simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using!
          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv) ((Hom.hom (d k G n)) (single i (MonoidAlgebra.single 1 1))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))

Tactic:
rw [d_single (k := k), map_add, map_sum]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv) (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1)) +
      ∑ x,
        (Hom.hom (diagonalSuccIsoFree k G n).inv)
          (single (x.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑x + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))
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
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (δ hX i j hij)) ((ConcreteCategory.hom (π X.X₃ i)) (cocyclesMk z ⋯)) =
    (ConcreteCategory.hom (π X.X₁ j)) (cocyclesMkOfCompEqD hX hx)

Tactic:
by
  exact (map_cochainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x
    (by simpa using! hx) (j + 1) (by simp)

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 : ↑A
hx✝ : x ∈ A.ρ.invariants
g : G
hx : (A.ρ g) x - x = 0
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A)) ⟨x, hx✝⟩ g = (ModuleCat.Hom.hom 0) ⟨x, hx✝⟩ g

Tactic:
exact hx

Goal state after: