mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g : G
⊢ ↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                finsuppTensorFinsupp' k G α ≪≫ₗ
              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
            curryLinearEquiv k ≪≫ₗ
          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm) ∘ₗ
      ((leftRegular k G).tprod (trivial k G k[α])) g =
    (free k G α) g ∘ₗ
      ↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                finsuppTensorFinsupp' k G α ≪≫ₗ
              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
            curryLinearEquiv k ≪≫ₗ
          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm)

Tactic:
by ext; simp

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω)) (μ.trim hm)

Tactic:
by
    refine (hX.integrable_exp_mul t).trim hm ?_
    exact Measurable.stronglyMeasurable <| by fun_prop

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✝⁵ : Semiring 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
φ : ρ.Equiv σ
⊢ φ.trans φ.symm = refl ρ

Tactic:
by ext; simp

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✝⁵ : Semiring 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
φ : ρ.Equiv σ
⊢ φ.symm.trans φ = refl σ

Tactic:
by ext; simp

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
g₁ g₂ : ρ.IntertwiningMap σ
⊢ { toFun := ⇑(g₁ + g₂).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑g₁.toLinearMap, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := ⇑g₂.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp

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
t : A
g : ρ.IntertwiningMap σ
⊢ { toFun := ⇑(t • g).toLinearMap, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) t • { toFun := ⇑g.toLinearMap, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp

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

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

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

Tactic:
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
a : A
f g : ρ.IntertwiningMap ρ
⊢ f * a • g = a • (f * g)

Tactic:
by ext; simp

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
⊢ centralAlgebraMul ρ ⋯ = 1

Tactic:
by ext; simp

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✝ : ↥(Submonoid.center A[G])
⊢ centralAlgebraMul ρ ⋯ = centralAlgebraMul ρ ⋯ * centralAlgebraMul ρ ⋯

Tactic:
by ext; simp

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
⊢ lTensor ρ (id σ) = id (ρ.tprod σ)

Tactic:
by ext; simp

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
⊢ lTensor ρ 0 = 0

Tactic:
by ext; simp

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
⊢ rTensor ρ (id σ) = id (σ.tprod ρ)

Tactic:
by ext; simp

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
⊢ rTensor ρ 0 = 0

Tactic:
by ext; simp

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
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (rTensor υ f).comp (lTensor ρ g) = f.tensor g

Tactic:
by ext; simp

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
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (lTensor τ g).comp (rTensor σ f) = f.tensor g

Tactic:
by ext; simp

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
g : G
⊢ ↑(_root_.TensorProduct.comm A V W) ∘ₗ (ρ.tprod σ) g = (σ.tprod ρ) g ∘ₗ ↑(_root_.TensorProduct.comm A V W)

Tactic:
by ext; simp

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 : σ.IntertwiningMap τ
⊢ (↑(comm ρ τ)).comp (IntertwiningMap.lTensor ρ f) = (IntertwiningMap.rTensor ρ f).comp ↑(comm ρ σ)

Tactic:
by ext; simp

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 : σ.IntertwiningMap τ
⊢ (↑(comm τ ρ)).comp (IntertwiningMap.rTensor ρ f) = (IntertwiningMap.lTensor ρ f).comp ↑(comm σ ρ)

Tactic:
by ext; simp

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
g : G
⊢ ↑(_root_.TensorProduct.assoc A V W U) ∘ₗ ((ρ.tprod σ).tprod τ) g =
    (ρ.tprod (σ.tprod τ)) g ∘ₗ ↑(_root_.TensorProduct.assoc A V W U)

Tactic:
by ext; simp

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
g : G
⊢ ↑(_root_.TensorProduct.rid A W) ∘ₗ (σ.tprod (trivial A G A)) g = σ g ∘ₗ ↑(_root_.TensorProduct.rid A W)

Tactic:
by ext; simp

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
g : G
⊢ ↑(_root_.TensorProduct.lid A W) ∘ₗ ((trivial A G A).tprod σ) g = σ g ∘ₗ ↑(_root_.TensorProduct.lid A W)

Tactic:
by ext; simp

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
hf : Function.Surjective ⇑f
X Y : Rep k G
f' : (resFunctor f).obj X ⟶ (resFunctor f).obj Y
⊢ (resFunctor f).map (liftHomOfSurj f hf f') = f'

Tactic:
by ext; simp

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
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⌋₊
⊢ (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
apply Asymptotics.isLittleO_iff.2 fun ε εpos => ?_

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
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 < ε
⊢ ∀ᶠ (x : ℕ) in atTop,
    ‖∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a‖ ≤
      ε * ‖↑⌊c ^ x⌋₊‖
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
⊢ (LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯ = 1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
h : H
⊢ (f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h = (coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
A B : Rep k G
f : A ⟶ B
h : H
⊢ Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h =
    (Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
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✝ : G
⊢ mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝ = mapRange.linearMap (Coinvariants.mk ρ)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
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
⊢ ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
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
⊢ ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝ : G
⊢ (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
      (ρ.tprod (leftRegular k G)) x✝ =
    TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      ↑(_root_.TensorProduct.comm k V k[G])

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
      Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1) =
    LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ (Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
      ρ.ofCoinvariantsTprodLeftRegular =
    LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
⊢ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g =
    A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
x : res φ B ⟶ A
⊢ (fun f ↦
        ofHom
          { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
            isIntertwining' := ⋯ })
      ((fun f ↦ resCoindToHom φ B A f) x) =
    x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝¹ ≫ x✝))) =
    ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝¹)) ≫
      ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝))

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X : Rep k G
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g =
    (Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ ModuleCat.Hom.hom ((coinvariantsMk k G).app X)

Tactic:
by ext; simp

Goal state after: