-- 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))
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))
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)))
    (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 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)
      (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: 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))