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

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
⊢ σ γ ∘ₗ f ∘ₗ ρ γ⁻¹ = f

Tactic:
ext v
    simp [hf.isIntertwining]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group 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
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ ↑(finrank k (ρ.IntertwiningMap ρ)) = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a)) →
    Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
hωneg

Goal state after:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x✝¹ x✝ : E
⊢ Function.const E c x✝ = 1 x✝ • c

Tactic:
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
⊢ 0 ∈ {f | ∀ (g : G) (h : H), f (φ g * h) = (σ g) (f h)}

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

Tactic:
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
x✝¹ : ↥(coindV φ σ)
x✝ : H
⊢ ↑(((f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h) x✝¹) x✝ = ↑(((coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯) x✝¹) x✝

Tactic:
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✝
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 := QuotientGroup.rightRel S
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 := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
s : ↥S
g : G
⊢ g * (↑s * g)⁻¹ ∈ S

Tactic:
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
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:
simp

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
S : Subgroup G
inst✝ : S.Normal
g : G
x✝¹ : V
x✝ : x✝¹ ∈ Set.range fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2
s : ↥S
x : V
hs : (fun gv ↦ ((MonoidHom.comp ρ S.subtype) gv.1) gv.2 - gv.2) (s, x) = x✝¹
⊢ ((MonoidHom.comp ρ S.subtype) ⟨g * ↑s * g⁻¹, ⋯⟩) ((ρ g) x) - (ρ g) x = (ρ g) ((ρ ↑s) x) - (ρ g) x

Tactic:
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
x : ↥(Representation.coindV φ A.ρ)
⊢ (fun f ↦ ⟨fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1), ⋯⟩)
      ((fun f ↦
          ofHom { toLinearMap := linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k), isIntertwining' := ⋯ })
        x) =
    x

Tactic:
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
x : res φ (leftRegular k H) ⟶ A
x✝ : H
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k), isIntertwining' := ⋯ })
            ((fun f ↦ ⟨fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1), ⋯⟩) x))).toLinearMap
      (MonoidAlgebra.single x✝ 1) =
    (Hom.hom x).toLinearMap (MonoidAlgebra.single x✝ 1)

Tactic:
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
a✝¹ : α
x✝ : V
a✝ : α
⊢ (((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝¹) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
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
a : α
g : G
x : V
⊢ ((ρ.finsupp α) g) (single a x) - single a x = (lsingle a) ((ρ g) x) - (lsingle a) x

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: 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
y : W
g : G
⊢ ((ρ.tprod τ) g⁻¹) (x ⊗ₜ[k] (τ g) y) - x ⊗ₜ[k] (τ g) y = (ρ g⁻¹) x ⊗ₜ[k] y - x ⊗ₜ[k] (τ g) y

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: 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
y : W
g : G
⊢ ((ρ.tprod τ) g⁻¹) ((ρ g) x ⊗ₜ[k] y) - (ρ g) x ⊗ₜ[k] y = x ⊗ₜ[k] (τ g⁻¹) y - (ρ g) x ⊗ₜ[k] y

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

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

Tactic:
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
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
x✝¹ : ↑B
x✝ : H
⊢ ↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
            ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g) ⋯)
          x✝¹)
      x✝ =
    ↑(((Representation.coind φ A.ρ) g ∘ₗ
            LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h)
              ⋯)
          x✝¹)
      x✝

Tactic:
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
x✝ : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
⊢ ((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g) x✝ =
    (A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) x✝

Tactic:
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
⊢ ModuleCat.ofHom (Coinvariants.map x✝.ρ x✝.ρ (Hom.hom (𝟙 x✝))) = 𝟙 (ModuleCat.of k x✝.ρ.Coinvariants)

Tactic:
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
x✝ : ↑(of (MonoidHom.comp B.ρ φ))
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                  isIntertwining' := ⋯ })
            ((fun f ↦ resCoindToHom φ B A f) x))).toLinearMap
      x✝ =
    (Hom.hom x).toLinearMap x✝

Tactic:
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✝
x✝ : ↑X✝
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝² ≫ x✝¹)))) ∘ₗ Coinvariants.mk X✝.ρ) x✝ =
    (ModuleCat.Hom.hom
          (ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝²)) ≫
            ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝¹))) ∘ₗ
        Coinvariants.mk X✝.ρ)
      x✝

Tactic:
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
x✝ : ↑X
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g) x✝ =
    ((Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ
        ModuleCat.Hom.hom ((coinvariantsMk k G).app X))
      x✝

Tactic:
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 : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
x✝ : ↑X
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((Hom.hom (𝟙 (X.quotientToCoinvariants S))).toLinearMap ∘ₗ Coinvariants.mk (MonoidHom.comp X.ρ S.subtype)) x✝

Tactic:
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 : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝ =
    ((Hom.hom
            (ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)),
                  isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map g)),
                  isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝

Tactic:
simp

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
g : G
⊢ ContinuousLinearMap.id R V ∘SL π₁ g = π₁ g ∘SL ContinuousLinearMap.id R V

Tactic:
simp

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g h : π₁ →ⁱL π₂
x✝ : V
⊢ (f.comp (g + h)).toContinuousLinearMap x✝ = (f.comp g + f.comp h).toContinuousLinearMap x✝

Tactic:
simp

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f g : π₂ →ⁱL π₃
h : π₁ →ⁱL π₂
x✝ : V
⊢ ((f + g).comp h).toContinuousLinearMap x✝ = (f.comp h + g.comp h).toContinuousLinearMap x✝

Tactic:
simp

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
⊢ ∀ (g : G), 0 ∘SL π₁ g = π₂ g ∘SL 0

Tactic:
simp

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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f g : π₂ →ⁱL π₃
h : π₁ →ⁱL π₂
x✝ : V
⊢ ((f - g).comp h).toContinuousLinearMap x✝ = (f.comp h - g.comp h).toContinuousLinearMap x✝

Tactic:
simp

Goal state after: