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

Goal state before:
pp: case e'_8
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ 1 = ↑⌊c ^ n⌋₊ * (↑⌊c ^ n⌋₊)⁻¹

Tactic:
;

Goal state after:
case e'_8
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ 1 = ↑⌊c ^ n⌋₊ * (↑⌊c ^ n⌋₊)⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Monoid G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : FiniteDimensional k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ (ρ.tprod σ).character g = (ρ.character * σ.character) g

Tactic:
;

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Monoid G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : FiniteDimensional k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ (ρ.tprod σ).character g = (ρ.character * σ.character) g
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : FiniteDimensional k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ Invertible ↑(Nat.card G)

Tactic:
;

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Field k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : FiniteDimensional k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ Invertible ↑(Nat.card G)
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g

Tactic:
;

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| (↑(Nat.card G))⁻¹

pp: case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹

Tactic:
;

Goal state after:
case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| (↑(Nat.card G))⁻¹

case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹

Tactic:
;

Goal state after:
case a
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| ∑ g, W.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.s
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| Finset.univ

pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹

Tactic:
;

Goal state after:
case a.s
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| Finset.univ

case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹

Tactic:
;

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| W.character x✝ * V.character x✝⁻¹

Tactic:
;

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| W.character x✝ * V.character 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
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯) x✝¹) x✝ = ↑(1 x✝¹) x✝

Tactic:
;

Goal state after:
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
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯) x✝¹) x✝ = ↑(1 x✝¹) 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
x✝³ x✝² : H
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * (x✝³ * x✝²)).restrict ⋯) x✝¹) x✝ =
    ↑(((LinearMap.funLeft k B fun x ↦ x * x✝³).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝²).restrict ⋯) x✝¹) x✝

Tactic:
;

Goal state after:
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
x✝³ x✝² : H
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * (x✝³ * x✝²)).restrict ⋯) x✝¹) x✝ =
    ↑(((LinearMap.funLeft k B fun x ↦ x * x✝³).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝²).restrict ⋯) x✝¹) 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
f : σ.IntertwiningMap ρ
h : H
x✝¹ : ↥(coindV φ σ)
x✝ : H
⊢ ↑(((f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h) x✝¹) x✝ = ↑(((coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯) x✝¹) x✝

Tactic:
;

Goal state after:
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
x✝¹ : ↥(coindV φ σ)
x✝ : H
⊢ ↑(((f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h) x✝¹) x✝ = ↑(((coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯) x✝¹) x✝
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✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := ⋯
s✝ : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s✝ b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := ⋯
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
s : ↥S
g : G
⊢ ↑(γ (↑s * g)) = ↑(s * γ g)

Tactic:
;

Goal state after:
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := ⋯
s✝ : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s✝ b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := ⋯
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
s : ↥S
g : G
⊢ ↑(γ (↑s * g)) = ↑(s * γ g)
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
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap
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
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
h : H
⊢ ((Hom.hom f).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1 = ((Hom.hom g).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
h : H
⊢ ((Hom.hom f).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1 = ((Hom.hom g).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1
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
x✝ : res φ (leftRegular k H) ⟶ A
h✝ : H
⊢ (Hom.hom ((Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1)

Tactic:
;

Goal state after:
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
x✝ : res φ (leftRegular k H) ⟶ A
h✝ : H
⊢ (Hom.hom ((Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1)
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
f : ↥(Representation.coindV φ A.ρ)
g : G
⊢ (linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g) =
    A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : ↥(Representation.coindV φ A.ρ)
g : G
⊢ (linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g) =
    A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)
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
f : ↥(Representation.coindV φ A.ρ)
g : G
x✝ : H
⊢ (((linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f : ↥(Representation.coindV φ A.ρ)
g : G
x✝ : H
⊢ (((linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ MonoidAlgebra.lsingle x✝) 1
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ (map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ) x✝ = (LinearMap.id ∘ₗ mk ρ) x✝

Tactic:
;

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ (map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ) x✝ = (LinearMap.id ∘ₗ mk ρ) x✝
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
a✝¹ : α
x✝ : V
a✝ : α
⊢ (((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝¹) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
;

Goal state after:
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
a✝¹ : α
x✝ : V
a✝ : α
⊢ (((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝¹) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a✝¹) x✝) a✝
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
h : H
x✝ : ↥(Representation.coindV φ A.ρ)
h✝ : H
⊢ (Hom.hom ((↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1)

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
h : H
x✝ : ↥(Representation.coindV φ A.ρ)
h✝ : H
⊢ (Hom.hom ((↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1)
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
a✝¹ : α
x✝ : V
a✝ : α
⊢ ((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝ =
    (((LinearMap.id ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝

Tactic:
;

Goal state after:
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
a✝¹ : α
x✝ : V
a✝ : α
⊢ ((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝ =
    (((LinearMap.id ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝
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
a✝ : α
x✝ : V
⊢ (((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝ =
    ((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝

Tactic:
;

Goal state after:
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
a✝ : α
x✝ : V
⊢ (((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝ =
    ((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝
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
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
              (ρ.tprod (leftRegular k G)) x✝²))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
              ↑(_root_.TensorProduct.comm k V k[G])))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
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
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
              (ρ.tprod (leftRegular k G)) x✝²))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
              ↑(_root_.TensorProduct.comm k V k[G])))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
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✝ : V
⊢ (ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
        Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1))
      x✝ =
    LinearMap.id x✝

Tactic:
;

Goal state after:
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✝ : V
⊢ (ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
        Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1))
      x✝ =
    LinearMap.id x✝