awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
X Y : FDRep R G
f :
  Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      X ⟶
    Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      Y
g : G
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ∘ₗ
      (X.ρ : (a : G) → (↑X.V : Type u) →ₗ[R] (↑X.V : Type u)) g =
    (Y.ρ : (a : G) → (↑Y.V : Type u) →ₗ[R] (↑Y.V : Type u)) g ∘ₗ
      ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)

Tactic:
f.hom.2 g

Premises used: Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
X Y : FDRep R G
f :
  Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      X ⟶
    Functor.obj
      (forget₂ (FDRep R G) (FC :=
        Action.HomSubtype (FGModuleCat R) G (FV :=
          fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.obj (P := ModuleCat.isFG R)) : Type u)) (CV :=
          fun (X : ObjectProperty.FullSubcategory (C := ModuleCat R) (ModuleCat.isFG R)) ↦
          (↑(X.obj (P := ModuleCat.isFG R)) : Type u)))
        (CC := fun (X : Action.{u, u + 1, v} (FGModuleCat R) G) ↦ (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u))
        (Rep R G) (FD := fun (A B : Rep R G) ↦ A.ρ.IntertwiningMap B.ρ) (CD := Rep.V))
      Y
g : G
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ∘ₗ
      (X.ρ : (a : G) → (↑X.V : Type u) →ₗ[R] (↑X.V : Type u)) g =
    (Y.ρ : (a : G) → (↑Y.V : Type u) →ₗ[R] (↑Y.V : Type u)) g ∘ₗ
      ModuleCat.Hom.hom (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)

Tactic:
exact f.hom.2 g

Premises used: Representation.IntertwiningMap.isIntertwining', Rep.Hom.hom
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ Functor.Full (C := FDRep R G) (Functor.mapAction (ObjectProperty.ι (ModuleCat.isFG R)) G ⋙ Rep.ActionToRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
R k : Type u
G : Type v
inst : CommRing R
inst_1 : Field k
inst_2 : Monoid G
⊢ Functor.Faithful (C := FDRep R G) (Functor.mapAction (ObjectProperty.ι (ModuleCat.isFG R)) G ⋙ Rep.ActionToRep R G)

Tactic:
infer_instance
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
refine :
  ∀ (g : G),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)
      (CategoryStruct.comp (Y :=
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
          (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
                (a : G) → End (of ρV.dual ⊗ W).V)
              g :
            End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
          (Iso.hom (dualTensorIsoLinHomAux ρV W) :
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
              (of (ρV.linHom W.ρ)).V) :
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
          (of (ρV.linHom W.ρ)).V)
      (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
          (Iso.hom (dualTensorIsoLinHomAux ρV W) :
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
              (of (ρV.linHom W.ρ)).V)
          (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V) :
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
          (of (ρV.linHom W.ρ)).V)
⊢ MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W ≅ of (ρV.linHom W.ρ)

Tactic:
refine Action.mkIso (dualTensorIsoLinHomAux ρV W) (fun g => ?_)

Premises used: Action.mkIso, FDRep.dualTensorIsoLinHomAux
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
g : G
⊢ Eq (α :=
    (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
            ModuleCat.isFG k)) :
        Type u) →ₗ[k]
      (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
                  (a : G) → End (of ρV.dual ⊗ W).V)
                g :
              End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V)
            (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))

Tactic:
dualTensorHom_comm ρV W.ρ g

Premises used: Quotient, TensorProduct, AddCon.Quotient, Representation.dualTensorHom_comm, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
g : G
⊢ Eq (α :=
    (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
            ModuleCat.isFG k)) :
        Type u) →ₗ[k]
      (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).ρ :
                  (a : G) → End (of ρV.dual ⊗ W).V)
                g :
              End (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))
    (ModuleCat.Hom.hom
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := (of (ρV.linHom W.ρ)).V)
            (Iso.hom (dualTensorIsoLinHomAux ρV W) :
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
                (of (ρV.linHom W.ρ)).V)
            (((of (ρV.linHom W.ρ)).ρ : (a : G) → End (of (ρV.linHom W.ρ)).V) g : End (of (ρV.linHom W.ρ)).V))) :
      (↑((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V.obj (P :=
              ModuleCat.isFG k)) :
          Type u) →ₗ[k]
        (↑((of (ρV.linHom W.ρ)).V.obj (P := ModuleCat.isFG k)) : Type u))

Tactic:
exact dualTensorHom_comm ρV W.ρ g

Premises used: Representation.dualTensorHom_comm, FDRep.ρ
-- Module: Mathlib.RepresentationTheory.FDRep
Goal:
k : Type u
G : Type v
V : Type u
inst : Field k
inst_1 : Group G
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
      (of (ρV.linHom W.ρ)).V)
    (Action.Hom.hom (Iso.hom (dualTensorIsoLinHom ρV W)) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)
    (ConcreteCategory.ofHom (FC := fun (X Y : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
        (↑(X.obj (P := ModuleCat.isFG k)) : Type u) →ₗ[k] (↑(Y.obj (P := ModuleCat.isFG k)) : Type u)) (CC :=
        fun (X : ObjectProperty.FullSubcategory (C := ModuleCat k) (ModuleCat.isFG k)) ↦
        (↑(X.obj (P := ModuleCat.isFG k)) : Type u)) (dualTensorHom k V (↑W.V : Type u)) :
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W).V ⟶
        (of (ρV.linHom W.ρ)).V)

Tactic:
rfl

Premises used: dualTensorHom, rfl
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep.{w, u, u} k G
rw :
  Module.Injective.{u, w} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep.{w, u, u} k G ⥤ ModuleCat.{w, u} (MonoidAlgebra k G)).1
          V) :
      Type w)
⊢ Injective V

Tactic:
rw [← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff,
    ← Module.injective_iff_injective_object]

Premises used: CategoryTheory.Equivalence.map_injective_iff, Rep.equivalenceModuleMonoidAlgebra, Module.injective_iff_injective_object
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep.{w, u, u} k G
⊢ Module.Injective.{u, w} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep.{w, u, u} k G ⥤ ModuleCat.{w, u} (MonoidAlgebra k G)).1
          V) :
      Type w)

Tactic:
Module.injective_of_isSemisimpleRing _ _

Premises used: Module.injective_of_isSemisimpleRing
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep.{w, u, u} k G
⊢ Module.Injective.{u, w} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep.{w, u, u} k G ⥤ ModuleCat.{w, u} (MonoidAlgebra k G)).1
          V) :
      Type w)

Tactic:
exact Module.injective_of_isSemisimpleRing _ _

Premises used: Module.injective_of_isSemisimpleRing
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep k G
rw :
  Module.Projective.{u, u} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep k G ⥤ ModuleCat (MonoidAlgebra k G)).1 V) : Type u)
⊢ Projective V

Tactic:
rw [← Rep.equivalenceModuleMonoidAlgebra.map_projective_iff,
    ← IsProjective.iff_projective]

Premises used: IsProjective.iff_projective, Rep.equivalenceModuleMonoidAlgebra, CategoryTheory.Equivalence.map_projective_iff
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep k G
⊢ Module.Projective.{u, u} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep k G ⥤ ModuleCat (MonoidAlgebra k G)).1 V) : Type u)

Tactic:
Module.projective_of_isSemisimpleRing _ _

Premises used: Module.projective_of_isSemisimpleRing
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : Rep k G
⊢ Module.Projective.{u, u} (MonoidAlgebra k G)
    (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep k G ⥤ ModuleCat (MonoidAlgebra k G)).1 V) : Type u)

Tactic:
exact Module.projective_of_isSemisimpleRing _ _

Premises used: Module.projective_of_isSemisimpleRing
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
⊢ Injective V

Tactic:
(forget₂ (FDRep k G) (Rep k G)).injective_of_map_injective inferInstance

Premises used: inferInstance, FDRep, CategoryTheory.forget₂, Rep, CategoryTheory.Functor.injective_of_map_injective
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
⊢ Projective V

Tactic:
(forget₂ (FDRep k G) (Rep k G)).projective_of_map_projective inferInstance

Premises used: CategoryTheory.Functor.projective_of_map_projective, inferInstance, FDRep, CategoryTheory.forget₂, Rep
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
⊢ Simple V

Tactic:
{ mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ }

Premises used: CategoryTheory.Simple.mk, Iff.intro
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
refine_1 : ∀ {W : FDRep k G} (f : W ⟶ V), Mono f → ∀ (hf : IsIso f) (habs : f = 0), False
refine_2 : ∀ {W : FDRep k G} (f : W ⟶ V), Mono f → ∀ (hf : f ≠ 0), IsIso f
⊢ Simple V

Tactic:
refine { mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ }
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsIso f
habs : f = 0
⊢ IsZero W ∧ IsZero V

Tactic:
rw [habs, isIsoZero_iff_source_target_isZero] at hf

Premises used: CategoryTheory.Limits.isIsoZero_iff_source_target_isZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsIso f
habs : f = 0
hf₁ : IsZero W ∧ IsZero V
⊢ f = 0

Tactic:
rw [habs, isIsoZero_iff_source_target_isZero] at hf

Premises used: CategoryTheory.Limits.isIsoZero_iff_source_target_isZero
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsZero W ∧ IsZero V
habs : f = 0
⊢ 0 < Module.finrank k (V ⟶ V)

Tactic:
grind
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsZero W ∧ IsZero V
habs : f = 0
refine_1 : ∀ (g : V ⟶ V) (hg : g ≠ 0), False
⊢ False

Tactic:
obtain ⟨g, hg⟩ : ∃ g : V ⟶ V, g ≠ 0 :=
        (Module.finrank_pos_iff_exists_ne_zero (R := k)).mp (by grind)

Premises used: Module.finrank_pos_iff_exists_ne_zero, Iff.mp
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsZero W ∧ IsZero V
habs : f = 0
g : V ⟶ V
hg : g ≠ 0
⊢ False

Tactic:
hg (hf.2.eq_zero_of_src g)

Premises used: And.right, CategoryTheory.Limits.IsZero.eq_zero_of_src
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : IsZero W ∧ IsZero V
habs : f = 0
g : V ⟶ V
hg : g ≠ 0
⊢ False

Tactic:
exact hg (hf.2.eq_zero_of_src g)

Premises used: And.right, CategoryTheory.Limits.IsZero.eq_zero_of_src
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f

Tactic:
isIso_of_mono_of_epi f

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f

Tactic:
exact isIso_of_mono_of_epi f

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
refine_2 : Epi f
⊢ IsIso f

Tactic:
suffices Epi f by exact isIso_of_mono_of_epi f
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
this : Epi (X := Abelian.image f) (Abelian.image.ι f)
rw : Epi (CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f))
⊢ Epi f

Tactic:
rw [← Abelian.image.fac f]

Premises used: CategoryTheory.Abelian.image.fac
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
this : Epi (X := Abelian.image f) (Abelian.image.ι f)
⊢ Epi (CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f))

Tactic:
epi_comp _ _

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
this : Epi (X := Abelian.image f) (Abelian.image.ι f)
⊢ Epi (CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f))

Tactic:
exact epi_comp _ _

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
refine_2 : Epi (X := Abelian.image f) (Abelian.image.ι f)
⊢ Epi f

Tactic:
suffices Epi (Abelian.image.ι f) by
        rw [← Abelian.image.fac f]
        exact epi_comp _ _
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : f ≠ 0
⊢ CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f) ≠ 0

Tactic:
rw [← Abelian.image.fac f] at hf

Premises used: CategoryTheory.Abelian.image.fac
-- Module: Mathlib.RepresentationTheory.FinGroupCharZero
Goal:
k : Type u
inst : Field k
G : Type u
inst_1 : Finite G
inst_2 : Group G
inst_3 : IsAlgClosed k
inst_4 : NeZero.{u} (R := k) (↑(Nat.card G) : k)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
h_1 : Mono f
hf : CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f) ≠ 0
refine_2 :
  let ι : Abelian.image f ⟶ V := Abelian.image.ι f;
  ∀ (hf : Abelian.factorThruImage f ≫ ι ≠ 0), Epi ι
⊢ Epi (X := Abelian.image f) (Abelian.image.ι f)

Tactic:
set ι := Abelian.image.ι f

Premises used: CategoryTheory.Abelian.image.ι