awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
X : FreeGroupoid.{v, u} C
⊢ NatTrans.app (Iso.hom (mapId C)) X = 𝟙 X

Tactic:
liftNatIso_hom_app ..

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_hom_app, Quiver.FreeGroupoid
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
X : FreeGroupoid.{v, u} C
⊢ NatTrans.app (Iso.inv (mapId C)) X = 𝟙 X

Tactic:
liftNatIso_inv_app ..

Premises used: CategoryTheory.FreeGroupoid, Quiver.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_inv_app
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
symm : Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (𝟭 (FreeGroupoid.{v, u} C)) (map (𝟭 C))
⊢ Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (map (𝟭 C)) (𝟭 (FreeGroupoid.{v, u} C))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
hΦ : Eq (α := C ⥤ FreeGroupoid.{v, u} C) (of C ⋙ 𝟭 (FreeGroupoid.{v, u} C)) (𝟭 C ⋙ of C)
⊢ Eq (α := FreeGroupoid.{v, u} C ⥤ FreeGroupoid.{v, u} C) (𝟭 (FreeGroupoid.{v, u} C)) (map (𝟭 C))

Tactic:
apply lift_unique

Premises used: CategoryTheory.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := C ⥤ FreeGroupoid.{v, u} C) (of C ⋙ 𝟭 (FreeGroupoid.{v, u} C)) (𝟭 C ⋙ of C)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
X : FreeGroupoid.{v, u} C
⊢ (mapComp φ φ').hom.app X = 𝟙 ((map (φ ⋙ φ')).obj X)

Tactic:
liftNatIso_hom_app ..

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_hom_app, Quiver.FreeGroupoid
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
X : FreeGroupoid.{v, u} C
⊢ (mapComp φ φ').inv.app X = 𝟙 ((map φ ⋙ map φ').obj X)

Tactic:
liftNatIso_inv_app ..

Premises used: CategoryTheory.FreeGroupoid, Quiver.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_inv_app
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
symm : map φ ⋙ map φ' = map (φ ⋙ φ')
⊢ map (φ ⋙ φ') = map φ ⋙ map φ'

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : of C ⋙ map φ ⋙ map φ' = (φ ⋙ φ') ⋙ of E
⊢ map φ ⋙ map φ' = map (φ ⋙ φ')

Tactic:
apply lift_unique

Premises used: CategoryTheory.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Category.{v₂, u₂} E
φ : Functor.{v, v₁, u, u₁} C D
φ' : Functor.{v₁, v₂, u₁, u₂} D E
⊢ of C ⋙ map φ ⋙ map φ' = (φ ⋙ φ') ⋙ of E

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
φ : Functor.{v, v₁, u, u₁} C D
X : C
⊢ (map φ).obj (mk X) = mk (φ.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
φ : Functor.{v, v₁, u, u₁} C D
X Y : C
f : X ⟶ Y
⊢ (map φ).map (homMk f) = homMk (φ.map f)

Tactic:
rfl

Premises used: Quiver.Hom.toPath, CategoryTheory.Quotient.comp, Quiver.Path.comp, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : of C ⋙ map F ⋙ lift G = F ⋙ G
⊢ map F ⋙ lift G = lift (F ⋙ G)

Tactic:
apply lift_unique

Premises used: CategoryTheory.FreeGroupoid.lift_unique
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
hΦ : (of C ⋙ map F) ⋙ lift G = F ⋙ G
hΦ₁ : (F ⋙ of D) ⋙ lift G = F ⋙ G
hΦ₂ : F ⋙ of D ⋙ lift G = F ⋙ G
hΦ₃ hΦ₄ : F ⋙ G = F ⋙ G
⊢ of C ⋙ map F ⋙ lift G = F ⋙ G

Tactic:
rw [← Functor.assoc, of_comp_map, Functor.assoc, lift_spec G]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.FreeGroupoid.of_comp_map, CategoryTheory.FreeGroupoid.lift_spec
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
X : FreeGroupoid.{v, u} C
⊢ (mapCompLift F G).hom.app X = 𝟙 ((map F ⋙ lift G).obj X)

Tactic:
liftNatIso_hom_app ..

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_hom_app, Quiver.FreeGroupoid
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
E : Type u₂
inst_2 : Groupoid.{v₂, u₂} E
F : Functor.{v, v₁, u, u₁} C D
G : Functor.{v₁, v₂, u₁, u₂} D E
X : FreeGroupoid.{v, u} C
⊢ (mapCompLift F G).inv.app X = 𝟙 ((lift (F ⋙ G)).obj X)

Tactic:
liftNatIso_inv_app ..

Premises used: CategoryTheory.FreeGroupoid, Quiver.FreeGroupoid, CategoryTheory.FreeGroupoid.liftNatIso_inv_app
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Cat
⊢ map (Cat.Hom.toFunctor (𝟙 C)) = 𝟙 (of (FreeGroupoid (↑C : Type u)))

Tactic:
simp [map_id, id_eq_id]

Premises used: CategoryTheory.FreeGroupoid.map_id, CategoryTheory.Grpd.id_eq_id
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : Cat
F : X ⟶ Y
G : Y ⟶ Z
⊢ map (F ≫ G).toFunctor = CategoryStruct.comp (Y := of (FreeGroupoid (↑Y : Type u))) (map F.toFunctor) (map G.toFunctor)

Tactic:
simp [Grpd.comp_eq_comp, map_comp]

Premises used: CategoryTheory.Grpd.comp_eq_comp, CategoryTheory.FreeGroupoid.map_comp
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Cat
⊢ (↑(free.obj C) : Type u) = FreeGroupoid (↑C : Type u)

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C D : Cat
F : C ⟶ D
⊢ free.map F = map F.toFunctor

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid.map, CategoryTheory.Quotient.lift, rfl, CategoryTheory.FreeGroupoid.lift
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{u, u} C
D : Type u
inst_1 : Groupoid D
F : FreeGroupoid C ⥤ D
⊢ Cat.Hom.toFunctor
      ((freeForgetAdjunction.homEquiv (Cat.of C) (of D) :
          (a : free.obj (Cat.of C) ⟶ of D) → Cat.of C ⟶ forgetToCat.obj (of D))
        F) =
    FreeGroupoid.of C ⋙ F

Tactic:
rfl

Premises used: CategoryTheory.Paths, CategoryTheory.Functor.comp, Quiver.Symmetrify, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{u, u} C
D : Type u
inst_1 : Groupoid D
F : C ⥤ D
⊢ (Equiv.symm (freeForgetAdjunction.homEquiv (Cat.of C) (of D)) :
        (a : Cat.of C ⟶ forgetToCat.obj (of D)) → free.obj (Cat.of C) ⟶ of D)
      F.toCatHom =
    map F ⋙ lift (𝟭 D)

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.Paths, CategoryTheory.Functor.comp, Quiver.Symmetrify, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
C : Type u
inst : Category.{u, u} C
⊢ Eq (α := (↑(Functor.obj (𝟭 Cat) (Cat.of C)) : Type u) ⥤ (↑((free ⋙ forgetToCat).obj (Cat.of C)) : Type u))
    (Cat.Hom.toFunctor (freeForgetAdjunction.unit.app (Cat.of C))) (FreeGroupoid.of C)

Tactic:
rfl

Premises used: CategoryTheory.FreeGroupoid, CategoryTheory.Paths, CategoryTheory.Functor.comp, Quiver.Symmetrify, CategoryTheory.FreeGroupoid.of, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
Goal:
D : Type u
inst : Groupoid D
⊢ Eq (α := (forgetToCat ⋙ free).obj (of D) ⟶ Functor.obj (𝟭 Grpd) (of D)) (freeForgetAdjunction.counit.app (of D))
    (lift (𝟭 D))

Tactic:
rfl

Premises used: CategoryTheory.Paths, Quiver.Symmetrify, CategoryTheory.Quotient.lift, rfl, CategoryTheory.FreeGroupoid.lift
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
⊢ (↑(of C) : Type u) = C

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
W X Y Z : Grpd
f : Functor.{v, v, u, u} (↑W : Type u) (↑X : Type u)
g : Functor.{v, v, u, u} (↑X : Type u) (↑Y : Type u)
h : Functor.{v, v, u, u} (↑Y : Type u) (↑Z : Type u)
⊢ (f ⋙ g) ⋙ h = f ⋙ g ⋙ h

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
C D E : Grpd
f : C ⟶ D
g : D ⟶ E
⊢ f ≫ g = f ⋙ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
C : Grpd
⊢ 𝟙 C = 𝟭 (↑C : Type u)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
j : J
⊢ CategoryStruct.comp (Y :=
      Limits.Cone.pt (J := Discrete J) (F := Discrete.functor F)
        (Limits.Fan.mk (of ((j : J) → (↑(F j) : Type u))) fun (j : J) ↦ Pi.eval (fun (j : J) ↦ (↑(F j) : Type u)) j))
      (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j)
      (Limits.Fan.proj
        (Limits.Fan.mk (of ((j : J) → (↑(F j) : Type u))) fun (j : J) ↦ Pi.eval (fun (j : J) ↦ (↑(F j) : Type u)) j)
        j) =
    s.proj j

Tactic:
simp [comp_eq_comp]

Premises used: CategoryTheory.Grpd.comp_eq_comp
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
h :
  ∀ (i : J),
    m ⋙ Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) i =
      Functor.comp (D := (i : J) → (↑(F i) : Type u))
        ((fun (s : Limits.Fan F) ↦
            (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
              (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
          s)
        (Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) i)
⊢ m =
    (fun (s : Limits.Fan F) ↦
        (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
          (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
      s

Tactic:
apply Functor.pi_ext

Premises used: CategoryTheory.Functor.pi_ext
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
j : J
⊢ m ≫ (piLimitFan F).proj j = s.proj j

Tactic:
specialize w j
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
j : J
w : m ≫ (piLimitFan F).proj j = s.proj j
⊢ m ⋙ Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) j =
    Functor.comp (D := (i : J) → (↑(F i) : Type u))
      ((fun (s : Limits.Fan F) ↦
          (Functor.pi' (C := fun (j : J) ↦ (↑(F j) : Type u)) fun (j : J) ↦ s.proj j :
            (↑s.pt : Type u) ⥤ ((i : J) → (↑(F i) : Type u))))
        s)
      (Pi.eval (fun (i : J) ↦ (↑(F i) : Type u)) j)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
⊢ {J : Type u} → (f : J → Grpd.{u, u}) → Limits.Fan f

Tactic:
apply piLimitFan

Premises used: CategoryTheory.Grpd.piLimitFan
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
⊢ {J : Type u} → (f : J → Grpd.{u, u}) → Limits.IsLimit (piLimitFan f)

Tactic:
apply piLimitFanIsLimit

Premises used: CategoryTheory.Grpd.piLimitFanIsLimit
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
f : J → Grpd
j : J
simp : (piLimitFan f).π.app { as := j } = Pi.eval (fun (i : J) ↦ (↑(f i) : Type u)) j
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun (i : J) ↦ (↑(f i) : Type u)) j

Tactic:
simp [piIsoPi]

Premises used: CategoryTheory.Grpd.piIsoPi
-- Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic
Goal:
J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun (i : J) ↦ (↑(f i) : Type u)) j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
mp : Groupoid.inv f ∈ S.arrows d c → f ∈ S.arrows c d
mpr : f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c
⊢ Groupoid.inv f ∈ S.arrows d c ↔ f ∈ S.arrows c d

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
h : Groupoid.inv f ∈ S.arrows d c
⊢ f ∈ S.arrows c d

Tactic:
simpa only [inv_eq_inv, IsIso.inv_inv] using S.inv h

Premises used: CategoryTheory.IsIso.inv_inv, CategoryTheory.Subgroupoid.inv, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
⊢ f ∈ S.arrows c d → Groupoid.inv f ∈ S.arrows d c

Tactic:
apply S.inv

Premises used: CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
mp : f ≫ g ∈ S.arrows c e → g ∈ S.arrows d e
mpr : g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e
⊢ f ≫ g ∈ S.arrows c e ↔ g ∈ S.arrows d e

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
this : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e

Tactic:
simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this

Premises used: CategoryTheory.IsIso.inv_hom_id_assoc, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
mp : Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e
⊢ g ∈ S.arrows d e

Tactic:
suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
      simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
h : f ≫ g ∈ S.arrows c e
⊢ Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e

Tactic:
apply S.mul (S.inv hf) h

Premises used: CategoryTheory.Subgroupoid.mul, CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hf : f ∈ S.arrows c d
⊢ g ∈ S.arrows d e → f ≫ g ∈ S.arrows c e

Tactic:
apply S.mul hf

Premises used: CategoryTheory.Subgroupoid.mul
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
mp : f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d
mpr : f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e
⊢ f ≫ g ∈ S.arrows c e ↔ f ∈ S.arrows c d

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
this : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
mp : (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d
⊢ f ∈ S.arrows c d

Tactic:
suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
h : f ≫ g ∈ S.arrows c e
⊢ (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d

Tactic:
apply S.mul h (S.inv hg)

Premises used: CategoryTheory.Subgroupoid.mul, CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
fun hf => S.mul hf hg

Premises used: CategoryTheory.Subgroupoid.mul
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ∈ S.arrows c d → f ≫ g ∈ S.arrows c e

Tactic:
exact fun hf => S.mul hf hg

Premises used: CategoryTheory.Subgroupoid.mul
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
h : f ∈ S.arrows c d
⊢ c ∈ S.objs

Tactic:
⟨f ≫ Groupoid.inv f, S.mul h (S.inv h)⟩

Premises used: CategoryTheory.Subgroupoid.mul, Set.Mem, setOf, CategoryTheory.Groupoid.inv, Set.Nonempty, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Subgroupoid.inv, CategoryTheory.Subgroupoid.objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
h : f ∈ S.arrows c d
⊢ d ∈ S.objs

Tactic:
⟨Groupoid.inv f ≫ f, S.mul (S.inv h) h⟩

Premises used: CategoryTheory.Subgroupoid.mul, Set.Mem, setOf, CategoryTheory.Groupoid.inv, Set.Nonempty, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Subgroupoid.inv, CategoryTheory.Subgroupoid.objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ γ ≫ Groupoid.inv γ ∈ S.arrows c c

Tactic:
S.mul hγ (S.inv hγ)

Premises used: CategoryTheory.Subgroupoid.mul, CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
h : 𝟙 c = γ ≫ Groupoid.inv γ
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
convert! S.mul hγ (S.inv hγ)

Premises used: CategoryTheory.Subgroupoid.mul, CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c = γ ≫ Groupoid.inv γ

Tactic:
simp only [inv_eq_inv, IsIso.hom_inv_id]

Premises used: CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
h : f ∈ S.arrows c d
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
id_mem_of_nonempty_isotropy S c (mem_objs_of_src S h)

Premises used: CategoryTheory.Subgroupoid.mem_objs_of_src, CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
f : c ⟶ d
h : f ∈ S.arrows c d
⊢ 𝟙 d ∈ S.arrows d d

Tactic:
id_mem_of_nonempty_isotropy S d (mem_objs_of_tgt S h)

Premises used: CategoryTheory.Subgroupoid.id_mem_of_nonempty_isotropy, CategoryTheory.Subgroupoid.mem_objs_of_tgt
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : (↑S.objs : Type u)
p : c ⟶ d
⊢ (↑(inv p) : (↑d : C) ⟶ (↑c : C)) = inv (↑p : (↑c : C) ⟶ (↑d : C))

Tactic:
simp only [← inv_eq_inv, coe_inv_coe]

Premises used: CategoryTheory.Subgroupoid.coe_inv_coe, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd :
  S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) =
    S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd)
simp : c = d
⊢ Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc = Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd

Tactic:
simp only [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd :
  S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) =
    S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd)
⊢ c = d

Tactic:
hcd
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd :
  S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) =
    S.hom.obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd)
⊢ c = d

Tactic:
exact hcd
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 x x_1 : Subgroupoid.{u, u_1} C
S : (c d : C) → Set (c ⟶ d)
inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ S c d → Groupoid.inv p ∈ S d c
mul : ∀ {c d e : C} {p : c ⟶ d}, p ∈ S c d → ∀ {q : d ⟶ e}, q ∈ S d e → p ≫ q ∈ S c e
T : (c d : C) → Set (c ⟶ d)
inv_1 : ∀ {c d : C} {p : c ⟶ d}, p ∈ T c d → Groupoid.inv p ∈ T d c
mul_1 : ∀ {c d e : C} {p : c ⟶ d}, p ∈ T c d → ∀ {q : d ⟶ e}, q ∈ T d e → p ≫ q ∈ T c e
h :
  (↑{ arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C } : Set ((c : C) × (d : C) × (c ⟶ d))) =
    (↑{ arrows := T, inv := @inv_1, mul := @mul_1 } : Set ((c : C) × (d : C) × (c ⟶ d)))
arrows :
  ∀ (c d : C) (f : c ⟶ d),
    f ∈ { arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C }.arrows c d ↔
      f ∈ { arrows := T, inv := @inv_1, mul := @mul_1 : Subgroupoid.{u, u_1} C }.arrows c d
⊢ { arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C } = { arrows := T, inv := @inv_1, mul := @mul_1 }

Tactic:
ext c d f
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 x x_1 : Subgroupoid.{u, u_1} C
S : (c d : C) → Set (c ⟶ d)
inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ S c d → Groupoid.inv p ∈ S d c
mul : ∀ {c d e : C} {p : c ⟶ d}, p ∈ S c d → ∀ {q : d ⟶ e}, q ∈ S d e → p ≫ q ∈ S c e
T : (c d : C) → Set (c ⟶ d)
inv_1 : ∀ {c d : C} {p : c ⟶ d}, p ∈ T c d → Groupoid.inv p ∈ T d c
mul_1 : ∀ {c d e : C} {p : c ⟶ d}, p ∈ T c d → ∀ {q : d ⟶ e}, q ∈ T d e → p ≫ q ∈ T c e
h :
  (↑{ arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C } : Set ((c : C) × (d : C) × (c ⟶ d))) =
    (↑{ arrows := T, inv := @inv_1, mul := @mul_1 } : Set ((c : C) × (d : C) × (c ⟶ d)))
c d : C
f : c ⟶ d
⊢ f ∈ { arrows := S, inv := @inv, mul := @mul : Subgroupoid.{u, u_1} C }.arrows c d ↔
    f ∈ { arrows := T, inv := @inv_1, mul := @mul_1 : Subgroupoid.{u, u_1} C }.arrows c d

Tactic:
apply Set.ext_iff.1 h ⟨c, d, f⟩

Premises used: Iff.mp, Set.ext_iff, Sigma.mk