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

Goal state before:
pp: case zero
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
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 ∈ σ.toSubmodule.carrier

Tactic:
;

Goal state after:
case zero
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
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
⊢ 0 ∈ σ.toSubmodule.carrier
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case add
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
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • m ∈ σ.toSubmodule.carrier

Tactic:
;

Goal state after:
case add
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
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
x y : A[G]
hx : x • m ∈ σ.toSubmodule.carrier
hy : y • m ∈ σ.toSubmodule.carrier
⊢ x • m + y • m ∈ σ.toSubmodule.carrier
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
⊢ (fun x ↦ 0) ∘ f = 0

Tactic:
;

Goal state after:
α : Type u_1
f : α → ℝ
⊢ (fun x ↦ 0) ∘ f = 0
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ MemLp (truncation f A) 1 μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : ¬SFinite ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
;

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : ¬SFinite ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
;

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : ¬IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

pp: case pos
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
;

Goal state after:
case neg
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : ¬IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

case pos
Ω : 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : 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 κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

pp: case pos
Ω : 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 κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
;

Goal state after:
case neg
Ω : 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 κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

case pos
Ω : 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 κ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case e_s
ι : 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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω x✝ : Ω
⊢ x✝ ∈ {ω | ⊥ < hL.localSeq n ω ∧ ⊥ < τ n (nk n) ω} ↔ x✝ ∈ {ω | ⊥ < τ n (nk n) ω} ∩ {ω | ⊥ < hL.localSeq n ω}

Tactic:
;

Goal state after:
case e_s
ι : 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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω x✝ : Ω
⊢ x✝ ∈ {ω | ⊥ < hL.localSeq n ω ∧ ⊥ < τ n (nk n) ω} ↔ x✝ ∈ {ω | ⊥ < τ n (nk n) ω} ∩ {ω | ⊥ < hL.localSeq n ω}
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: case e_f
ι : 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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ stoppedProcess X (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i = stoppedProcess X (τ n (nk n) ⊓ hL.localSeq n) i

Tactic:
inf_comm

Goal state after:
case e_f
ι : 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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ stoppedProcess X (fun ω ↦ min (τ n (nk n) ω) (hL.localSeq n ω)) i = stoppedProcess X (τ n (nk n) ⊓ hL.localSeq n) i
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ 1)) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    ((1 ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ 1)) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    ((1 ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x✝² x✝¹ : G
x✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ (x✝² * x✝¹))) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff
      a✝ =
    (((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝²)) *
              MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝¹))) ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x✝² x✝¹ : G
x✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ (x✝² * x✝¹))) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff
      a✝ =
    (((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝²)) *
              MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝¹))) ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
x : X.V
y : Y.V
⊢ (((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom) ∘ₗ (linearize k G X) g) ∘ₗ
            MonoidAlgebra.lsingle x)
          1).coeff
      y =
    ((((linearize k G Y) g ∘ₗ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom)) ∘ₗ
            MonoidAlgebra.lsingle x)
          1).coeff
      y

Tactic:
;

Goal state after:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
x : X.V
y : Y.V
⊢ (((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom) ∘ₗ (linearize k G X) g) ∘ₗ
            MonoidAlgebra.lsingle x)
          1).coeff
      y =
    ((((linearize k G Y) g ∘ₗ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom)) ∘ₗ
            MonoidAlgebra.lsingle x)
          1).coeff
      y
Module: Mathlib.RepresentationTheory.Action

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
x✝ : (𝟙_ (Action (Type u) G)).V
a✝ : (𝟙_ (Action (Type u) G)).V
⊢ ((((ε k G).comp (η k G)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (𝟙_ (Action (Type u) G)))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
x✝ : (𝟙_ (Action (Type u) G)).V
a✝ : (𝟙_ (Action (Type u) G)).V
⊢ ((((ε k G).comp (η k G)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (𝟙_ (Action (Type u) G)))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
⊢ ((η k G).comp (ε k G)).toLinearMap 1 = (IntertwiningMap.id (trivial k G k)).toLinearMap 1

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
⊢ ((η k G).comp (ε k G)).toLinearMap 1 = (IntertwiningMap.id (trivial k G k)).toLinearMap 1
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
x✝¹ : X.V
x✝ : Y.V
a✝ : (X ⊗ Y).V
⊢ (((TensorProduct.AlgebraTensorModule.curry
                  (↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g) ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)) ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
;

Goal state after:
k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
x✝¹ : X.V
x✝ : Y.V
a✝ : (X ⊗ Y).V
⊢ (((TensorProduct.AlgebraTensorModule.curry
                  (↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g) ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)) ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
x✝¹ : X.V
x✝ : Y.V
a✝ : (X ⊗ Y).V
⊢ (Finsupp.single ((ConcreteCategory.hom (X.ρ g)) x✝¹, (ConcreteCategory.hom (Y.ρ g)) x✝) 1) a✝ =
    (Finsupp.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) (x✝¹, x✝)) 1) a✝

Tactic:
;

Goal state after:
k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
x✝¹ : X.V
x✝ : Y.V
a✝ : (X ⊗ Y).V
⊢ (Finsupp.single ((ConcreteCategory.hom (X.ρ g)) x✝¹, (ConcreteCategory.hom (Y.ρ g)) x✝) 1) a✝ =
    (Finsupp.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) (x✝¹, x✝)) 1) a✝
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
r s : k
a✝ : (X ⊗ Y).V
⊢ ((μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s)).coeff a✝ =
    (MonoidAlgebra.single (x, y) (r * s)).coeff a✝

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
r s : k
a✝ : (X ⊗ Y).V
⊢ ((μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s)).coeff a✝ =
    (MonoidAlgebra.single (x, y) (r * s)).coeff a✝