mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : Y.HasTensor Z
inst✝² : Z.HasTensor Y
inst✝¹ : X.HasTensor Z
inst✝ : Z.HasTensor X
f : X ⟶ Y
⊢ whiskerRight f Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ whiskerLeft Z f

Tactic:
by

Goal state after:
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
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
x : (i : ι) → (F.obj (X i)).obj := fun i ↦ ⋯.some
P : C := ∏ᶜ X
is₁ : F.obj P ≅ ∏ᶜ fun i ↦ F.obj (X i) := PreservesProduct.iso F X
is₂ : (∏ᶜ fun i ↦ F.obj (X i)).obj ≃ ((i : ι) → (F.obj (X i)).obj) := FintypeCat.productEquiv fun i ↦ F.obj (X i)
px : (F.obj P).obj := (ConcreteCategory.hom is₁.inv) (is₂.symm x)
i : ι
⊢ (ConcreteCategory.hom (F.map (Pi.π X i))) px = x i

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h✝ : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
h : ⟦μ * ↑σ⁻¹⟧ = ⟦μ⟧
⊢ (ConcreteCategory.hom
        (u.inv ≫
            (functorToAction F).map ((quotientDiag V h✝ u).map ⟦σ⟧) ≫
              u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV).hom)
      ⟦μ⟧ =
    (ConcreteCategory.hom (quotientToQuotientOfLE (↑V) (↑U) hUinV).hom) ⟦μ⟧

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
⊢ ∀ (a : ↥↑V ⧸ (↑U).subgroupOf ↑V),
    (quotientDiag V h u ⋙ functorToAction F).map a ≫ u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV =
      (u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV) ≫
        ((const (SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V))).obj (ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑V)))).map a

Tactic:
by

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
⊢ i₂ + i₃ + i₁ = k

Tactic:
by

Goal state after:
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
inst✝³ : GaloisCategory C
inst✝² : FiberFunctor F
t : Aut F
ι : Type u_2
inst✝¹ : Finite ι
X : ι → C
inst✝ : ∀ (i : ι), IsGalois (X i)
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
⊢ ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (ConcreteCategory.hom (t.hom.app (X i))) x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
J' : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V) ⥤ Action FintypeCat (Aut F) := quotientDiag V h u ⋙ functorToAction F
m : End (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)) := ⟦⟨σ⁻¹ * τ, ⋯⟩⟧
h1 :
  J'.map m ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)) = s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))
⊢ (ConcreteCategory.hom (J'.map m).hom) ((ConcreteCategory.hom u.inv.hom) ⟦τ⟧) = (ConcreteCategory.hom u.inv.hom) ⟦σ⟧

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
σ τ : Aut F
hst : σ ≈ τ
⊢ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧ =
    (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦τ⟧

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
V : Type u_1
inst✝¹ : Quiver V
inst✝ : Nonempty V
⊢ Nonempty (Quiver.FreeGroupoid V)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
⊢ HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)

Tactic:
by

Goal state after:
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ c.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p q : X ⟶ Y
⊢ HomRel.CompClosure redStep p q → HomRel.CompClosure redStep (Path.reverse p) (Path.reverse q)

Tactic:
by

Goal state after:
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
g : G
hg : g ∈ c
X : C
x✝ : IsGalois X
x : (F.obj X).obj
⊢ g ∈ gi { obj := X, pt := x, isGalois := ⋯ } • ↑(MulAction.stabilizer G x)

Tactic:
by

Goal state after:
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
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
⊢ Function.Surjective ⇑(toAut F G)

Tactic:
by

Goal state after:
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
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
⊢ ∃ g, g • x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: 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)
⊢ HomRel.CompClosure redStep (q ≫ 𝟙 b✝ ≫ q.reverse) (q ≫ (f.toPath ≫ (reverse f).toPath) ≫ q.reverse)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝³ : GaloisCategory C
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : FiberFunctor F
g : Aut F
h : ∀ (X : C) (x : (F.obj X).obj), g • x = x
⊢ g = 1

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ IsHomeomorph ⇑(toAut F G)

Tactic:
isHomeomorph_iff_continuous_bijective

Goal state after:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ Continuous ⇑(toAut F G) ∧ Function.Bijective ⇑(toAut F G)
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).obj
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ IsHomeomorph ⇑(toAut F G)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
g : Aut F
⊢ (coconeQuotientDiag h u hUinV).pt.ρ g ≫
      FintypeCat.homMk
        (Quotient.lift
          (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧) ⋯) =
    FintypeCat.homMk
        (Quotient.lift
          (fun σ ↦ (ConcreteCategory.hom (u.inv ≫ s.ι.app (SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V))).hom) ⟦σ⟧) ⋯) ≫
      s.pt.ρ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ x✝ : C
h : (of C).obj x✝¹ = (of C).obj x✝
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
r : homRel C f g
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
E : Type u₂
inst✝ : Groupoid E
φ : C ⥤ E
X Y : C
f : X ⟶ Y
⊢ (lift φ).map (homMk f) = φ.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
Φ : FreeGroupoid C ⥤ G
hΦ : of C ⋙ Φ = φ
⊢ Φ = lift φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

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

Tactic:
by

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
⊢ i₂ + i₁ + i₃ = k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (p ≫ Path.reverse p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 X)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
p : X ⟶ Y
⊢ Quot.mk (HomRel.CompClosure redStep) (Path.reverse p ≫ p) = Quot.mk (HomRel.CompClosure redStep) (𝟙 Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G✝ : Type u₁
inst✝ : Groupoid G✝
F G : FreeGroupoid C ⥤ G✝
h : of C ⋙ F = of C ⋙ G
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
F₁ F₂ : FreeGroupoid C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).hom.app (mk X) = τ.hom.app X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
F₁ F₂ : FreeGroupoid C ⥤ G
τ : of C ⋙ F₁ ≅ of C ⋙ F₂
X : C
⊢ (liftNatIso F₁ F₂ τ).inv.app (mk X) = τ.inv.app X

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)
⊢ (coconeQuotientDiag h u hUinV).ι.app j ≫ coconeQuotientDiagDesc h u hUinV s = s.ι.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

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

Tactic:
by

Goal state after:
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)) (f₁ f₂ : x ⟶ y),
    redStep f₁ f₂ → (Paths.lift (Symmetrify.lift φ)).map f₁ = (Paths.lift (Symmetrify.lift φ)).map f₂

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

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

Tactic:
by

Goal state after:
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✝ : Groupoid E
F : C ⥤ D
G : D ⥤ E
⊢ map F ⋙ lift G = lift (F ⋙ G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C✝ : Type u
inst✝ : Category.{v, u} C✝
C : Cat
⊢ map (𝟙 C).toFunctor = 𝟙 (of (FreeGroupoid ↑C))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ Z✝ : Cat
F : X✝ ⟶ Y✝
G : Y✝ ⟶ Z✝
⊢ map (F ≫ G).toFunctor = map F.toFunctor ≫ map G.toFunctor

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ : c ⟶ c
⊢ (fun δ ↦ f ≫ δ ≫ inv f) ((fun γ ↦ inv f ≫ γ ≫ f) γ) = γ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
δ : d ⟶ d
⊢ (fun γ ↦ inv f ≫ γ ≫ f) ((fun δ ↦ f ≫ δ ≫ inv f) δ) = δ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.VertexGroup

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c d : C
f : c ⟶ d
γ₁ γ₂ : c ⟶ c
⊢ inv f ≫ (γ₁ * γ₂) ≫ f = inv f ≫ γ₁ ≫ f * inv f ≫ γ₂ ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
s : Cocone (quotientDiag V h u ⋙ functorToAction F)
f : (coconeQuotientDiag h u hUinV).pt ⟶ s.pt
hf : ∀ (j : SingleObj (↥↑V ⧸ (↑U).subgroupOf ↑V)), (coconeQuotientDiag h u hUinV).ι.app j ≫ f = s.ι.app j
⊢ f = coconeQuotientDiagDesc h u hUinV s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
Φ : Quiver.FreeGroupoid V ⥤ V'
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

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

Tactic:
by

Goal state after:
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''
⊢ freeGroupoidFunctor (φ ⋙q φ') = freeGroupoidFunctor φ ⋙ freeGroupoidFunctor φ'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
⊢ (prod.lift
          (have this := W.hom;
          this)
          g ≫
        inv (prodComparison F X Z)) ≫
      ((Over.post F).obj (Over.mk prod.fst)).hom =
    W.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
⊢ (Over.forget (F.obj X)).map
        (Over.homMk
          (prod.lift
              (have this := W.hom;
              this)
              g ≫
            inv (prodComparison F X Z))
          ⋯) ≫
      (TwoSquare.overPost F X).app (Over.mk prod.fst) ≫ F.map prod.snd =
    g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.snd =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.snd

Tactic:
simpa [← Functor.map_comp, P] using CostructuredArrow.w Q.hom

Goal state after: