mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
      ((X.toCoinvariants S).ρ.ofQuotient S) ↑g =
    ((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
      ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
ext

Goal state after:
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 : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↑X
⊢ ((ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
          ((X.toCoinvariants S).ρ.ofQuotient S) ↑g) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝
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
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
        isIntertwining' := ⋯ } =
    𝟙 (X.quotientToCoinvariants S)

Tactic:
ext

Goal state after:
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✝
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✝
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
        isIntertwining' := ⋯ } =
    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' := ⋯ }

Tactic:
ext

Goal state after:
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✝
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
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) =
    (resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝

Tactic:
ext

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.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
x✝ : ↑X✝
⊢ (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝))).toLinearMap x✝ =
    (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f g : A ⟶ B
h : B ⟶ C
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
by
  ext : 1; simp [hom_add, ContIntertwiningMap.comp_add]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom ((r • f) ≫ g)).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom (f ≫ (r • g))).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝
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
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
x✝² x✝¹ : π₁ →ⁱL π₂
x✝ : (fun f ↦ f.toIntertwiningMap) x✝² = (fun f ↦ f.toIntertwiningMap) x✝¹
⊢ x✝² = x✝¹

Tactic:
ext

Goal state after:
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
x✝³ x✝² : π₁ →ⁱL π₂
x✝¹ : (fun f ↦ f.toIntertwiningMap) x✝³ = (fun f ↦ f.toIntertwiningMap) x✝²
x✝ : V
⊢ x✝³.toContinuousLinearMap x✝ = x✝².toContinuousLinearMap x✝
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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ f.toContinuousLinearMap ∘SL g.toContinuousLinearMap ∘SL π₁ h =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

Tactic:
g.2,

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

Tactic:
ext

Goal state after:
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✝
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 π₂
⊢ (f + g).comp h = f.comp h + g.comp h

Tactic:
ext

Goal state after:
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✝
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 π₂
⊢ (f - g).comp h = f.comp h - g.comp h

Tactic:
ext

Goal state after:
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✝
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 π₂
⊢ f.comp (g - h) = f.comp g - f.comp h

Tactic:
ext

Goal state after:
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✝
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
S : Type u_7
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S U
inst✝² : SMulCommClass R S U
inst✝¹ : ContinuousConstSMul S U
inst✝ : LinearMap.CompatibleSMul U U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
⊢ (s • f).comp g = s • f.comp g

Tactic:
ext

Goal state after:
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
S : Type u_7
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S U
inst✝² : SMulCommClass R S U
inst✝¹ : ContinuousConstSMul S U
inst✝ : LinearMap.CompatibleSMul U U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
x✝ : V
⊢ ((s • f).comp g).toContinuousLinearMap x✝ = (s • f.comp g).toContinuousLinearMap x✝
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
S : Type u_7
inst✝⁹ : Monoid S
inst✝⁸ : DistribMulAction S U
inst✝⁷ : SMulCommClass R S U
inst✝⁶ : ContinuousConstSMul S U
inst✝⁵ : LinearMap.CompatibleSMul U U S R
inst✝⁴ : DistribMulAction S W
inst✝³ : SMulCommClass R S W
inst✝² : ContinuousConstSMul S W
inst✝¹ : LinearMap.CompatibleSMul W W S R
inst✝ : LinearMap.CompatibleSMul W U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
⊢ f.comp (s • g) = s • f.comp g

Tactic:
ext

Goal state after:
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
S : Type u_7
inst✝⁹ : Monoid S
inst✝⁸ : DistribMulAction S U
inst✝⁷ : SMulCommClass R S U
inst✝⁶ : ContinuousConstSMul S U
inst✝⁵ : LinearMap.CompatibleSMul U U S R
inst✝⁴ : DistribMulAction S W
inst✝³ : SMulCommClass R S W
inst✝² : ContinuousConstSMul S W
inst✝¹ : LinearMap.CompatibleSMul W W S R
inst✝ : LinearMap.CompatibleSMul W U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
x✝ : V
⊢ (f.comp (s • g)).toContinuousLinearMap x✝ = (s • f.comp g).toContinuousLinearMap x✝
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝² x✝¹ : S
x✝ : π₁ →ⁱL π₂
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext

Goal state after:
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝³ x✝² : S
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ ((x✝³ * x✝²) • x✝¹).toContinuousLinearMap x✝ = (x✝³ • x✝² • x✝¹).toContinuousLinearMap x✝
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝ : π₁ →ⁱL π₂
⊢ 1 • x✝ = x✝

Tactic:
ext

Goal state after:
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (1 • x✝¹).toContinuousLinearMap x✝ = x✝¹.toContinuousLinearMap x✝
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
ext

Goal state after:
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : S
x✝ : V
⊢ (x✝¹ • 0).toContinuousLinearMap x✝ = (toContinuousLinearMap 0) x✝
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝² : S
x✝¹ x✝ : π₁ →ⁱL π₂
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
ext

Goal state after:
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
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝³ : S
x✝² x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (x✝³ • (x✝² + x✝¹)).toContinuousLinearMap x✝ = (x✝³ • x✝² + x✝³ • x✝¹).toContinuousLinearMap x✝