awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
      (ofHom { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ })
      (ofHom { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ }) =
    𝟙 A
have hf : Representation.IntertwiningMap.toLinearMap
    (Hom.hom
      (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
        (ofHom
          { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
        (ofHom
          { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))) =
  (Hom.hom (𝟙 A)).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Eq.{w + 1} (α := A ⟶ B)
    (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
      (ofHom { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ })
      (ofHom { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ }))
    0
have hf : Eq.{w + 1} (α := (↑A : Type w) →ₗ[k] (↑B : Type w))
  (Representation.IntertwiningMap.toLinearMap
    (Hom.hom
      (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
        (ofHom
          { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
        (ofHom
          { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))))
  (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Eq.{w + 1} (α := B ⟶ A)
    (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
      (ofHom { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ })
      (ofHom { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ }))
    0
have hf : Eq.{w + 1} (α := (↑B : Type w) →ₗ[k] (↑A : Type w))
  (Representation.IntertwiningMap.toLinearMap
    (Hom.hom
      (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
        (ofHom
          { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
        (ofHom
          { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))))
  (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
      (ofHom { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ })
      (ofHom { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ }) =
    𝟙 B
have hf : Representation.IntertwiningMap.toLinearMap
    (Hom.hom
      (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
        (ofHom
          { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
        (ofHom
          { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := sorry :
            (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))) =
  (Hom.hom (𝟙 B)).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ f = default
have hf : ∀ (x : (↑(trivial k G PUnit.{w + 1}) : Type w)),
  Eq (α := (↑X : Type w))
    (((Hom.hom f).toLinearMap : (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w)) x : (↑X : Type w))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom default) :
          (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w))
        x :
      (↑X : Type w))
Tactic: ext x
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (hypothesis)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : (↑(trivial k G PUnit.{w + 1}) : Type w)
⊢ Eq (α := (↑X : Type w))
    (((Hom.hom f).toLinearMap : (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w)) x : (↑X : Type w))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom default) :
          (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w))
        x :
      (↑X : Type w))
have this : x = 0
Tactic: have : x = 0 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
f : trivial k G PUnit.{w + 1} ⟶ X
x : (↑(trivial k G PUnit.{w + 1}) : Type w)
this : x = 0
⊢ Eq (α := (↑X : Type w))
    (((Hom.hom f).toLinearMap : (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w)) x : (↑X : Type w))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom default) :
          (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w))
        x :
      (↑X : Type w))
have hf : Eq (α := (↑X : Type w))
  (((Hom.hom f).toLinearMap : (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w)) 0 : (↑X : Type w))
  ((Representation.IntertwiningMap.toLinearMap (Hom.hom default) :
        (a : (↑(trivial k G PUnit.{w + 1}) : Type w)) → (↑X : Type w))
      0 :
    (↑X : Type w))
Tactic: subst this
Cleared hypotheses: x, this
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
X Y : Rep.{u_1, u, v1} k G
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) (CategoryTheory.Functor.map (resFunctor f) a₁)
    (CategoryTheory.Functor.map (resFunctor f) a₂)
⊢ a₁ = a₂
have hf : (Hom.hom a₁).toLinearMap = (Hom.hom a₂).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (hypothesis)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
X Y : Rep.{u_1, u, v1} k G
a₁ a₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) (CategoryTheory.Functor.map (resFunctor f) a₁)
    (CategoryTheory.Functor.map (resFunctor f) a₂)
⊢ (Hom.hom a₁).toLinearMap = (Hom.hom a₂).toLinearMap
have h₁ : Eq (α := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1))
  (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) a₁)))
  (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) a₂)))
Tactic: rw [Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
X Y : Rep.{u_1, u, v1} k G
hf : Function.Surjective.{v2 + 1, v1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
f' : res f X ⟶ res f Y
g : G
⊢ (Hom.hom f').toLinearMap ∘ₗ (X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) g =
    (Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) g ∘ₗ (Hom.hom f').toLinearMap
have obtain : ∀ (h : H),
  (Hom.hom f').toLinearMap ∘ₗ (X.ρ : (a : G) → (↑X : Type u_1) →ₗ[k] (↑X : Type u_1)) ((f : (a : H) → G) h) =
    (Y.ρ : (a : G) → (↑Y : Type u_1) →ₗ[k] (↑Y : Type u_1)) ((f : (a : H) → G) h) ∘ₗ (Hom.hom f').toLinearMap
Tactic: obtain ⟨h, rfl⟩ := hf g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
hf : Function.Surjective.{v2 + 1, v1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
X Y : Rep.{u_1, u, v1} k G
f' : Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y
⊢ CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f') = f'
have hf₁ : Representation.IntertwiningMap.toLinearMap
    (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f'))) =
  (Hom.hom f').toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
hf : Function.Surjective.{v2 + 1, v1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
X Y : Rep.{u_1, u, v1} k G
f' : Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f'))) =
    (Hom.hom f').toLinearMap
have hf₁ : (Hom.hom (liftHomOfSurj f hf f')).toLinearMap = (Hom.hom f').toLinearMap
Tactic: rw [res_map_hom_toLinearMap, liftHomOfSurj_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
hf : Function.Surjective.{v2 + 1, v1 + 1} (α := H) (β := G) (⇑f : (a : H) → G)
X Y : Rep.{u_1, u, v1} k G
f' : Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y
hf₁ : (Hom.hom (liftHomOfSurj f hf f')).toLinearMap = (Hom.hom f').toLinearMap
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f'))) =
    (Hom.hom f').toLinearMap
have hf₂ : (Hom.hom f').toLinearMap = (Hom.hom f').toLinearMap
Tactic: rw [res_map_hom_toLinearMap, liftHomOfSurj_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
x x_1 : Rep.{u_1, u, v1} k G
x_2 x_3 : x ⟶ x_1
⊢ CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3) =
    HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
      (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3)
have hf : Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3))) =
  (Hom.hom
      (HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
        (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3))).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k G
x x_1 : Rep.{u_1, u, v1} k G
x_2 x_3 : x ⟶ x_1
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (x_2 + x_3))) =
    (Hom.hom
        (HAdd.hAdd (α := Functor.obj (resFunctor f) x ⟶ Functor.obj (resFunctor f) x_1)
          (CategoryTheory.Functor.map (resFunctor f) x_2) (CategoryTheory.Functor.map (resFunctor f) x_3))).toLinearMap
have hf : Representation.IntertwiningMap.toLinearMap
    (Hom.hom
      (ofHom
        {
          toLinearMap :=
            (↑(Hom.hom x_2 + Hom.hom x_3) :
              [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                  (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
          isIntertwining' := sorry : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })) =
  HAdd.hAdd (α := (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1))
    (Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom x_2) :
                [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                  [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
            isIntertwining' := sorry : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))
    (Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (ofHom
          {
            toLinearMap :=
              (↑(Hom.hom x_3) :
                [inst_3 : FunLike (x.ρ.IntertwiningMap x_1.ρ) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                  [SemilinearMapClass (x.ρ.IntertwiningMap x_1.ρ) (RingHom.id k) (↑x : Type u_1) (↑x_1 : Type u_1)] →
                    (↑x : Type u_1) →ₗ[k] (↑x_1 : Type u_1)),
            isIntertwining' := sorry : Representation.IntertwiningMap (MonoidHom.comp x.ρ f) (MonoidHom.comp x_1.ρ f) })))
Tactic: simp only [add_hom, Representation.IntertwiningMap.add_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
⊢ CategoryTheory.Functor.map (resFunctor f) (r • l) =
    HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
      (CategoryTheory.Functor.map (resFunctor f) l)
have hf : Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
  (Hom.hom
      (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
        (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf : Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
  (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
      (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf₁ : Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
  HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
hf₁ :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf₂ : (Hom.hom (r • l)).toLinearMap =
  HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
hf₁ :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₂ :
  (Hom.hom (r • l)).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf₃ : (r • Hom.hom l).toLinearMap =
  HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
hf₁ :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₂ :
  (Hom.hom (r • l)).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₃ :
  (r • Hom.hom l).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf₄ : r • (Hom.hom l).toLinearMap =
  HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]