mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module 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✝² • x✝¹).toContinuousLinearMap x✝

Tactic:
;

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
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module 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✝² • 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
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (0 • x✝¹).toContinuousLinearMap x✝ = (toContinuousLinearMap 0) x✝

Tactic:
;

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
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (0 • x✝¹).toContinuousLinearMap x✝ = (toContinuousLinearMap 0) x✝
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''
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
ψ : σ.Equiv ρ
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv =
    ψ.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ

Tactic:
;

Goal state after:
case mk''
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
ψ : σ.Equiv ρ
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv =
    ψ.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''.mk''
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
toContinuousLinearEquiv✝¹ : W ≃L[R] V
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
        isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }

Tactic:
;

Goal state after:
case mk''.mk''
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
toContinuousLinearEquiv✝¹ : W ≃L[R] V
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : W ≃L[R] V
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL σ g =
      ρ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹,
        isIntertwining' := isIntertwining'✝¹ }.toContinuousLinearEquiv =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
        isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''
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
φ ψ : ρ.Equiv σ
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h1 :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
          isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv =
    ⇑ψ.toContinuousLinearEquiv
h2 :
  (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
            isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv).invFun =
    (↑ψ.toContinuousLinearEquiv).invFun
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ

Tactic:
;

Goal state after:
case mk''
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
φ ψ : ρ.Equiv σ
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h1 :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
          isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv =
    ⇑ψ.toContinuousLinearEquiv
h2 :
  (↑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝,
            isIntertwining' := isIntertwining'✝ }.toContinuousLinearEquiv).invFun =
    (↑ψ.toContinuousLinearEquiv).invFun
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''
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
ψ : ρ.Equiv σ
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h : ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ⇑ψ
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ

Tactic:
;

Goal state after:
case mk''
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
ψ : ρ.Equiv σ
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h : ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ⇑ψ
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ } = ψ
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A : Rep k G
g1 g2 : G
x✝ : ↑A
⊢ (A.ρ (g1 * g2)) x✝ = (A.ρ g1 ∘ₗ A.ρ g2) x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A : Rep k G
g1 g2 : G
x✝ : ↑A
⊢ (A.ρ (g1 * g2)) x✝ = (A.ρ g1 ∘ₗ A.ρ g2) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
x✝ : ↑A
⊢ (Hom.hom (A.applyAsHom g ≫ f)).toLinearMap x✝ = (Hom.hom (f ≫ B.applyAsHom g)).toLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
x✝ : ↑A
⊢ (Hom.hom (A.applyAsHom g ≫ f)).toLinearMap x✝ = (Hom.hom (f ≫ B.applyAsHom g)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A : Rep k G
x : ↑A
g x✝ : G
⊢ (((((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          (Representation.ofMulAction k G G) g) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ ((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A : Rep k G
x : ↑A
g x✝ : G
⊢ (((((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          (Representation.ofMulAction k G G) g) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ ((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X Y : Rep k G
f g : X ⟶ Y
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (f + g)) =
    ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map f + (forget₂ (Rep k G) (ModuleCat k)).map g)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X Y : Rep k G
f g : X ⟶ Y
⊢ ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (f + g)) =
    ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map f + (forget₂ (Rep k G) (ModuleCat k)).map g)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom (𝟙 A)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom (𝟙 A)
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
φ : ρ.Equiv σ
x✝ : V
⊢ (φ.trans φ.symm) x✝ = (refl ρ) x✝

Tactic:
;

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
φ : ρ.Equiv σ
x✝ : V
⊢ (φ.trans φ.symm) x✝ = (refl ρ) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom 0

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom 0
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
φ : ρ.Equiv σ
x✝ : W
⊢ (φ.symm.trans φ) x✝ = (refl σ) x✝

Tactic:
;

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
φ : ρ.Equiv σ
x✝ : W
⊢ (φ.symm.trans φ) x✝ = (refl σ) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom 0

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom 0
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
H : Type u_6
inst✝ : Monoid H
π : ContRepresentation R G V
π' : ContRepresentation R G W
φ : H →* G
f : π →ⁱL π'
h : H
x✝ : V
⊢ (f.toContinuousLinearMap ∘SL (π.restrict φ) h) x✝ = ((π'.restrict φ) h ∘SL f.toContinuousLinearMap) x✝

Tactic:
;

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
H : Type u_6
inst✝ : Monoid H
π : ContRepresentation R G V
π' : ContRepresentation R G W
φ : H →* G
f : π →ⁱL π'
h : H
x✝ : V
⊢ (f.toContinuousLinearMap ∘SL (π.restrict φ) h) x✝ = ((π'.restrict φ) h ∘SL f.toContinuousLinearMap) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom (𝟙 B)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom (𝟙 B)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
this : x = 0
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : ↑(trivial k G PUnit.{w + 1})
this : x = 0
⊢ (Hom.hom f).toLinearMap x = (Hom.hom default).toLinearMap x
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
habs : φ ≫ ι = 0
hιφ : 𝟙 (Abelian.image f) = ι ≫ φ
⊢ False

Tactic:
apply_fun (· ≫ ι) at hιφ

Goal state after:
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
habs : φ ≫ ι = 0
hιφ : 𝟙 (Abelian.image f) ≫ ι = (ι ≫ φ) ≫ ι
⊢ False
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ (Hom.hom f).toLinearMap 0 = (Hom.hom default).toLinearMap 0

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ (Hom.hom f).toLinearMap 0 = (Hom.hom default).toLinearMap 0