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
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
a : A
f : ρ.IntertwiningMap σ
⊢ (⇑(a • f) : (a : V) → W) = HSMul.hSMul (β := (a : V) → W) a (⇑f : (a : V) → W)

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
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
a : A
f : ρ.IntertwiningMap σ
⊢ (a • f).toLinearMap = a • f.toLinearMap

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
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
a : A
f : ρ.IntertwiningMap σ
v : V
⊢ (a • f : (a : V) → W) v = HSMul.hSMul (β := W) a ((f : (a : V) → W) v : W)

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 σ
v : ρ.asModule
⊢ (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) 0 v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) 0)
      ((f.toLinearMap : (a : V) → W) v : W)

Tactic:
simp [f.toLinearMap.map_zero]

Premises used: LinearMap.map_zero, Representation.IntertwiningMap.toLinearMap
-- 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 σ
v : ρ.asModule
x y : A[G]
hx :
  (f.toLinearMap : (a : V) → W) (x • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) x : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
hy :
  (f.toLinearMap : (a : V) → W) (y • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) y : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)
⊢ (f.toLinearMap : (a : V) → W) ((x + y) • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (x + y) : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)

Tactic:
simp [add_smul, map_add, hx, hy]

Premises used: map_add, add_smul
-- 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 σ
v : ρ.asModule
g : G
a : A
single :
  HSMul.hSMul (β := W) a
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
          ((f : (a : V) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) v : V) : W) :
        W) =
    HSMul.hSMul (β := W) a
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
          ((σ.asModuleEquiv : (a : σ.asModule) → W) ((f : (a : V) → W) v : W) : W) :
        W)
⊢ (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (MonoidAlgebra.single g a) : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)

Tactic:
simp [f.isIntertwining]

Premises used: Representation.IntertwiningMap.isIntertwining
-- 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 σ
v : ρ.asModule
g : G
a : A
⊢ HSMul.hSMul (β := W) a
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
          ((f : (a : V) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → V) v : V) : W) :
        W) =
    HSMul.hSMul (β := W) a
      ((((σ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W)
          ((σ.asModuleEquiv : (a : σ.asModule) → W) ((f : (a : V) → W) v : W) : W) :
        W)

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 σ
m : A[G]
v : ρ.asModule
zero :
  (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) 0 v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) 0)
      ((f.toLinearMap : (a : V) → W) v : W)
add :
  ∀ (x y : A[G])
    (hx :
      (f.toLinearMap : (a : V) → W) (x • v) =
        HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) x : A[G])
          ((f.toLinearMap : (a : V) → W) v : W))
    (hy :
      (f.toLinearMap : (a : V) → W) (y • v) =
        HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) y : A[G])
          ((f.toLinearMap : (a : V) → W) v : W)),
    (f.toLinearMap : (a : V) → W) ((x + y) • v) =
      HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) (x + y) : A[G])
        ((f.toLinearMap : (a : V) → W) v : W)
single :
  ∀ (g : G) (a : A),
    (f.toLinearMap : (a : V) → W) (HSMul.hSMul (α := A[G]) (MonoidAlgebra.single g a) v) =
      HSMul.hSMul (α := A[G]) (β := σ.asModule)
        ((RingHom.id A[G] : (a : A[G]) → A[G]) (MonoidAlgebra.single g a) : A[G]) ((f.toLinearMap : (a : V) → W) v : W)
⊢ (f.toLinearMap : (a : V) → W) (m • v) =
    HSMul.hSMul (α := A[G]) (β := σ.asModule) ((RingHom.id A[G] : (a : A[G]) → A[G]) m : A[G])
      ((f.toLinearMap : (a : V) → W) v : W)

Tactic:
induction m using MonoidAlgebra.induction_linear with
          | zero => simp [f.toLinearMap.map_zero]
          | add x y hx hy => simp [add_smul, map_add, hx, hy]
          | single g a => simp [f.isIntertwining]; rfl

Premises used: LinearMap.map_zero, map_add, add_smul, Representation.IntertwiningMap.isIntertwining, Representation.IntertwiningMap.toLinearMap
-- 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
g₁ g₂ : ρ.IntertwiningMap σ
h :
  ∀ (x : ρ.asModule),
    Eq.{u_4 + 1} (α := σ.asModule)
      ((({ toFun := (⇑(g₁ + g₂).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
            (a : ρ.asModule) → σ.asModule)
          x :
        σ.asModule)
      ((HAdd.hAdd (α := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
              { toFun := (⇑g₁.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
                LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
              { toFun := (⇑g₂.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
                LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
            (a : ρ.asModule) → σ.asModule)
          x :
        σ.asModule)
⊢ { toFun := (⇑(g₁ + g₂).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
      { toFun := (⇑g₁.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
      { toFun := (⇑g₂.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }

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
g₁ g₂ : ρ.IntertwiningMap σ
x : ρ.asModule
⊢ Eq.{u_4 + 1} (α := σ.asModule)
    ((({ toFun := (⇑(g₁ + g₂).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } :
            LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
    ((HAdd.hAdd (α := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
            { toFun := (⇑g₁.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }
            { toFun := (⇑g₂.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)

Tactic:
simp
-- 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
t : A
g : ρ.IntertwiningMap σ
h :
  ∀ (x : ρ.asModule),
    Eq.{u_4 + 1} (α := σ.asModule)
      ((({ toFun := (⇑(t • g).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
            (a : ρ.asModule) → σ.asModule)
          x :
        σ.asModule)
      ((HSMul.hSMul (α := A) (β := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
              ((RingHom.id A : (a : A) → A) t : A)
              { toFun := (⇑g.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
                LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
            (a : ρ.asModule) → σ.asModule)
          x :
        σ.asModule)
⊢ { toFun := (⇑(t • g).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := A) (β := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
      ((RingHom.id A : (a : A) → A) t : A)
      { toFun := (⇑g.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
        LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule }

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
t : A
g : ρ.IntertwiningMap σ
x : ρ.asModule
⊢ Eq.{u_4 + 1} (α := σ.asModule)
    ((({ toFun := (⇑(t • g).toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ } :
            LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule) :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)
    ((HSMul.hSMul (α := A) (β := LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule)
            ((RingHom.id A : (a : A) → A) t : A)
            { toFun := (⇑g.toLinearMap : (a : V) → W), map_add' := ⋯, map_smul' := ⋯ :
              LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule } :
          (a : ρ.asModule) → σ.asModule)
        x :
      σ.asModule)

Tactic:
simp
-- 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 : LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule
a : A
v : V
⊢ f.toFun (a • v) = HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) a : A) (f.toFun v)

Tactic:
simp
-- 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 : LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule
g : G
h :
  ∀ (v : V),
    Eq.{u_4 + 1} (α := W)
      (({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g : (a : V) → W) v : W)
      (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ } : (a : V) → W) v : W)
⊢ Eq (α := V →ₗ[A] W) ({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g)
    ((σ : (a : G) → W →ₗ[A] W) g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ })

Tactic:
ext v
-- 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 : LinearMap (R := A[G]) (RingHom.id A[G]) ρ.asModule σ.asModule
g : G
v : V
⊢ Eq.{u_4 + 1} (α := W)
    (({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ (ρ : (a : G) → V →ₗ[A] V) g : (a : V) → W) v : W)
    (((σ : (a : G) → W →ₗ[A] W) g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ } : (a : V) → W) v : W)

Tactic:
simpa using f.map_smul' (MonoidAlgebra.single g 1) v

Premises used: LinearMap.map_smul', OfNat.ofNat, MonoidAlgebra.single
-- 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 τ
g : ρ.IntertwiningMap σ
γ : G
v : V
⊢ Eq (α := U)
    ((f.toLinearMap ∘ₗ g.toLinearMap : (a : V) → U) ((((ρ : (a : G) → V →ₗ[A] V) γ : V →ₗ[A] V) : (a : V) → V) v : V) :
      U)
    ((((τ : (a : G) → U →ₗ[A] U) γ : U →ₗ[A] U) : (a : U) → U) ((f.toLinearMap ∘ₗ g.toLinearMap : (a : V) → U) v : U) :
      U)

Tactic:
simp [f.isIntertwining, g.isIntertwining]

Premises used: Representation.IntertwiningMap.isIntertwining
-- 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 τ
x x_1 : ρ.IntertwiningMap σ
h :
  ∀ (x_2 : V),
    Eq.{u_5 + 1} (α := U)
      (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x + x_1).toLinearMap) ⋯).toLinearMap :
            (a : V) → U)
          x_2 :
        U)
      (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x.toLinearMap) ⋯ +
                LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯).toLinearMap :
            (a : V) → U)
          x_2 :
        U)
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x + x_1).toLinearMap) ⋯ =
    LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x.toLinearMap) ⋯ +
      LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯

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
f : σ.IntertwiningMap τ
x x_1 : ρ.IntertwiningMap σ
x_2 : V
⊢ Eq.{u_5 + 1} (α := U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x + x_1).toLinearMap) ⋯).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x.toLinearMap) ⋯ +
              LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯).toLinearMap :
          (a : V) → U)
        x_2 :
      U)

Tactic:
simp [map_add, toLinearMap_apply]

Premises used: map_add, 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_1 : V →ₗ[A] W
f : σ.IntertwiningMap τ
x : A
x_1 : ρ.IntertwiningMap σ
h :
  ∀ (x_2 : V),
    Eq.{u_5 + 1} (α := U)
      (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x • x_1).toLinearMap) ⋯).toLinearMap :
            (a : V) → U)
          x_2 :
        U)
      (((HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) x : A)
                (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯)).toLinearMap :
            (a : V) → U)
          x_2 :
        U)
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x • x_1).toLinearMap) ⋯ =
    HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) x : A)
      (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯)

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
f : σ.IntertwiningMap τ
x : A
x_1 : ρ.IntertwiningMap σ
x_2 : V
⊢ Eq.{u_5 + 1} (α := U)
    (((LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x • x_1).toLinearMap) ⋯).toLinearMap :
          (a : V) → U)
        x_2 :
      U)
    (((HSMul.hSMul (α := A) ((RingHom.id A : (a : A) → A) x : A)
              (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x_1.toLinearMap) ⋯)).toLinearMap :
          (a : V) → U)
        x_2 :
      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 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) (ρ := ρ) (σ := τ)
              ((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)
⊢ {
      toFun := fun (g : ρ.IntertwiningMap σ) ↦
        LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x + x_1).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    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 τ }

Tactic:
ext