awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
g : G
⊢ Eq (α := (α →₀ G →₀ k) →ₗ[k] V)
    (((linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
        (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
      (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g)
    ((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
      (linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
        (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k))
have h : ∀ (a : α) (a_1 : G),
  Eq.{v' + 1} (α := V)
    ((((((linearCombination k fun (x : α × G) ↦ (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                  (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
                (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)
    (((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
                (linearCombination k fun (x : α × G) ↦
                    (((σ : (a : G) → V →ₗ[k] V) x.2 : V →ₗ[k] V) : (a : V) → V) (f x.1)) ∘ₗ
                  (↑(LinearEquiv.symm (curryLinearEquiv k)) : (α →₀ G →₀ k) →ₗ[k] α × G →₀ k)) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : IntertwiningMap (free k G α) σ
⊢ σ.freeLift
      ((fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦ ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
        f) =
    f
have h : ∀ (a : α) (a_1 : G),
  Eq.{v' + 1} (α := V)
    (((toLinearMap
                (σ.freeLift
                  ((fun (f : IntertwiningMap (free k G α) σ) (i : α) ↦
                      ((f : (a : α →₀ G →₀ k) → V) (single i (single 1 1)) : V))
                    f)) ∘ₗ
              lsingle a) ∘ₗ
            lsingle a_1 :
          (a : k) → V)
        1 :
      V)
    (((f.toLinearMap ∘ₗ lsingle a) ∘ₗ lsingle a_1 : (a : k) → V) 1 : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
g : G
⊢ (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ curryLinearEquiv k) :
        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k) ∘ₗ
      (tprod (leftRegular k G) (trivial k G (α →₀ k)) :
          (a : G) → TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] TensorProduct k (G →₀ k) (α →₀ k))
        g =
    (free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g ∘ₗ
      (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ curryLinearEquiv k) :
        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k)
have a : ∀ (a : G) (a_1 a_2 : α) (a_3 : G),
  Eq.{u + 1} (α := k)
    (((((((TensorProduct.AlgebraTensorModule.curry
                                ((↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                        curryLinearEquiv k) :
                                    TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k) ∘ₗ
                                  (tprod (leftRegular k G) (trivial k G (α →₀ k)) :
                                      (a : G) →
                                        TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] TensorProduct k (G →₀ k) (α →₀ k))
                                    g) ∘ₗ
                              lsingle a :
                            k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                          (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                        1 ∘ₗ
                      lsingle a_1 :
                    (a : k) → α →₀ G →₀ k)
                  1 :
                (a : α) → G →₀ k)
              a_2 :
            G →₀ k) :
          (a : G) → k)
        a_3 :
      k)
    (((((((TensorProduct.AlgebraTensorModule.curry
                                ((free k G α : (a : G) → (α →₀ G →₀ k) →ₗ[k] α →₀ G →₀ k) g ∘ₗ
                                  (↑(finsuppTensorFinsupp' k G α ≪≫ₗ Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                                        curryLinearEquiv k) :
                                    TensorProduct k (G →₀ k) (α →₀ k) →ₗ[k] α →₀ G →₀ k)) ∘ₗ
                              lsingle a :
                            k →ₗ[k] (α →₀ k) →ₗ[k] α →₀ G →₀ k) :
                          (a : k) → (α →₀ k) →ₗ[k] α →₀ G →₀ k)
                        1 ∘ₗ
                      lsingle a_1 :
                    (a : k) → α →₀ G →₀ k)
                  1 :
                (a : α) → G →₀ k)
              a_2 :
            G →₀ k) :
          (a : G) → k)
        a_3 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
v : V
g : G
⊢ Eq (α := (G →₀ k) →ₗ[k] V)
    (((Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
        (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
      (leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g)
    ((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
      (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
        (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v)
have h : ∀ (g' : G),
  Eq.{v' + 1} (α := V)
    (((((Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
              (leftRegular k G : (a : G) → (G →₀ k) →ₗ[k] G →₀ k) g) ∘ₗ
            Finsupp.lsingle g' :
          (a : k) → V)
        1 :
      V)
    ((((σ : (a : G) → V →ₗ[k] V) g ∘ₗ
              (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v) ∘ₗ
            Finsupp.lsingle g' :
          (a : k) → V)
        1 :
      V)
Tactic: ext g'
-- Lean 4 proof step from Mathlib.RepresentationTheory.Equiv (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v
inst_1 : Monoid G
V : Type v'
inst_2 : AddCommMonoid V
inst_3 : Module k_1 V
W : Type w'
inst_4 : AddCommMonoid W
inst_5 : Module k_1 W
H : Type w
inst_6 : Subsingleton H
inst_7 : MulOneClass H
inst_8 : MulAction G H
k : Type u
inst_9 : CommSemiring k
inst_10 : Module k V
inst_11 : Module k W
σ : Representation k G V
ρ : Representation k G W
x : IntertwiningMap (leftRegular k G) σ
⊢ (fun (v : V) ↦
        ({
            toLinearMap :=
              (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
            isIntertwining' := ⋯ } :
          IntertwiningMap (leftRegular k G) σ))
      ((fun (f : IntertwiningMap (leftRegular k G) σ) ↦
          ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
        x) =
    x
have h : ∀ (a : G),
  Eq.{v' + 1} (α := V)
    ((IntertwiningMap.toLinearMap (G := G) (ρ := leftRegular k G) (σ := σ)
              ((fun (v : V) ↦
                  ({
                      toLinearMap :=
                        (Finsupp.llift V k k G : (a : G → V) → (G →₀ k) →ₗ[k] V) fun (g : G) ↦
                          (((σ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v,
                      isIntertwining' := sorry } :
                    IntertwiningMap (leftRegular k G) σ))
                ((fun (f : IntertwiningMap (leftRegular k G) σ) ↦
                    ((LinearEquiv.symm (Finsupp.llift V k k G) : (a : (G →₀ k) →ₗ[k] V) → G → V) f.toLinearMap 1 : V))
                  x)) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → V)
        1 :
      V)
    ((x.toLinearMap ∘ₗ Finsupp.lsingle a : (a : k) → V) 1 : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ Eq.{u + 1} (α := (↑W.V : Type u) →ₗ[R] (↑W.V : Type u))
    ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g : (↑W.V : Type u) →ₗ[R] (↑W.V : Type u))
    (((isoToLinearEquiv i).conj : (a : Module.End R (↑V.V : Type u)) → Module.End R (↑W.V : Type u))
        ((V.ρ : (a : G) → (↑V.V : Type u) →ₗ[R] (↑V.V : Type u)) g) :
      Module.End R (↑W.V : Type u))
have rw : Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
    Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
        (CategoryStruct.comp (Y := V.V) ((V.ρ : (a : G) → End V.V) g)
          (Iso.hom (Functor.mapIso (Action.forget (FGModuleCat R) G) i)))) :
    W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
Tactic: rw [FDRep.isoToLinearEquiv, ← hom_hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj,
    Iso.conj_apply, ← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          (CategoryStruct.comp (Y := V.V) ((V.ρ : (a : G) → End V.V) g)
            (Iso.hom (Functor.mapIso (Action.forget (FGModuleCat R) G) i)))) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
have dsimp : Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
    Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
        ((V.ρ : (a : G) → End V.V) g ≫ i.hom.hom)) :
    W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
Tactic: dsimp only [Action.forget_map, Functor.mapIso_hom]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
Goal:
R : Type u
G : Type v
inst : CommRing R
inst_1 : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
      Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
    (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := V.V) (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i))
          ((V.ρ : (a : G) → End V.V) g ≫ i.hom.hom)) :
      W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
have rw : Eq (α := Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (ModuleCat.ofHom ((W.ρ : (a : G) → (↑W.V : Type u) →ₗ[R] (↑W.V : Type u)) g) :
    Quiver.Hom (V := ModuleCat R) (ModuleCat.of R (↑W.V : Type u)) (ModuleCat.of R (↑W.V : Type u)))
  (InducedCategory.Hom.hom
      (Iso.inv (Functor.mapIso (Action.forget (FGModuleCat R) G) i) ≫ i.hom.hom ≫ (W.ρ : (a : G) → End W.V) g) :
    W.V.obj (P := ModuleCat.isFG R) ⟶ W.V.obj (P := ModuleCat.isFG R))
Tactic: rw [i.hom.comm g]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
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
⊢ Eq.{u + 1} (α := X.V ⟶ Y.V)
    (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
      (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))
    (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
      ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))
have h : Eq.{u + 1} (α := (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.V.obj (P := ModuleCat.isFG R)) : Type u))
  (ModuleCat.Hom.hom
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
        (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))))
  (ModuleCat.Hom.hom
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
        ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
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
⊢ Eq.{u + 1} (α := (↑(X.V.obj (P := ModuleCat.isFG R)) : Type u) →ₗ[R] (↑(Y.V.obj (P := ModuleCat.isFG R)) : Type u))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := X.V) ((X.ρ : (a : G) → CategoryTheory.End X.V) g)
          (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)))))
    (ModuleCat.Hom.hom
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := Y.V) (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap))
          ((Y.ρ : (a : G) → CategoryTheory.End Y.V) g))))
have h : 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: simp only [FGModuleCat.obj_carrier, ObjectProperty.FullSubcategory.comp_hom,
      InducedCategory.homMk_hom, ModuleCat.hom_comp, hom_hom_action_ρ]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FDRep (goal)
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
⊢ MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) (of (V := Module.Dual k V) ρV.dual) W ≅ of (ρV.linHom W.ρ)
have 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)
Tactic: refine Action.mkIso (dualTensorIsoLinHomAux ρV W) (fun g => ?_)
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
⊢ Injective V
have 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)
Tactic: rw [← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff,
    ← Module.injective_iff_injective_object]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
⊢ Projective V
have rw : Module.Projective.{u, u} (MonoidAlgebra k G)
  (↑((Equivalence.functor equivalenceModuleMonoidAlgebra : Rep k G ⥤ ModuleCat (MonoidAlgebra k G)).1 V) : Type u)
Tactic: rw [← Rep.equivalenceModuleMonoidAlgebra.map_projective_iff,
    ← IsProjective.iff_projective]
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
have refine_1 : ∀ {W : FDRep k G} (f : W ⟶ V), Mono f → ∀ (hf : IsIso f) (habs : f = 0), False
Tactic: refine { mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ }
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
⊢ Simple V
have refine_2 : ∀ {W : FDRep k G} (f : W ⟶ V), Mono f → ∀ (hf : f ≠ 0), IsIso f
Tactic: refine { mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ }
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (hypothesis)
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
⊢ False
have hf₁ : IsZero W ∧ IsZero V
Tactic: rw [habs, isIsoZero_iff_source_target_isZero] at hf
Cleared hypotheses: hf, habs
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
⊢ False
have refine_1 : ∀ (g : V ⟶ V) (hg : g ≠ 0), False
Tactic: obtain ⟨g, hg⟩ : ∃ g : V ⟶ V, g ≠ 0 :=
        (Module.finrank_pos_iff_exists_ne_zero (R := k)).mp (by grind)
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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
⊢ IsIso f
have refine_2 : Epi f
Tactic: suffices Epi f by exact isIso_of_mono_of_epi f
-- Lean 4 proof step from Mathlib.RepresentationTheory.FinGroupCharZero (goal)
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 f
have rw : Epi (CategoryStruct.comp (Y := Abelian.image f) (Abelian.factorThruImage f) (Abelian.image.ι f))
Tactic: rw [← Abelian.image.fac f]