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
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)
this : Fintype G
⊢ η₁ = η₂
have h₁ : ∀ (X : FDRep k G) (v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)),
  Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
Tactic: ext X v
-- 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)
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)
this : Fintype G
X : FDRep k G
v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
have h1 : Eq (α :=
  Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
    Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₁.hom.hom.app X)
  (η₁.hom.hom.app rightFDRep ≫
    CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))
Tactic: have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
-- 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)
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)
this : Fintype G
X : FDRep k G
v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)
h1 :
  Eq (α :=
    Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₁.hom.hom.app X)
    (η₁.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
have h2 : Eq (α :=
  Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
    Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₂.hom.hom.app X)
  (η₂.hom.hom.app rightFDRep ≫
    CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))
Tactic: have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
-- 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)
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)
this : Fintype G
X : FDRep k G
v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)
h1 :
  Eq (α :=
    Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₁.hom.hom.app X)
    (η₁.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))
h2 :
  Eq (α :=
    Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₂.hom.hom.app X)
    (η₂.hom.hom.app rightFDRep ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
have h1₁ : Eq (α :=
  Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
    Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₁.hom.hom.app X)
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₂.hom.hom.app X)
Tactic: rw [h, ← h2] at h1
Cleared hypotheses: h1, h2
-- 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)
this : Fintype G
⊢ η₁ = η₂
have h₁ : ∀ (X : FDRep k G) (v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)),
  Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
Tactic: classical
  ext X v
  have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
  have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
  rw [h, ← h2] at h1
  simpa using congr(($h1).hom (single 1 1))
-- 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)
this : Fintype G
h₁ :
  ∀ (X : FDRep k G) (v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u)),
    Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
      ((Hom.hom (η₁.hom.hom.app X).hom :
            (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
          v :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
      ((Hom.hom (η₂.hom.hom.app X).hom :
            (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
          v :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
⊢ η₁ = η₂
have h₂ : ∀ (X : FDRep k G) (v : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
  (h1 :
    Eq (α :=
      Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
      (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₁.hom.hom.app X)
      (η₁.hom.hom.app rightFDRep ≫
        CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v))),
  Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₁.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
    ((Hom.hom (η₂.hom.hom.app X).hom :
          (a : (↑((forget k G).obj X).obj : Type u)) → (↑((forget k G).obj X).obj : Type u))
        v :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X).obj (P := isFG k)) : Type u))
Tactic: classical
  ext X v
  have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
  have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
  rw [h, ← h2] at h1
  simpa using congr(($h1).hom (single 1 1))
-- 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
s x : G
⊢ Eq.{u + 1} (α := Quiver.Hom (V := FGModuleCat k) (Action.V (G := G) rightFDRep) (Action.V (G := G) rightFDRep))
    (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep) ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
      (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))
    (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
      (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
      ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))
have h : ∀ (f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) 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) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(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 (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
Tactic: ext f
-- 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
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) 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) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(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 (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
have h : ∀ (x_1 : G),
  Eq (α := k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)
Tactic: funext _
-- 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
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
x_1 : G
⊢ Eq (α := k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)
have h : s⁻¹ * x_1 * x = s⁻¹ * (x_1 * x)
Tactic: apply congrArg f
-- 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 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
⊢ ∃ (s : G),
    Eq (α :=
      (↑(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))
      (Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))) ((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s)
have refine : ∀ (u : G),
  Eq (α :=
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
      Type u))
    (((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) → (↑((forget k G).obj rightFDRep).obj : Type u))
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) :
          (a : G → k) → (↑((forget k G).obj rightFDRep).obj : Type u))
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
Tactic: refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
-- 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 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u : G
⊢ Eq (α :=
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
      Type u))
    (((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) → (↑((forget k G).obj rightFDRep).obj : Type u))
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) :
          (a : G → k) → (↑((forget k G).obj rightFDRep).obj : Type u))
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
have simp : Eq (α := G → k)
  (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
          (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
        (a : G → k) → G → k)
      ((basisFun k G : (a : G) → G → k) u : G → k) :
    G → k)
  ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
      ((basisFun k G : (a : G) → G → k) u : G → k) :
    G → k)
Tactic: simp only [rightFDRep, forget_obj]
-- 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 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u : G
⊢ Eq (α := G → k)
    (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
            (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
          (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      G → k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) :
      G → k)
have h : ∀ (t : G),
  Eq (α := k)
    (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
            (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
          (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
Tactic: ext t
-- 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 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
s : G
hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s
u t : G
⊢ Eq (α := k)
    (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
            (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
          (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
    ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((basisFun k G : (a : G) → G → k) u : G → k) t :
      k)
have nat : 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))
  (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹) ≫
    η.hom.hom.app rightFDRep)
  (η.hom.hom.app rightFDRep ≫
    CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹))
Tactic: have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)