awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
h_inj :
  Eq (α := Submodule k V)
    (LinearMap.ker
      ((↑k :
          {S : Type (max u_1 u_2)} →
            {M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring k] →
                  [inst_8 : Semiring S] →
                    [inst_9 : AddCommMonoid M] →
                      [inst_10 : AddCommMonoid M₂] →
                        [inst_11 : Module k M] →
                          [inst_12 : Module k M₂] →
                            [inst_13 : Module S M] →
                              [inst_14 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
        f))
    ⊥
⊢ ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x

Tactic:
apply LinearMap.leftInverse_apply_of_inj

Premises used: LinearMap.leftInverse_apply_of_inj
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
⊢ Eq (α := Submodule k V)
    (LinearMap.ker
      ((↑k :
          {S : Type (max u_1 u_2)} →
            {M : Type u_3} →
              {M₂ : Type u_4} →
                [inst : Semiring k] →
                  [inst_8 : Semiring S] →
                    [inst_9 : AddCommMonoid M] →
                      [inst_10 : AddCommMonoid M₂] →
                        [inst_11 : Module k M] →
                          [inst_12 : Module k M₂] →
                            [inst_13 : Module S M] →
                              [inst_14 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
        f))
    ⊥

Tactic:
simp [hf]
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
⊢ ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x

Tactic:
have hφ : ∀ (x : V), φ (f x) = x := by
    apply LinearMap.leftInverse_apply_of_inj
    simp [hf]
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
have : ∀ (x : Fintype G), ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id

Tactic:
have _ : Fintype G := Fintype.ofFinite G
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
x : Fintype G
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id

Tactic:
⟨φ.equivariantProjection G, LinearMap.ext ?_⟩

Premises used: LinearMap.equivariantProjection, LinearMap.ext, Exists.intro
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
x : Fintype G
refine :
  ∀ (x_1 : V),
    Eq (α := V) ((LinearMap.equivariantProjection G φ ∘ₗ f : (a : V) → V) x_1 : V)
      ((LinearMap.id : (a : V) → V) x_1 : V)
⊢ ∃ (g : LinearMap (R := k[G]) (RingHom.id k[G]) W V), g ∘ₗ f = LinearMap.id

Tactic:
refine ⟨φ.equivariantProjection G, LinearMap.ext ?_⟩
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
x : Fintype G
⊢ ∀ (x_1 : V),
    Eq (α := V) ((LinearMap.equivariantProjection G φ ∘ₗ f : (a : V) → V) x_1 : V)
      ((LinearMap.id : (a : V) → V) x_1 : V)

Tactic:
φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| hφ

Premises used: LinearMap.equivariantProjection_condition, IsUnit.mk0, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
f : LinearMap (R := k[G]) (RingHom.id k[G]) V W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this_1 : Module k W := Module.compHom W (algebraMap k A)
this_2 : Module k V := Module.compHom V (algebraMap k A)
this_3 : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V :=
  LinearMap.leftInverse
    ((↑k :
        {S : Type (max u_1 u_2)} →
          {M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring k] →
                [inst_8 : Semiring S] →
                  [inst_9 : AddCommMonoid M] →
                    [inst_10 : AddCommMonoid M₂] →
                      [inst_11 : Module k M] →
                        [inst_12 : Module k M₂] →
                          [inst_13 : Module S M] →
                            [inst_14 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ k S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[k] M₂)
      f)
hφ : ∀ (x : V), (φ : (a : W) → V) ((f : (a : V) → W) x : W) = x
x : Fintype G
⊢ ∀ (x_1 : V),
    Eq (α := V) ((LinearMap.equivariantProjection G φ ∘ₗ f : (a : V) → V) x_1 : V)
      ((LinearMap.id : (a : V) → V) x_1 : V)

Tactic:
exact φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| hφ

Premises used: LinearMap.equivariantProjection_condition, IsUnit.mk0, NeZero.ne
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
p : Submodule k[G] V
rcases :
  ∀ (f : LinearMap (R := k[G]) (RingHom.id k[G]) V ↥p) (hf : f ∘ₗ p.subtype = LinearMap.id),
    ∃ (q : Submodule k[G] V), IsCompl p q
⊢ ∃ (q : Submodule k[G] V), IsCompl p q

Tactic:
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩

Premises used: MonoidAlgebra.exists_leftInverse_of_injective, Submodule.ker_subtype, Submodule.subtype
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
p : Submodule k[G] V
f : LinearMap (R := k[G]) (RingHom.id k[G]) V ↥p
hf : f ∘ₗ p.subtype = LinearMap.id
⊢ ∃ (q : Submodule k[G] V), IsCompl p q

Tactic:
⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩

Premises used: DFunLike.congr_fun, LinearMap.ker, Exists.intro, LinearMap.isCompl_of_proj
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
p : Submodule k[G] V
f : LinearMap (R := k[G]) (RingHom.id k[G]) V ↥p
hf : f ∘ₗ p.subtype = LinearMap.id
⊢ ∃ (q : Submodule k[G] V), IsCompl p q

Tactic:
exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k : Type u_1
inst : Field k
G : Type u_2
inst_1 : Finite G
inst_2 : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
inst_3 : Group G
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Module k[G] V
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k[G] W
inst_8 : AddGroup G
rwa rwa₁ rwa₂ rwa₃ : NeZero.{u_1} (R := k) (↑(Nat.card G) : k)
⊢ NeZero.{u_1} (R := k) (↑(Nat.card.{u_2} (Multiplicative G)) : k)

Tactic:
rwa [Nat.card_congr Multiplicative.toAdd]

Premises used: Nat.card_congr, Multiplicative.toAdd
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k_1 : Type u_1
inst : Field k_1
G_1 : Type u_2
inst_1 : Finite G_1
inst_2 : NeZero.{u_1} (R := k_1) (↑(Nat.card G_1) : k_1)
inst_3 : Group G_1
V_1 : Type u_3
inst_4 : AddCommGroup V_1
inst_5 : Module k_1[G_1] V_1
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k_1[G_1] W
G : Type u_5
k : Type u_6
V : Type u_7
inst_8 : Group G
inst_9 : Field k
inst_10 : Finite G
inst_11 : NeZero.{u_6} (R := k) (↑(Nat.card G) : k)
inst_12 : AddCommGroup V
inst_13 : Module k V
ρ : Representation k G V
rw : IsSemisimpleModule k[G] ρ.asModule
⊢ ρ.IsSemisimpleRepresentation

Tactic:
rw [isSemisimpleRepresentation_iff_isSemisimpleModule_asModule]

Premises used: Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule
-- Module: Mathlib.RepresentationTheory.Maschke
Goal:
k_1 : Type u_1
inst : Field k_1
G_1 : Type u_2
inst_1 : Finite G_1
inst_2 : NeZero.{u_1} (R := k_1) (↑(Nat.card G_1) : k_1)
inst_3 : Group G_1
V_1 : Type u_3
inst_4 : AddCommGroup V_1
inst_5 : Module k_1[G_1] V_1
W : Type u_4
inst_6 : AddCommGroup W
inst_7 : Module k_1[G_1] W
G : Type u_5
k : Type u_6
V : Type u_7
inst_8 : Group G
inst_9 : Field k
inst_10 : Finite G
inst_11 : NeZero.{u_6} (R := k) (↑(Nat.card G) : k)
inst_12 : AddCommGroup V
inst_13 : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X : Type w
inst_2 : AddCommGroup X
inst_3 : Module k X
ρ : Representation k G X
⊢ (↑(of ρ) : Type w) = X

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X : Type w
inst_2 : AddCommGroup X
inst_3 : Module k X
ρ : Representation k G X
⊢ (↑(of ρ) : Type w) = X

Tactic:
with_reducible rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X : Type w
inst_2 : AddCommGroup X
inst_3 : Module k X
ρ : Representation k G X
⊢ (of ρ).ρ = ρ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X : Type w
inst_2 : AddCommGroup X
inst_3 : Module k X
ρ : Representation k G X
⊢ (of ρ).ρ = ρ

Tactic:
with_reducible rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
⊢ Hom.hom (𝟙 A) = Representation.IntertwiningMap.id A.ρ

Tactic:
rfl

Premises used: Representation.IntertwiningMap.id, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
a : (↑A : Type w)
⊢ (@ConcreteCategory.hom _ instCategory (fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) V
          (fun (X Y : Rep.{w, u, v} k G) ↦ Representation.IntertwiningMap.instFunLike X.ρ Y.ρ) _ _ _ (𝟙 A : A ⟶ A) :
        (a : (↑A : Type w)) → (↑A : Type w))
      a =
    a

Tactic:
simp [Representation.IntertwiningMap.id]

Premises used: Representation.IntertwiningMap.id
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g : B ⟶ C
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: Representation.IntertwiningMap.comp, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B C : Rep.{w, u, v} k G
f : A ⟶ B
g : B ⟶ C
a : (↑A : Type w)
⊢ Eq (α := (↑C : Type w))
    ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (f ≫ g) :
          (a : (↑A : Type w)) → (↑C : Type w))
        a :
      (↑C : Type w))
    ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) g :
          (a : (↑B : Type w)) → (↑C : Type w))
        ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) f :
              (a : (↑A : Type w)) → (↑B : Type w))
            a :
          (↑B : Type w)) :
      (↑C : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f g : A ⟶ B
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: Rep.Hom.ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
g : G
a : (↑A : Type w)
⊢ Eq (α := (↑B : Type w))
    ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w))
        ((((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (↑A : Type w) →ₗ[k] (↑A : Type w)) :
              (a : (↑A : Type w)) → (↑A : Type w))
            a :
          (↑A : Type w)) :
      (↑B : Type w))
    ((((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g : (↑B : Type w) →ₗ[k] (↑B : Type w)) :
          (a : (↑B : Type w)) → (↑B : Type w))
        ((Hom.hom f : (a : (↑A : Type w)) → (↑B : Type w)) a : (↑B : Type w)) :
      (↑B : Type w))

Tactic:
simpa using congr($(f.hom.2 g) a)
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f : ρ.IntertwiningMap σ
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
Y : Type w
inst_2 : AddCommGroup Y
inst_3 : Module k Y
σ : Representation k G Y
⊢ ofHom (Representation.IntertwiningMap.id σ) = 𝟙 (of σ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
Z : Type w
inst_6 : AddCommGroup Z
inst_7 : Module k Z
τ : Representation k G Z
f : ρ.IntertwiningMap σ
g : σ.IntertwiningMap τ
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
X Y : Type w
inst_2 : AddCommGroup X
inst_3 : AddCommGroup Y
inst_4 : Module k X
inst_5 : Module k Y
ρ : Representation k G X
σ : Representation k G Y
f : ρ.IntertwiningMap σ
x : X
⊢ Eq (α := (↑(of σ) : Type w))
    ((ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ofHom f) :
          (a : (↑(of ρ) : Type w)) → (↑(of σ) : Type w))
        x :
      (↑(of σ) : Type w))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
e : A ≅ B
x : (↑A : Type w)
⊢ (Hom.hom e.inv : (a : (↑B : Type w)) → (↑A : Type w))
      ((Hom.hom e.hom : (a : (↑A : Type w)) → (↑B : Type w)) x : (↑B : Type w)) =
    x

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
e : A ≅ B
x : (↑B : Type w)
⊢ (Hom.hom e.hom : (a : (↑A : Type w)) → (↑B : Type w))
      ((Hom.hom e.inv : (a : (↑B : Type w)) → (↑A : Type w)) x : (↑A : Type w)) =
    x

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A : Rep.{w, u, v} k G
⊢ Functor.obj (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) A =
    (↑A : Type w)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : Semiring k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
f : A ⟶ B
⊢ Eq (α :=
    (a :
        (fun (X : Type w) ↦ X)
          (Functor.obj
            (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) A)) →
      (fun (X : Type w) ↦ X)
        (Functor.obj
          (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (Rep.{w, u, v} k G) (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V)) f)) :
      (a : (fun (X : Type w) ↦ X) ((forget (Rep k G)).obj A)) → (fun (X : Type w) ↦ X) ((forget (Rep k G)).obj B))
    (⇑(ConcreteCategory.hom (FC := fun (A B : Rep.{w, u, v} k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) f) :
      (a : (↑A : Type w)) → (↑B : Type w))

Tactic:
rfl

Premises used: rfl