awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Tannaka
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 :
  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))
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)

Tactic:
this
-- Module: Mathlib.RepresentationTheory.Tannaka
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 :
  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))
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)

Tactic:
exact this
-- Module: Mathlib.RepresentationTheory.Tannaka
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)
x x_1 : G → k
⊢ ∑ s : G,
      HSMul.hSMul (β := (↑X.V : Type u)) ((x + x_1) 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)) =
    HAdd.hAdd (α := (↑X.V : Type u))
      (∑ s : G,
        HSMul.hSMul (β := (↑X.V : Type u)) (x 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)))
      (∑ s : G,
        HSMul.hSMul (β := (↑X.V : Type u)) (x_1 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)))

Tactic:
simp [add_smul, sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul
-- Module: Mathlib.RepresentationTheory.Tannaka
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)
x : k
x_1 : G → k
⊢ ∑ s : G,
      HSMul.hSMul (β := (↑X.V : Type u)) ((x • x_1) 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)) =
    HSMul.hSMul (α := k) (β := (↑X.V : Type u)) ((RingHom.id k : (a : k) → k) x : k)
      (∑ s : G,
        HSMul.hSMul (β := (↑X.V : Type u)) (x_1 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)))

Tactic:
simp [smul_sum, smul_smul]

Premises used: smul_smul, Finset.smul_sum
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Fintype G
inst_3 : DecidableEq G
X : FDRep k G
v : (↑X.V : Type u)
⊢ ∑ s : G,
      HSMul.hSMul (α := k) (β := (↑X.V : Type u)) (single (M := fun (a : G) ↦ k) 1 1 s : k)
        ((((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)) =
    v

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
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
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))
⊢ 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))

Tactic:
ext f
-- Module: Mathlib.RepresentationTheory.Tannaka
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 : 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)
-- Module: Mathlib.RepresentationTheory.Tannaka
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))
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))
⊢ 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:
simpa [φ_term] using this
-- Module: Mathlib.RepresentationTheory.Tannaka
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 : ∀ (this : Fintype G), η₁ = η₂
⊢ η₁ = η₂

Tactic:
have := Fintype.ofFinite G
-- Module: Mathlib.RepresentationTheory.Tannaka
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))
⊢ η₁ = η₂

Tactic:
ext X v
-- Module: Mathlib.RepresentationTheory.Tannaka
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 (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)
-- Module: Mathlib.RepresentationTheory.Tannaka
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 (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)
-- Module: Mathlib.RepresentationTheory.Tannaka
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 (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
-- Module: Mathlib.RepresentationTheory.Tannaka
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))
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)
⊢ 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:
rw [h, ← h2] at h1
-- Module: Mathlib.RepresentationTheory.Tannaka
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)
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (ofRightFDRep X v) ≫ η₂.hom.hom.app X)
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))

Tactic:
simpa using congr(($h1).hom (single 1 1))
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
s x : G
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))
⊢ 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))

Tactic:
ext f