awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x x_1 : σ.IntertwiningMap τ
x_2 : ρ.IntertwiningMap σ
x_3 : V
⊢ Eq.{u_5 + 1} (α := U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            (({
                  toFun := fun (g : ρ.IntertwiningMap σ) ↦
                    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x + x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
                  map_add' := ⋯, map_smul' := ⋯ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            ((HAdd.hAdd (α := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x.toLinearMap ∘ₗ g.toLinearMap) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)

Tactic:
simp [toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x : A
x_1 : σ.IntertwiningMap τ
h :
  ∀ (x_2 : ρ.IntertwiningMap σ) (x_3 : V),
    Eq.{u_5 + 1} (α := U)
      ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
              (({
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x • x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ } :
                  (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
                x_2) :
            (a : V) → U)
          x_3 :
        U)
      ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
              ((HSMul.hSMul (α := A) (β := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
                    ((RingHom.id A : (a : A) → A) x : A)
                    {
                      toFun := fun (g : ρ.IntertwiningMap σ) ↦
                        LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
                      map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ } :
                  (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
                x_2) :
            (a : V) → U)
          x_3 :
        U)
⊢ {
      toFun := fun (g : ρ.IntertwiningMap σ) ↦
        LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x • x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ) ((RingHom.id A : (a : A) → A) x : A)
      {
        toFun := fun (g : ρ.IntertwiningMap σ) ↦
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ }

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x : A
x_1 : σ.IntertwiningMap τ
x_2 : ρ.IntertwiningMap σ
x_3 : V
⊢ Eq.{u_5 + 1} (α := U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            (({
                  toFun := fun (g : ρ.IntertwiningMap σ) ↦
                    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x • x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
                  map_add' := ⋯, map_smul' := ⋯ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)
    ((toLinearMap.{u_1, u_2, u_3, u_5} (G := G) (ρ := ρ) (σ := τ)
            ((HSMul.hSMul (α := A) (β := ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ)
                  ((RingHom.id A : (a : A) → A) x : A)
                  {
                    toFun := fun (g : ρ.IntertwiningMap σ) ↦
                      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x_1.toLinearMap ∘ₗ g.toLinearMap) ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ } :
                (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
              x_2) :
          (a : V) → U)
        x_3 :
      U)

Tactic:
simp [toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ f.comp g =
    (((llcomp ρ σ τ : (a : σ.IntertwiningMap τ) → ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ) f :
          ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ) :
        (a : ρ.IntertwiningMap σ) → ρ.IntertwiningMap τ)
      g

Tactic:
rfl

Premises used: Representation.IntertwiningMap.comp, LinearMap.intertwiningMap_of_isIntertwiningMap, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
a : A
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ (a • f).comp g = a • f.comp g

Tactic:
simp [comp_def]

Premises used: Representation.IntertwiningMap.comp_def
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
a : A
f : σ.IntertwiningMap τ
g : ρ.IntertwiningMap σ
⊢ f.comp (a • g) = a • f.comp g

Tactic:
simp [comp_def]

Premises used: Representation.IntertwiningMap.comp_def
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
f g : ρ.IntertwiningMap ρ
⊢ (f * g).toLinearMap = f.toLinearMap * g.toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
f g : ρ.IntertwiningMap ρ
v : V
⊢ Eq (α := V) ((f * g : (a : V) → V) v : V) ((f : (a : V) → V) ((g : (a : V) → V) v : V) : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
⊢ Eq.{u_3 + 1} (α := (a : V) → V) (⇑1 : (a : V) → V) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
    HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
ih :
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ (n + 1)) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) (n + 1)

Tactic:
simp only [pow_succ, coe_mul, show f ^ (n + 1) = f ^ n * f from rfl, ih]

Premises used: Representation.IntertwiningMap.coe_mul, pow_succ, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
zero :
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
    HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0
succ :
  ∀ (n : ℕ)
    (ih :
      (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
        HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n),
    (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ (n + 1)) =
      HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) (n + 1)
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n

Tactic:
induction n with
      | zero => rfl
      | succ n ih => simp only [pow_succ, coe_mul, show f ^ (n + 1) = f ^ n * f from rfl, ih]

Premises used: Representation.IntertwiningMap.coe_mul, pow_succ, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
ih :
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ (n + 1)) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) (n + 1)

Tactic:
simp [ih, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f : ρ.IntertwiningMap ρ
n : ℕ
zero :
  (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (HPow.hPow (β := ℕ) f 0) =
    HPow.hPow (α := V →ₗ[A] V) (β := ℕ) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) 0
succ :
  ∀ (n : ℕ)
    (ih :
      (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
        HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n),
    (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ (n + 1)) =
      HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) (n + 1)
⊢ (fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) (f ^ n) =
    HPow.hPow (α := V →ₗ[A] V) ((fun (f : ρ.IntertwiningMap ρ) ↦ f.toLinearMap) f) n

Tactic:
induction n with
      | zero => rfl
      | succ n ih => simp [ih, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
a : A
f g : ρ.IntertwiningMap ρ
h :
  ∀ (x : V),
    Eq (α := V) (((f * a • g).toLinearMap : (a : V) → V) x : V) (((a • (f * g)).toLinearMap : (a : V) → V) x : V)
⊢ f * a • g = a • (f * g)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
a : A
f g : ρ.IntertwiningMap ρ
x : V
⊢ Eq (α := V) (((f * a • g).toLinearMap : (a : V) → V) x : V) (((a • (f * g)).toLinearMap : (a : V) → V) x : V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
a : A
⊢ (algebraMap A (ρ.IntertwiningMap ρ) : (a : A) → ρ.IntertwiningMap ρ) a = HSMul.hSMul (β := ρ.IntertwiningMap ρ) a 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
⊢ Eq (α := Module.End A[G] ρ.asModule)
    ((equivLinearMapAsModule ρ ρ : (a : ρ.IntertwiningMap ρ) → Module.End A[G] ρ.asModule) 1 :
      Module.End A[G] ρ.asModule)
    (1 : Module.End A[G] ρ.asModule)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f_1 : V →ₗ[A] W
f g : ρ.IntertwiningMap ρ
⊢ (equivLinearMapAsModule ρ ρ : (a : ρ.IntertwiningMap ρ) → Module.End A[G] ρ.asModule) (f * g) =
    HMul.hMul (α := Module.End A[G] ρ.asModule) (β := Module.End A[G] ρ.asModule)
      ((equivLinearMapAsModule ρ ρ : (a : ρ.IntertwiningMap ρ) → Module.End A[G] ρ.asModule) f :
        Module.End A[G] ρ.asModule)
      ((equivLinearMapAsModule ρ ρ : (a : ρ.IntertwiningMap ρ) → Module.End A[G] ρ.asModule) g :
        Module.End A[G] ρ.asModule)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : Membership.mem (γ := Submonoid G) (Submonoid.center G) g
rw :
  ∀ (g_1 : G) (v : V),
    Eq (α := V)
      ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[A] V) g_1 : V →ₗ[A] V) : (a : V) → V) v : V) :
        V)
      ((((ρ : (a : G) → V →ₗ[A] V) g_1 : V →ₗ[A] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
        V)
⊢ ρ.IsIntertwiningMap ρ ((ρ : (a : G) → V →ₗ[A] V) g)

Tactic:
rw [isIntertwiningMap_iff]

Premises used: Representation.isIntertwiningMap_iff
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : Membership.mem (γ := Submonoid G) (Submonoid.center G) g
g' : G
v : V
rw :
  ∀ (hg : ∀ (g_1 : G), g_1 * g = g * g_1) (g' : G) (v : V),
    Eq (α := V)
      ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
        V)
      ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
          ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
        V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)

Tactic:
rw [Submonoid.mem_center_iff] at hg

Premises used: Submonoid.mem_center_iff
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module A V
ρ : Representation A G V
g : G
hg : ∀ (g_1 : G), g_1 * g = g * g_1
g' : G
v : V
rw :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
rw₁ :
  Eq (α := V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₂ :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g * g') : V →ₗ[A] V) : (a : V) → V) v : V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₃ :
  Eq (α := V) ((((ρ : (a : G) → V →ₗ[A] V) (g' * g) : V →ₗ[A] V) : (a : V) → V) v : V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
rw₄ rw₅ :
  Eq (α := V)
    ((HMul.hMul (α := V →ₗ[A] V) (β := V →ₗ[A] V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
    ((HMul.hMul (α := Module.End A V) (β := Module.End A V) ((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V)
            ((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) :
          (a : V) → V)
        v :
      V)
⊢ Eq (α := V)
    ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)
    ((((ρ : (a : G) → V →ₗ[A] V) g' : V →ₗ[A] V) : (a : V) → V)
        ((((ρ : (a : G) → V →ₗ[A] V) g : V →ₗ[A] V) : (a : V) → V) v : V) :
      V)

Tactic:
rw [← Module.End.mul_apply, ← Module.End.mul_apply, ← ρ.map_mul, ← hg g', ρ.map_mul]

Premises used: Module.End.mul_apply, MonoidHom.map_mul
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A_1 : Type u_1
G_1 : Type u_2
V_1 : Type u_3
W_1 : Type u_4
U : Type u_5
inst : CommSemiring A_1
inst_1 : Monoid G_1
inst_2 : AddCommMonoid V_1
inst_3 : AddCommMonoid W_1
inst_4 : AddCommMonoid U
inst_5 : Module A_1 V_1
inst_6 : Module A_1 W_1
inst_7 : Module A_1 U
ρ_1 : Representation A_1 G_1 V_1
σ_1 : Representation A_1 G_1 W_1
τ : Representation A_1 G_1 U
f : V_1 →ₗ[A_1] W_1
A : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst_8 : CommRing A
inst_9 : Monoid G
inst_10 : AddCommGroup V
inst_11 : AddCommGroup W
inst_12 : Module A V
inst_13 : Module A W
ρ : Representation A G V
σ : Representation A G W
inst_14 : Module.Finite A V
inst_15 : IsNoetherian A W
⊢ Module.Finite A (ρ.IntertwiningMap σ)

Tactic:
.of_injective (toLinearMapl (ρ := ρ) (σ := σ)) (toLinearMap_injective ρ σ)

Premises used: Representation.IntertwiningMap.toLinearMap_injective, Module.Finite.of_injective, Representation.IntertwiningMap.toLinearMapl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
f : ρ.IntertwiningMap σ
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ Eq (α := (a : V) → W) (⇑(f.ofBijective hf) : (a : V) → W) (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl