awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
⊢ (functorToContAction F).Full

Tactic:
inferInstanceAs <| (ObjectProperty.lift _ _ _).Full

Premises used: _private.0.CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatFunObjFiniteAutFunctorFunctorToContAction._proof_1
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
⊢ ContinuousSMul.{u₁, u₁} (Aut F)
    X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj

Tactic:
have : ContinuousSMul (Aut F) X.obj.V := X.2
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
this :
  ContinuousSMul.{u₁, u₁} (Aut F)
    X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj
obtain :
  ∀ (A : C)
    (i :
      (functorToAction F).obj A ≅
        X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))),
    (functorToContAction F).essImage X
⊢ (functorToContAction F).essImage X

Tactic:
obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X

Premises used: CategoryTheory.PreGaloisCategory.exists_lift_of_continuous, CategoryTheory.ObjectProperty.FullSubcategory.obj
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
this :
  ContinuousSMul.{u₁, u₁} (Aut F)
    X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj
A : C
i :
  (functorToAction F).obj A ≅
    X.obj (P :=
      Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
⊢ (functorToContAction F).essImage X

Tactic:
⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.ObjectProperty.isoMk, Exists.intro
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F_1 : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F_1
F : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat
inst_3 : FiberFunctor F
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F)
this :
  ContinuousSMul.{u₁, u₁} (Aut F)
    X.obj (P :=
          Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
            fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj
A : C
i :
  (functorToAction F).obj A ≅
    X.obj (P :=
      Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
        fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
⊢ (functorToContAction F).essImage X

Tactic:
exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := ⋯
⊢ (functorToContAction F').EssSurj

Tactic:
have : (functorToContAction F').EssSurj := inferInstance
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
⊢ Continuous.{u₁, w} (Y :=
    (FintypeCat.uSwitch.obj
        X.obj (P :=
            Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V).obj)
    fun
      (p :
        X.obj (P :=
              Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj) ↦
    (Equiv.symm
          X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.uSwitchEquiv :
        (a : X.obj.V.obj) → (FintypeCat.uSwitch.obj X.obj.V).obj)
      p

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X :
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
⊢ Continuous (Y :=
    Aut F' ×
      (fun (X : Type u₁) ↦ X)
        X.obj (P :=
              Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj)
    fun
      (p :
        Prod.{u₁, w} (Aut F')
          (FintypeCat.uSwitch.obj
              X.obj (P :=
                  Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V).obj) ↦
    (p.1,
      (X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.uSwitchEquiv :
          (a : (FintypeCat.uSwitch.obj X.obj.V).obj) → X.obj.V.obj)
        p.2)

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X :
  ContAction.{w, w + 1, w, w, u₁} FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
⊢ Continuous.{w, u₁} (Y :=
    (FintypeCat.uSwitch.obj
        X.obj (P :=
            Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
              (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V).obj)
    fun
      (p :
        X.obj (P :=
              Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj) ↦
    (Equiv.symm
          X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.uSwitchEquiv :
        (a : X.obj.V.obj) → (FintypeCat.uSwitch.obj X.obj.V).obj)
      p

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
X :
  ContAction.{w, w + 1, w, w, u₁} FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F')
⊢ Continuous (Y :=
    Prod.{u₁, w} (Aut F')
      ((fun (X : Type w) ↦ X)
        X.obj (P :=
              Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.obj))
    fun
      (p :
        Aut F' ×
          (FintypeCat.uSwitch.obj
              X.obj (P :=
                  Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                    TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V).obj) ↦
    (p.1,
      (X.obj (P :=
                Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
                  (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)).V.uSwitchEquiv :
          (a : (FintypeCat.uSwitch.obj X.obj.V).obj) → X.obj.V.obj)
        p.2)

Tactic:
fun_prop
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f_1 : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') ≌
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f_1)
X Y : C
f : X ⟶ Y
⊢ Action.Hom.hom
      (InducedCategory.Hom.hom
        ((functorToContAction F).map f ≫
          Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              Y))) =
    Action.Hom.hom
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              X) ≫
          (functorToContAction F' ⋙ equiv.functor).map f))

Tactic:
FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f)

Premises used: CategoryTheory.Equivalence.unitIso, FintypeCat.uSwitchEquivalence, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, FintypeCat.homMk
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f_1 : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') ≌
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f_1)
X Y : C
f : X ⟶ Y
⊢ Action.Hom.hom
      (InducedCategory.Hom.hom
        ((functorToContAction F).map f ≫
          Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              Y))) =
    Action.Hom.hom
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (X : C) ↦
                (ObjectProperty.isoMk
                    (Action.IsContinuous (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
                      TypeCat.Fun X.obj Y.obj) (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj))
                    (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app (F.obj X)) ⋯) :
                  (functorToContAction F).obj X ≅ (functorToContAction F' ⋙ equiv.functor).obj X))
              X) ≫
          (functorToContAction F' ⋙ equiv.functor).map f))

Tactic:
exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f)

Premises used: CategoryTheory.Equivalence.unitIso, FintypeCat.uSwitchEquivalence, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') ≌
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f)
have : ∀ (this : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor), (functorToContAction F).EssSurj
⊢ (functorToContAction F).EssSurj

Tactic:
have : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor :=
    NatIso.ofComponents
      (fun X ↦ ObjectProperty.isoMk _ (Action.mkIso (FintypeCat.uSwitchEquivalence.unitIso.app _)
      (fun g ↦ FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (g.hom.app X))))
      (fun f ↦ by
        ext : 2
        exact FintypeCat.uSwitchEquivalence.unitIso.hom.naturality (F.map f))
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this_2 : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') ≌
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f)
this : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor
⊢ (functorToContAction F).EssSurj

Tactic:
Functor.essSurj_of_iso this.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.essSurj_of_iso
-- Module: Mathlib.CategoryTheory.Galois.Equivalence
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
F' : Functor.{u₂, u₁, u₁, u₁ + 1} C FintypeCat := F ⋙ FintypeCat.uSwitch
this_1 : FiberFunctor F' := ⋯
this_2 : (functorToContAction F').EssSurj
f : Aut F ≃ₜ* Aut F' := autEquivAutWhiskerRight F FintypeCat.uSwitchEquivalence.fullyFaithfulFunctor
equiv : ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') ≌
  ContAction FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CV :=
    fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F) :=
  Equivalence.trans
    (Equivalence.mapContAction (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (FW :=
      fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj) (CW :=
      fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (Aut F') FintypeCat.uSwitchEquivalence ⋯ ⋯)
    (ContAction.resEquiv FintypeCat (FV := fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
      (CV := fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) f)
this : functorToContAction F ≅ functorToContAction F' ⋙ equiv.functor
⊢ (functorToContAction F).EssSurj

Tactic:
exact Functor.essSurj_of_iso this.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.essSurj_of_iso
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
k i j : I
hij : i + j = k
⊢ j + i = k

Tactic:
simpa only [add_comm j i] using hij

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.GradedObject.Braiding
Goal:
I : Type u_1
inst : AddCommMonoid I
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : MonoidalCategory.{v_1, u_2} C
X Y Z : GradedObject I C
inst_3 : BraidedCategory.{v_1, u_2} C
inst_4 : HasTensor.{u_1, v_1, u_2} X Y
inst_5 : HasTensor.{u_1, v_1, u_2} Y X
inst_6 : HasTensor.{u_1, v_1, u_2} X Z
inst_7 : HasTensor.{u_1, v_1, u_2} Z X
f : Y ⟶ Z
dsimp :
  Eq (α := tensorObj.{u_1, v_1, u_2} X Y ⟶ tensorObj.{u_1, v_1, u_2} Z X)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} X Z) (whiskerLeft X f) fun (k : I) ↦
      tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Z j)) ≫ ιTensorObj Z X j i k ⋯)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X)
      (fun (k : I) ↦ tensorObjDesc fun (i j : I) (hij : i + j = k) ↦ Iso.hom (β_ (X i) (Y j)) ≫ ιTensorObj Y X j i k ⋯)
      (whiskerRight f X))
⊢ Eq (α := tensorObj.{u_1, v_1, u_2} X Y ⟶ tensorObj.{u_1, v_1, u_2} Z X)
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} X Z) (whiskerLeft X f) (Iso.hom (braiding X Z)))
    (CategoryStruct.comp (Y := tensorObj.{u_1, v_1, u_2} Y X) (Iso.hom (braiding X Y)) (whiskerRight f X))

Tactic:
dsimp [braiding]

Premises used: CategoryTheory.GradedObject.Monoidal.braiding