awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
⊢ { toFun := fun (f : G → k) (t : G) ↦ f ((x * x_1)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := (G → k) →ₗ[k] G → k)
      { toFun := fun (f : G → k) (t : G) ↦ f (x⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
      { toFun := fun (f : G → k) (t : G) ↦ f (x_1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
have h : ∀ (x_2 : G → k) (x_3 : G),
  Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f ((x * x_1)⁻¹ * t), map_add' := sorry, map_smul' := sorry } : (a : G → k) → G → k)
        x_2 x_3 :
      k)
    ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
            { toFun := fun (f : G → k) (t : G) ↦ f (x⁻¹ * t), map_add' := sorry, map_smul' := sorry : (G → k) →ₗ[k] G → k }
            { toFun := fun (f : G → k) (t : G) ↦ f (x_1⁻¹ * t), map_add' := sorry, map_smul' := sorry : (G → k) →ₗ[k] G → k } :
          (a : G → k) → G → k)
        x_2 x_3 :
      k)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Nontrivial k
s t : G
h :
  Eq (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) s :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) t :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
⊢ s = t
have h₁ : Eq (α := k)
  ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) carrier
          _ _
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom
            (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) s)))
              rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      (single (M := fun (a : G) ↦ k) t 1) 1 :
    k)
  ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) carrier
          _ _
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom
            (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) t)))
              rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      (single (M := fun (a : G) ↦ k) t 1) 1 :
    k)
Tactic: apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Nontrivial k
s t : G
h :
  Eq (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) s :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) t :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
⊢ s = t
have h₁ : Eq (α := k)
  ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) carrier
          _ _
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom
            (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) s)))
              rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      (single (M := fun (a : G) ↦ k) t 1) 1 :
    k)
  ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) carrier
          _ _
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom
            (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) t)))
              rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      (single (M := fun (a : G) ↦ k) t 1) 1 :
    k)
Tactic: classical
  apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
  simp_all [single_apply]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
g : G
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := FGModuleCat k) (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Action.V (G := G) rightFDRep))
    (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
          (a : G) → End (rightFDRep ⊗ rightFDRep).V)
        g)
      (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))
    (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep) (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
      ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))
have h : ∀
  (u :
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))) :
      Type u)),
  Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                    (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                  g)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        u :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        u :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
Tactic: ext u
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
f g : G → k
⊢ let α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep));
  (α : (a : G → k) → G → k) (f * g) =
    HMul.hMul (α := G → k) (β := G → k) ((α : (a : G → k) → G → k) f : G → k) ((α : (a : G → k) → G → k) g : G → k)
have nat : Eq (α :=
  Quiver.Hom (V := FGModuleCat k)
    (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
      (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
    (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
  (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
    CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
Tactic: have nat := η.hom.hom.naturality mulRepHom
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
⊢ let α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep));
  (α : (a : G → k) → G → k) (f * g) =
    HMul.hMul (α := G → k) (β := G → k) ((α : (a : G → k) → G → k) f : G → k) ((α : (a : G → k) → G → k) g : G → k)
have tensor : ∀ (X Y : FDRep k G),
  Eq (α :=
    Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
Tactic: have tensor (X Y) : η.hom.hom.app (X ⊗ Y) = (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y) :=
    η.hom.isMonoidal.tensor X Y
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
tensor :
  ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
⊢ let α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep));
  (α : (a : G → k) → G → k) (f * g) =
    HMul.hMul (α := G → k) (β := G → k) ((α : (a : G → k) → G → k) f : G → k) ((α : (a : G → k) → G → k) g : G → k)
have nat₁ : Eq (α :=
  Quiver.Hom (V := FGModuleCat k)
    (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
      (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
    (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
  ((η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫
    CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
Tactic: rw [tensor] at nat
Cleared hypotheses: nat, tensor
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
⊢ (G → k) →ₐ[k] G → k
have refine : Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
Tactic: refine AlgHom.ofLinearMap α ?_ (map_mul_toRightFDRepComp η)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
this h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
have rwa : ∀
  (this :
    Eq (α := G → k)
      ((α : (a : G → k) → G → k)
          (HMul.hMul (α := G → k) (β := G → k) (1 : G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k)) :
        G → k)
      (1 : G → k))
  (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
  Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
Tactic: rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
this h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
rwa :
  ∀
    (this :
      Eq (α := G → k)
        ((α : (a : G → k) → G → k)
            (HMul.hMul (α := G → k) (β := G → k) (1 : G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k)) :
          G → k)
        (1 : G → k))
    (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
    Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
have rwa₁ : ∀
  (this :
    HMul.hMul (α := G → k) (β := G → k)
        (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)) :
                (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                        (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                    Type u) →ₗ[k]
                  (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                        (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                    Type u)) :
              (a : G → k) → G → k)
            1 :
          G → k)
        (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)) :
                (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                        (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                    Type u) →ₗ[k]
                  (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                        (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                    Type u)) :
              (a : G → k) → G → k)
            ((α_inv : (a : G → k) → G → k) 1 : G → k) :
          G → k) =
      1)
  (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
  Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
Tactic: rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
have suffices : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
Tactic: suffices α (α_inv 1) = (1 : G → k) by
    have h := this
    rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
have this : η.inv ≫ η.hom = 𝟙 (forget k G)
Tactic: have := η.inv_hom_id
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
this : η.inv ≫ η.hom = 𝟙 (forget k G)
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
have this₁ : Eq (α :=
  (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
        (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
    Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC := carrier) (X :=
          ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom ((η.inv ≫ η.hom).hom.app rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      1 :
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
      Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC := carrier) (X :=
          ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
          (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (𝟙 (forget k G))) rightFDRep)) :
        (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
      1 :
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
      Type u))
Tactic: apply_fun (fun x ↦ (x.hom.app rightFDRep).hom (1 : G → k)) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Fintype G
X : FDRep k G
v : (↑X.V : Type u)
t : G
⊢ Eq.{u + 1} (α := Action.V (G := G) rightFDRep ⟶ X.V)
    (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep) ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) t)
      (InducedCategory.homMk (↟(sumSMulInv v))))
    (CategoryStruct.comp (Y := X.V) (InducedCategory.homMk (↟(sumSMulInv v))) ((X.ρ : (a : G) → End X.V) t))
have h : ∀ (f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)),
  Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) t) (InducedCategory.homMk (↟(sumSMulInv v))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑X.V.obj : Type u))
        f :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V) (InducedCategory.homMk (↟(sumSMulInv v)))
                ((X.ρ : (a : G) → End X.V) t))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑X.V.obj : Type u))
        f :
      (↑(X.V.obj (P := isFG k)) : Type u))
Tactic: ext f
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Fintype G
X : FDRep k G
v : (↑X.V : Type u)
t : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
φ_term : (X : FDRep k G) → (f : G → k) → (v : (↑X.V : Type u)) → (s : G) → (↑X.V : Type u) :=
  fun (X : FDRep k G) (f : G → k) (v : (↑X.V : Type u)) (s : G) ↦
    HSMul.hSMul (β := (↑X.V : Type u)) (f s)
      ((((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) s⁻¹ : (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) :
            (a : (↑X.V : Type u)) → (↑X.V : Type u))
          v :
        (↑X.V : Type u))
⊢ Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) t) (InducedCategory.homMk (↟(sumSMulInv v))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑X.V.obj : Type u))
        f :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V) (InducedCategory.homMk (↟(sumSMulInv v)))
                ((X.ρ : (a : G) → End X.V) t))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑X.V.obj : Type u))
        f :
      (↑(X.V.obj (P := isFG k)) : Type u))
have this : Eq (α := (↑X.V : Type u))
  (∑ x ∈ map (mulRightEmbedding t⁻¹) univ,
    φ_term X ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) t : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k) f) v x)
  (∑ x : G,
    φ_term X ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) t : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k) f) v
      ((mulRightEmbedding t⁻¹ : (a : G) → G) x))
Tactic: have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (rightRegular t f) v)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η₁ η₂ : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
h :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (η₁.hom.hom.app rightFDRep) (η₂.hom.hom.app rightFDRep)
⊢ η₁ = η₂
have have : ∀ (this : Fintype G), η₁ = η₂
Tactic: have := Fintype.ofFinite G