awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : ModuleCat k[G]} (f : X ⟶ Y),
    Eq (α := Functor.obj (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) X ⟶ Functor.obj (𝟭 (ModuleCat k[G])) Y)
      (CategoryTheory.Functor.map (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) f ≫
        Iso.hom ((fun (M : ModuleCat k[G]) ↦ counitIso M) Y))
      (Iso.hom ((fun (M : ModuleCat k[G]) ↦ counitIso M) X) ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat k[G])) f)
⊢ ∀ {X Y : ModuleCat k[G]} (f : X ⟶ Y),
    Eq (α := Functor.obj (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) X ⟶ Functor.obj (𝟭 (ModuleCat k[G])) Y)
      (CategoryTheory.Functor.map (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) f ≫
        Iso.hom ((fun (M : ModuleCat k[G]) ↦ counitIso M) Y))
      (Iso.hom ((fun (M : ModuleCat k[G]) ↦ counitIso M) X) ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat k[G])) f)

Tactic:
cat_disch
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Functor.IsEquivalence (C := Rep.{w, u, v} k G) toModuleMonoidAlgebra

Tactic:
(equivalenceModuleMonoidAlgebra (k := k) (G := G)).isEquivalence_functor

Premises used: Rep.equivalenceModuleMonoidAlgebra, Rep.toModuleMonoidAlgebra, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Functor.IsEquivalence (C := ModuleCat k[G]) ofModuleMonoidAlgebra

Tactic:
(equivalenceModuleMonoidAlgebra (k := k) (G := G)).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, Rep.ofModuleMonoidAlgebra, Rep.equivalenceModuleMonoidAlgebra
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ ∀ (g : G),
    Eq.{w + 1} (α := (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑A : Type w))
      (LinearMap.fst k (↑A : Type w) (↑B : Type w) ∘ₗ
        (A.ρ.prod B.ρ : (a : G) → (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w)) g)
      ((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ LinearMap.fst k (↑A : Type w) (↑B : Type w))

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ ∀ (g : G),
    Eq.{w + 1} (α := (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑B : Type w))
      (LinearMap.snd k (↑A : Type w) (↑B : Type w) ∘ₗ
        (A.ρ.prod B.ρ : (a : G) → (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w)) g)
      ((B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g ∘ₗ LinearMap.snd k (↑A : Type w) (↑B : Type w))

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ ∀ (g : G),
    Eq.{w + 1} (α := (↑A : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w))
      (LinearMap.inl k (↑A : Type w) (↑B : Type w) ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g)
      ((A.ρ.prod B.ρ : (a : G) → (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w)) g ∘ₗ
        LinearMap.inl k (↑A : Type w) (↑B : Type w))

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ ∀ (g : G),
    Eq.{w + 1} (α := (↑B : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w))
      (LinearMap.inr k (↑A : Type w) (↑B : Type w) ∘ₗ (B.ρ : (a : G) → (↑B : Type w) →ₗ[k] (↑B : Type w)) g)
      ((A.ρ.prod B.ρ : (a : G) → (↑A : Type w) × (↑B : Type w) →ₗ[k] (↑A : Type w) × (↑B : Type w)) g ∘ₗ
        LinearMap.inr k (↑A : Type w) (↑B : Type w))

Tactic:
simp [LinearMap.ext_iff]

Premises used: LinearMap.ext_iff
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
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' := ⋯ :
              A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))) =
    (Hom.hom (𝟙 A)).toLinearMap
⊢ 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

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
          (ofHom
            { toLinearMap := LinearMap.inl k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))) =
    (Hom.hom (𝟙 A)).toLinearMap

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
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' := ⋯ :
              A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))
⊢ 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

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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 : 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' := ⋯ :
              A.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))

Tactic:
simp [zero_hom]

Premises used: Rep.zero_hom
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
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' := ⋯ :
              B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))
⊢ 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

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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 : 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' := ⋯ :
              B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.fst k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap A.ρ }))))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom 0))

Tactic:
simp [zero_hom]

Premises used: Rep.zero_hom
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
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' := ⋯ :
              B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))) =
    (Hom.hom (𝟙 B)).toLinearMap
⊢ 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

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A B : Rep.{w, u, v} k G
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom
        (CategoryStruct.comp (Y := of (A.ρ.prod B.ρ))
          (ofHom
            { toLinearMap := LinearMap.inr k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              B.ρ.IntertwiningMap (A.ρ.prod B.ρ) })
          (ofHom
            { toLinearMap := LinearMap.snd k (↑A : Type w) (↑B : Type w), isIntertwining' := ⋯ :
              (A.ρ.prod B.ρ).IntertwiningMap B.ρ }))) =
    (Hom.hom (𝟙 B)).toLinearMap

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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
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))
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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)
⊢ x = 0

Tactic:
have : x = 0 := Subsingleton.elim _ _
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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
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))
⊢ 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:
subst this
-- Module: Mathlib.RepresentationTheory.Rep.Iso
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
⊢ 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:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X : Rep.{w, u, v} k G
f : X ⟶ trivial k G PUnit.{w + 1}
⊢ f = default

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Limits.HasFiniteProducts (Rep.{w, u, v} k G)

Tactic:
hasFiniteProducts_of_has_binary_and_terminal

Premises used: CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
k G : Type u
inst_2 : CommRing k
inst_3 : Monoid G
⊢ EnoughProjectives (Rep k G)

Tactic:
equivalenceModuleMonoidAlgebra.enoughProjectives_iff.2 ModuleCat.enoughProjectives.{max w u}

Premises used: Iff.mpr, ModuleCat.enoughProjectives, Rep.equivalenceModuleMonoidAlgebra, CategoryTheory.Equivalence.enoughProjectives_iff
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
α : Type (max w u)
⊢ Projective (C := Rep k G) (free k G α)

Tactic:
equivalenceModuleMonoidAlgebra.toAdjunction.projective_of_map_projective _ <|
    @ModuleCat.projective_of_free _ _
      (ModuleCat.of k[G] (Representation.free k G α).asModule)
      _ (Representation.freeAsModuleBasis k G α)

Premises used: ModuleCat.projective_of_free, Rep.equivalenceModuleMonoidAlgebra, CategoryTheory.Adjunction.projective_of_map_projective, CategoryTheory.Equivalence.toAdjunction, Representation.freeAsModuleBasis
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (diagonal k G (n + 1))

Tactic:
Projective.of_iso (diagonalSuccIsoFree k G n).symm inferInstance

Premises used: inferInstance, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, Rep.diagonalSuccIsoFree
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (diagonal k G (n + 1))

Tactic:
exact Projective.of_iso (diagonalSuccIsoFree k G n).symm inferInstance

Premises used: inferInstance, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, Rep.diagonalSuccIsoFree
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (diagonal k G (n + 1))

Tactic:
classical
  exact Projective.of_iso (diagonalSuccIsoFree k G n).symm inferInstance

Premises used: inferInstance, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, Rep.diagonalSuccIsoFree
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
⊢ Projective (C := Rep k G) (leftRegular k G)

Tactic:
Projective.of_iso (diagonalOneIsoLeftRegular k G) inferInstance

Premises used: inferInstance, Rep.diagonalOneIsoLeftRegular, CategoryTheory.Projective.of_iso
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type u
inst_2 : Group G
n : ℕ
inst_3 : Subsingleton G
⊢ Projective (C := Rep k G) (trivial k G k)

Tactic:
Projective.of_iso (ofMulActionSubsingletonIsoTrivial _ _ (Fin 1 → G)) diagonal_succ_projective

Premises used: Rep.diagonal_succ_projective, Rep.ofMulActionSubsingletonIsoTrivial, CategoryTheory.Projective.of_iso
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
X Y : Rep.{t, u, v1} k G
f' : X ⟶ Y
h : H
⊢ Eq (α := (↑X : Type t) →ₗ[k] (↑Y : Type t))
    ((↑(Hom.hom f') :
        [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type t) (↑Y : Type t)] →
          [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type t) (↑Y : Type t)] →
            (↑X : Type t) →ₗ[k] (↑Y : Type t)) ∘ₗ
      (MonoidHom.comp X.ρ f : (a : H) → (↑X : Type t) →ₗ[k] (↑X : Type t)) h)
    ((MonoidHom.comp Y.ρ f : (a : H) → (↑Y : Type t) →ₗ[k] (↑Y : Type t)) h ∘ₗ
      (↑(Hom.hom f') :
        [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type t) (↑Y : Type t)] →
          [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type t) (↑Y : Type t)] →
            (↑X : Type t) →ₗ[k] (↑Y : Type t)))

Tactic:
simpa using f'.hom.2 (f h)

Premises used: Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Rep.Res
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.{u_1, u, v1} k G
⊢ (res f M).ρ = MonoidHom.comp M.ρ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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.{u_1, u, v1} k G
h : H
⊢ Eq.{u_1 + 1} (α := (↑(res f M) : Type u_1) →ₗ[k] (↑(res f M) : Type u_1))
    (((res f M).ρ : (a : H) → (↑(res f M) : Type u_1) →ₗ[k] (↑(res f M) : Type u_1)) h :
      (↑(res f M) : Type u_1) →ₗ[k] (↑(res f M) : Type u_1))
    ((M.ρ : (a : G) → (↑M : Type u_1) →ₗ[k] (↑M : Type u_1)) ((f : (a : H) → G) h) :
      (↑M : Type u_1) →ₗ[k] (↑M : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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.{u_1, u, v1} k G
⊢ (↑(res f M) : Type u_1) = (↑M : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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 N : Rep.{u_1, u, v1} k G
p : M ⟶ N
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) p)) =
    (Hom.hom p).toLinearMap

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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₂)
hf : (Hom.hom a₁).toLinearMap = (Hom.hom a₂).toLinearMap
⊢ a₁ = a₂

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Res
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₂)
⊢ 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

Premises used: Representation.IntertwiningMap.ext_iff, Rep.hom_ext_iff
-- Module: Mathlib.RepresentationTheory.Rep.Res
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) : 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₂)))
⊢ (Hom.hom a₁).toLinearMap = (Hom.hom a₂).toLinearMap

Tactic:
simpa using h
-- Module: Mathlib.RepresentationTheory.Rep.Res
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
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
⊢ (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

Tactic:
obtain ⟨h, rfl⟩ := hf g

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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
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:
simpa using f'.hom.2 h

Premises used: Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom
-- Module: Mathlib.RepresentationTheory.Rep.Res
Goal:
k : Type u
inst : Semiring k
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* 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
⊢ (Hom.hom (liftHomOfSurj f hf f')).toLinearMap = (Hom.hom f').toLinearMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Res
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₁ :
  Representation.IntertwiningMap.toLinearMap
      (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f'))) =
    (Hom.hom f').toLinearMap
⊢ CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f') = f'

Tactic:
ext : 2
-- Module: Mathlib.RepresentationTheory.Rep.Res
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
hf₂ hf₃ : (Hom.hom f').toLinearMap = (Hom.hom f').toLinearMap
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (liftHomOfSurj f hf f'))) =
    (Hom.hom f').toLinearMap

Tactic:
rw [res_map_hom_toLinearMap, liftHomOfSurj_toLinearMap]

Premises used: Rep.liftHomOfSurj_toLinearMap, Rep.res_map_hom_toLinearMap