mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y) i =
    (fun f ↦ (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map f)) y)
      (u.hom ≫ (functorToAction F).map f)

Tactic:
suffices h : i.hom y = F.map f z by simpa [hu]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝¹ : Mono i
inst✝ : IsConnected Y
y : ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).obj Y).obj
Z : C
f : Z ⟶ X
z : (F.obj Z).obj
hz : (ConcreteCategory.hom (F.map f)) z = (ConcreteCategory.hom i.hom) y
hc : IsConnected Z
hm : Mono f
this : IsConnected ((functorToAction F).obj Z)
u : Y ≅ (functorToAction F).obj Z
hu : (ConcreteCategory.hom ((forget₂ (Action FintypeCat (Aut F)) FintypeCat).map u.hom)) y = z
⊢ (ConcreteCategory.hom i.hom) y = (ConcreteCategory.hom (F.map f)) z
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X) = t

Tactic:
← piComparison_comp_π

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).obj
⊢ (ConcreteCategory.hom ((piComparison F fun x ↦ X) ≫ Pi.π (fun b ↦ F.obj X) t)) (mkSelfProdFib F X) = t
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
Z : C
h : Z ⟶ A
z : (F.obj Z).obj
hgal : IsGalois Z
hhz : (ConcreteCategory.hom (F.map h)) z = a
⊢ ∃ W h, h ≫ { val := f, comp := hf } = h ≫ { val := g, comp := hg }

Tactic:
refine ⟨⟨Z, z, hgal⟩, ⟨h, hhz⟩, hom_ext ?_⟩

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
x✝³ x✝² : PointedGaloisObject F
A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
x✝¹ x✝ : { obj := A, pt := a, isGalois := isGalois✝¹ } ⟶ { obj := B, pt := b, isGalois := isGalois✝ }
f : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hf :
  (ConcreteCategory.hom (F.map f)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
g : { obj := A, pt := a, isGalois := isGalois✝¹ }.obj ⟶ { obj := B, pt := b, isGalois := isGalois✝ }.obj
hg :
  (ConcreteCategory.hom (F.map g)) { obj := A, pt := a, isGalois := isGalois✝¹ }.pt =
    { obj := B, pt := b, isGalois := isGalois✝ }.pt
Z : C
h : Z ⟶ A
z : (F.obj Z).obj
hgal : IsGalois Z
hhz : (ConcreteCategory.hom (F.map h)) z = a
⊢ ({ val := h, comp := hhz } ≫ { val := f, comp := hf }).val =
    ({ val := h, comp := hhz } ≫ { val := g, comp := hg }).val
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: case h
C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
  u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
this✝¹ : Mono i
Z : C
g : Z ⟶ X ⨯ Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left✝ : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
this✝ : IsIso ((functorToAction F).map ψ)
this : IsIso ψ
z : (F.obj Z).obj
⊢ (ConcreteCategory.hom ((functorToAction F).map ψ ≫ (functorToAction F).map (inv ψ ≫ g ≫ prod.snd)).hom) z =
    (ConcreteCategory.hom ((functorToAction F).map ψ ≫ f).hom) z

Tactic:
simp [-FintypeCat.comp_apply, -Action.comp_hom, i, u, ψ, hgvi]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
u : A ⟶ X
v : B ⟶ X
⊢ (ConcreteCategory.hom
          ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
            (Opposite.op { obj := A, pt := a, isGalois := isGalois✝¹ })))
        u =
      (ConcreteCategory.hom
          ((((evaluation C (Type u₂)).obj X).mapCocone (cocone F)).ι.app
            (Opposite.op { obj := B, pt := b, isGalois := isGalois✝ })))
        v →
    ∃ k f g,
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
        (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v

Tactic:
(h : F.map u a = F.map v b)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝¹ : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
⊢ ∃ k f g,
    (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map f)) u =
      (ConcreteCategory.hom ((((incl F).op ⋙ coyoneda) ⋙ (evaluation C (Type u₂)).obj X).map g)) v
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
g : G
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (isoOnObj F g Y).hom = (isoOnObj F g X).hom ≫ F.map f

Tactic:
by
    intro X Y f
    ext
    exact (IsNaturalSMul.naturality _ _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
    (associator X Y Z).hom k ≫
      (tensorObjDesc fun i j hij ↦ (β_ (X i) (tensorObj Y Z j)).hom ≫ ιTensorObj (tensorObj Y Z) X j i k ⋯) ≫
        (associator Y Z X).hom k

Tactic:
rw [ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl,
    assoc, ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.id_tensorHom,
    BraidedCategory.braiding_naturality_assoc,
    BraidedCategory.braiding_tensor_right_hom, assoc, assoc, assoc, assoc, Iso.hom_inv_id_assoc,
    MonoidalCategory.tensorHom_id,
    ← ιTensorObj₃'_eq_assoc Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h]) _ rfl,
    ιTensorObj₃'_associator_hom, Iso.inv_hom_id_assoc]

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
    (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
    whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) Z k ≫
      (associator Y X Z).hom k ≫
        whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k

Tactic:
ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) (Z i₃) ≫
      ιTensorObj (tensorObj X Y) Z (i₁ + i₂) i₃ k ⋯) ≫
    whiskerRight (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) Z k ≫
      (associator Y X Z).hom k ≫
        whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.y
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ X ⟶ X

pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) ?cons.y

pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) ?cons.y (𝟙 X)

Tactic:
· exact q ≫ Quiver.Path.reverse q

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q.cons f ≫ (reverse f).toPath.comp q.reverse) (q ≫ q.reverse)

case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: G : Type u₁
inst✝ : Groupoid G
⊢ lift (of G) = 𝟭 (FreeGroupoid G)

Tactic:
symm

Goal state after:
G : Type u₁
inst✝ : Groupoid G
⊢ 𝟭 (FreeGroupoid G) = lift (of G)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ lift (φ ⋙ ψ) = lift φ ⋙ ψ

Tactic:
symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : Type u₁
inst✝¹ : Groupoid G
H : Type u₂
inst✝ : Groupoid H
φ : C ⥤ G
ψ : G ⥤ H
⊢ lift φ ⋙ ψ = lift (φ ⋙ ψ)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ map (𝟭 C) = 𝟭 (FreeGroupoid C)

Tactic:
symm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟭 (FreeGroupoid C) = map (𝟭 C)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Category.{v₂, u₂} E
φ : C ⥤ D
φ' : D ⥤ E
⊢ map (φ ⋙ φ') = map φ ⋙ map φ'

Tactic:
symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
E : Type u₂
inst✝ : Category.{v₂, u₂} E
φ : C ⥤ D
φ' : D ⥤ E
⊢ map φ ⋙ map φ' = map (φ ⋙ φ')
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ 𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X)) =
    (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f)

Tactic:
symm

Goal state after:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
X✝ Y✝ : Paths (Symmetrify V)
X Y : Symmetrify V
f : X ⟶ Y
⊢ (Symmetrify.lift φ).map f ≫ reverse ((Symmetrify.lift φ).map f) =
    𝟙 ((Symmetrify.lift φ).obj ((Paths.of (Symmetrify V)).obj X))
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ lift (𝟭q V ⋙q of V) = 𝟭 (Quiver.FreeGroupoid V)

Tactic:
symm

Goal state after:
V : Type u
inst✝ : Quiver V
⊢ 𝟭 (Quiver.FreeGroupoid V) = lift (𝟭q V ⋙q of V)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q φ' ⋙q of V'') = lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'')

Tactic:
symm

Goal state after:
V : Type u
inst✝² : Quiver V
V' : Type u'
inst✝¹ : Quiver V'
V'' : Type u''
inst✝ : Quiver V''
φ : V ⥤q V'
φ' : V' ⥤q V''
⊢ lift (φ ⋙q of V') ⋙ lift (φ' ⋙q of V'') = lift (φ ⋙q φ' ⋙q of V'')
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      (tensorObjDesc fun i j hij ↦ (β_ (tensorObj X Y i) (Z j)).hom ≫ ιTensorObj Z (tensorObj X Y) j i k ⋯) ≫
        (associator Z X Y).inv k

Tactic:
ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor Z
inst✝¹⁴ : Z.HasTensor X
inst✝¹³ : Z.HasTensor Y
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : Z.HasTensor (tensorObj X Y)
inst✝⁸ : (tensorObj Z X).HasTensor Y
inst✝⁷ : X.HasTensor (tensorObj Z Y)
inst✝⁶ : (tensorObj X Z).HasTensor Y
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Z.HasGoodTensor₁₂Tensor X Y
inst✝² : Z.HasGoodTensorTensor₂₃ X Y
inst✝¹ : X.HasGoodTensor₁₂Tensor Z Y
inst✝ : X.HasGoodTensorTensor₂₃ Z Y
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
| (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
    (MonoidalCategoryStruct.whiskerRight (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) (Z i₃) ≫
        ιTensorObj (tensorObj X Y) Z (i₁ + i₂) i₃ k ⋯) ≫
      (tensorObjDesc fun i j hij ↦ (β_ (tensorObj X Y i) (Z j)).hom ≫ ιTensorObj Z (tensorObj X Y) j i k ⋯) ≫
        (associator Z X Y).inv k
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ d ∈ (im φ hφ).objs

Tactic:
hφ'

Goal state after:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ d ∈ ⊤.objs
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ (im φ hφ).objs

Tactic:
hφ'

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ ⊤.objs
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c')

Tactic:
hφ'

Goal state after:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ g ∈ ⊤.arrows (φ.obj c) (φ.obj c')
Module: Mathlib.CategoryTheory.Limits.Pi

Goal state before:
pp: I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
i : I
⊢ ((fun i ↦ (P i).lift (coneCompEval s i)) ≫ (coneOfConeCompEval c).π.app j) i = s.π.app j i

Tactic:
exact (P i).fac (coneCompEval s i) j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteProducts C
X✝ Y✝ Z✝ : FormalCoproduct C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun x ↦ powerMap (x✝¹ ≫ x✝) (ToType (Opposite.unop x)), naturality := ⋯ } =
    { app := fun x ↦ powerMap x✝¹ (ToType (Opposite.unop x)), naturality := ⋯ } ≫
      { app := fun x ↦ powerMap x✝ (ToType (Opposite.unop x)), naturality := ⋯ }

Tactic:
ext : 1; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.obj Y₁).map f₂ ≫ (F.map (Cofork.π c₁)).app Y₂ ≫ l = coprod.inr ≫ 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l

Tactic:
NatTrans.naturality_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C : Type u_3
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} C
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : HasZeroMorphisms C
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
F : C₁ ⥤ C₂ ⥤ C
inst✝⁵ : (F.obj c₁.pt).PreservesZeroMorphisms
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)
inst✝² : PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)
inst✝¹ : HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)
s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))
l : (c₁.map (F.flip.obj Y₂)).pt ⟶ s.pt
hl : Cofork.π (c₁.map (F.flip.obj Y₂)) ≫ l = Cofork.π s
this : (F.map (Cofork.π c₁)).app X₂ ≫ (F.obj c₁.pt).map f₂ ≫ l = coprod.inr ≫ 0
⊢ (F.obj c₁.pt).map f₂ ≫ l = 0 ≫ l