awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ

Tactic:
simp only [inv_eq_inv, Category.assoc, IsIso.inv_hom_id, Category.comp_id,
      IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, 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
⊢ IsNormal.{u, u_1} (C := C) ⊤

Tactic:
{ wide := fun _ => trivial
    conj := fun _ _ _ => trivial }

Premises used: trivial, CategoryTheory.Subgroupoid.IsNormal.mk, CategoryTheory.Subgroupoid.IsWide.mk
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
simp_rw : ∀ (c : C) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), 𝟙 c ∈ i.arrows c c
⊢ ∀ (c : C), 𝟙 c ∈ (sInf s).arrows c c

Tactic:
simp_rw [sInf, mem_iInter₂]

Premises used: Set.mem_iInter₂, InfSet.sInf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), 𝟙 c ∈ i.arrows c c

Tactic:
fun c S Ss => (sn S Ss).wide c

Premises used: CategoryTheory.Subgroupoid.IsNormal.toIsWide, CategoryTheory.Subgroupoid.IsWide.wide
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ (c : C) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), 𝟙 c ∈ i.arrows c c

Tactic:
exact fun c S Ss => (sn S Ss).wide c

Premises used: CategoryTheory.Subgroupoid.IsNormal.toIsWide, CategoryTheory.Subgroupoid.IsWide.wide
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
simp_rw :
  ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
    (∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), γ ∈ i.arrows c c) →
      ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c}, γ ∈ (sInf s).arrows c c → Groupoid.inv p ≫ γ ≫ p ∈ (sInf s).arrows d d

Tactic:
simp_rw [sInf, mem_iInter₂]

Premises used: Set.mem_iInter₂, InfSet.sInf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
c d : C
⊢ ∀ (p : c ⟶ d) {γ : c ⟶ c},
    (∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), γ ∈ i.arrows c c) →
      ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d

Tactic:
fun p γ hγ S Ss => (sn S Ss).conj p (hγ S Ss)

Premises used: CategoryTheory.Subgroupoid.IsNormal.conj
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
sn : ∀ S ∈ s, S.IsNormal
⊢ ∀ {c d : C} (p : c ⟶ d) {γ : c ⟶ c},
    (∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), γ ∈ i.arrows c c) →
      ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), Groupoid.inv p ≫ γ ≫ p ∈ i.arrows d d

Tactic:
exact fun p γ hγ S Ss => (sn S Ss).conj p (hγ S Ss)

Premises used: CategoryTheory.Subgroupoid.IsNormal.conj
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c : C
⊢ Membership.mem (γ := Set (c ⟶ c)) (arrows discrete c c) (𝟙 c)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : Membership.mem (γ := Set (c ⟶ c)) (arrows discrete c c) γ
id : Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ 𝟙 c ≫ f)
⊢ Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ γ ≫ f)

Tactic:
cases hγ
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
id : Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (𝟙 d)
⊢ Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (Groupoid.inv f ≫ 𝟙 c ≫ f)

Tactic:
simp only [inv_eq_inv, Category.id_comp, IsIso.inv_hom_id]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Groupoid.inv_eq_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
⊢ Membership.mem (γ := Set (d ⟶ d)) (arrows discrete d d) (𝟙 d)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
rw : y * (x * y⁻¹) ∈ S.vertexSubgroup cS
⊢ y * x * y⁻¹ ∈ S.vertexSubgroup cS

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * (x * y⁻¹) ∈ S.vertexSubgroup cS

Tactic:
Sn.conj' y hx

Premises used: Set.Mem, CategoryTheory.Subgroupoid.IsNormal.conj'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * (x * y⁻¹) ∈ S.vertexSubgroup cS

Tactic:
exact Sn.conj' y hx

Premises used: CategoryTheory.Subgroupoid.IsNormal.conj'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
c d : C
simp :
  ∀ (i : Subgroupoid.{u, u_1} C)
    (j :
      Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
        {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d} i),
    X c d ⊆ i.arrows c d
⊢ X c d ⊆
    ⋂ (S : Subgroupoid.{u, u_1} C),
      ⋂ (_ :
        Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
          {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d} S),
        S.arrows c d

Tactic:
simp only [subset_iInter₂_iff]

Premises used: Set.subset_iInter₂_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ (i : Subgroupoid.{u, u_1} C)
    (j :
      Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
        {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d} i),
    X c d ⊆ i.arrows c d

Tactic:
fun S hS f fS => hS _ _ fS

Premises used: Set.Subset
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ (i : Subgroupoid.{u, u_1} C)
    (j :
      Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
        {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d} i),
    X c d ⊆ i.arrows c d

Tactic:
exact fun S hS f fS => hS _ _ fS
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
h :
  Subset (α := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}
    {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d}
⊢ generated X ≤ generatedNormal X

Tactic:
apply @sInf_le_sInf (Subgroupoid C) _

Premises used: sInf_le_sInf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
⊢ Subset (α := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}
    {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d}

Tactic:
fun S ⟨h, _⟩ => h

Premises used: _private.0.CategoryTheory.Subgroupoid.generated_le_generatedNormal.match_1, setOf, Membership.mem, Set.Subset
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
⊢ Subset (α := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal}
    {S : Subgroupoid.{u, u_1} C | ∀ (c d : C), X c d ⊆ S.arrows c d}

Tactic:
exact fun S ⟨h, _⟩ => h
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
⊢ (generatedNormal X).IsNormal

Tactic:
sInf_isNormal _ fun _ h => h.right

Premises used: CategoryTheory.Subgroupoid.generatedNormal, And.right, CategoryTheory.Subgroupoid.sInf_isNormal
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
mp : generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d
mpr : (∀ (c d : C), X c d ⊆ S.arrows c d) → generatedNormal X ≤ S
⊢ generatedNormal X ≤ S ↔ ∀ (c d : C), X c d ⊆ S.arrows c d

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
⊢ generated X ≤ generatedNormal X

Tactic:
have h' := generated_le_generatedNormal X
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
h' : generated X ≤ generatedNormal X
mp :
  ∀ (h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d) (c d : C)
    (h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d), X c d ⊆ S.arrows c d
⊢ X c d ⊆ S.arrows c d

Tactic:
rw [le_iff] at h h'

Premises used: CategoryTheory.Subgroupoid.le_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d

Tactic:
((subset_generated X c d).trans (@h' c d)).trans (@h c d)

Premises used: HasSubset.Subset.trans, CategoryTheory.Subgroupoid.subset_generated
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d

Tactic:
exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d)

Premises used: HasSubset.Subset.trans, CategoryTheory.Subgroupoid.subset_generated
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
mpr :
  Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} S
⊢ generatedNormal X ≤ S

Tactic:
apply @sInf_le (Subgroupoid C) _

Premises used: sInf_le
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} S

Tactic:
⟨h, Sn⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
h : ∀ (c d : C), X c d ⊆ S.arrows c d
⊢ Membership.mem (γ := Set (Subgroupoid.{u, u_1} C))
    {S : Subgroupoid.{u, u_1} C | (∀ (c d : C), X c d ⊆ S.arrows c d) ∧ S.IsNormal} S

Tactic:
exact ⟨h, Sn⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d : C
p : c ⟶ d
hp :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
rw : Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (Groupoid.inv (φ.map p))
⊢ Membership.mem (γ := Set (d ⟶ c))
    {f : d ⟶ c | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (φ.map f)}
    (Groupoid.inv p)

Tactic:
rw [mem_setOf, inv_eq_inv, φ.map_inv, ← inv_eq_inv]

Premises used: CategoryTheory.Functor.map_inv, Set.mem_setOf, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d : C
p : c ⟶ d
hp :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
⊢ Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (Groupoid.inv (φ.map p))

Tactic:
S.inv hp

Premises used: CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d : C
p : c ⟶ d
hp :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
⊢ Membership.mem (γ := Set (φ.obj d ⟶ φ.obj c)) (S.arrows (φ.obj d) (φ.obj c)) (Groupoid.inv (φ.map p))

Tactic:
exact S.inv hp

Premises used: CategoryTheory.Subgroupoid.inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
simp : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map p ≫ φ.map q)
⊢ Membership.mem (γ := Set (c ⟶ e))
    {f : c ⟶ e | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map f)} (p ≫ q)

Tactic:
simp only [mem_setOf, Functor.map_comp]

Premises used: Set.mem_setOf, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
a : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map p)
a₁ : Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map q)
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj e)) (S.arrows (φ.obj c) (φ.obj e)) (φ.map p ≫ φ.map q)

Tactic:
apply S.mul

Premises used: CategoryTheory.Subgroupoid.mul
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map p)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S_1 : Subgroupoid.{u, u_2} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
S : Subgroupoid.{u_1, u_3} D
c d e : C
p : c ⟶ d
h :
  Membership.mem (γ := Set (c ⟶ d))
    {f : c ⟶ d | Membership.mem (γ := Set (φ.obj c ⟶ φ.obj d)) (S.arrows (φ.obj c) (φ.obj d)) (φ.map f)} p
q : d ⟶ e
h_1 :
  Membership.mem (γ := Set (d ⟶ e))
    {f : d ⟶ e | Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map f)} q
⊢ Membership.mem (γ := Set (φ.obj d ⟶ φ.obj e)) (S.arrows (φ.obj d) (φ.obj e)) (φ.map q)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S T : Subgroupoid.{u_1, u_2} D
⊢ S ≤ T → comap φ S ≤ comap φ T

Tactic:
fun ST _ =>
  @ST ⟨_, _, _⟩

Premises used: Set.Mem, setOf, CategoryTheory.Subgroupoid.comap, CategoryTheory.Subgroupoid.toSet
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c : C
rw : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c)) (S.arrows (φ.obj c) (φ.obj c)) (𝟙 (φ.obj c))
⊢ 𝟙 c ∈ (comap φ S).arrows c c

Tactic:
rw [comap, mem_setOf, Functor.map_id]

Premises used: CategoryTheory.Subgroupoid.comap, Set.mem_setOf, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c : C
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c)) (S.arrows (φ.obj c) (φ.obj c)) (𝟙 (φ.obj c))

Tactic:
apply Sn.wide

Premises used: CategoryTheory.Subgroupoid.IsNormal.toIsWide, CategoryTheory.Subgroupoid.IsWide.wide
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : γ ∈ (comap φ S).arrows c c
simp_rw :
  Membership.mem (γ := Set (φ.obj d ⟶ φ.obj d)) (S.arrows (φ.obj d) (φ.obj d))
    (Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
⊢ Groupoid.inv f ≫ γ ≫ f ∈ (comap φ S).arrows d d

Tactic:
simp_rw [inv_eq_inv f, comap, mem_setOf, Functor.map_comp, Functor.map_inv, ← inv_eq_inv]

Premises used: CategoryTheory.Subgroupoid.comap, CategoryTheory.Functor.map_inv, Set.mem_setOf, CategoryTheory.Functor.map_comp, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : γ ∈ (comap φ S).arrows c c
⊢ Membership.mem (γ := Set (φ.obj d ⟶ φ.obj d)) (S.arrows (φ.obj d) (φ.obj d))
    (Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
Sn.conj _ hγ

Premises used: CategoryTheory.Subgroupoid.IsNormal.conj
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_3, u} C
D : Type u_1
inst_1 : Groupoid.{u_2, u_1} D
φ : Functor.{u_3, u_2, u, u_1} C D
S : Subgroupoid.{u_1, u_2} D
Sn : S.IsNormal
c d : C
f : c ⟶ d
γ : c ⟶ c
hγ : γ ∈ (comap φ S).arrows c c
⊢ Membership.mem (γ := Set (φ.obj d ⟶ φ.obj d)) (S.arrows (φ.obj d) (φ.obj d))
    (Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
exact Sn.conj _ hγ

Premises used: CategoryTheory.Subgroupoid.IsNormal.conj
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_5, u} C
D : Type u_1
inst_1 : Groupoid.{u_4, u_1} D
φ : Functor.{u_5, u_4, u, u_1} C D
E : Type u_2
inst_2 : Groupoid.{u_3, u_2} E
ψ : Functor.{u_4, u_3, u_1, u_2} D E
⊢ comap (φ ⋙ ψ) = comap φ ∘ comap ψ

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Subgroupoid.comap, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
c d : C
f : c ⟶ d
⊢ f ∈ (ker φ).arrows c d ↔ ∃ (h : φ.obj c = φ.obj d), φ.map f = eqToHom h

Tactic:
mem_discrete_iff (φ.map f)

Premises used: Set.Mem, setOf, CategoryTheory.Subgroupoid.mem_discrete_iff, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
⊢ (ker φ).IsNormal

Tactic:
isNormal_comap φ discrete_isNormal

Premises used: CategoryTheory.Subgroupoid.discrete_isNormal, CategoryTheory.Subgroupoid.ker, CategoryTheory.Subgroupoid.isNormal_comap
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_5, u} C
D : Type u_1
inst_1 : Groupoid.{u_4, u_1} D
φ : Functor.{u_5, u_4, u, u_1} C D
E : Type u_2
inst_2 : Groupoid.{u_3, u_2} E
ψ : Functor.{u_4, u_3, u_1, u_2} D E
⊢ ker (φ ⋙ ψ) = comap φ (ker ψ)

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Functor.comp, CategoryTheory.Subgroupoid.comap, CategoryTheory.Subgroupoid.ker, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
f : c ⟶ d
mp :
  Arrows φ hφ S c d f →
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
mpr :
  (∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb) →
    Arrows φ hφ S c d f
⊢ Arrows φ hφ S c d f ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
      f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
g : c_1 ⟶ d_1
hg : g ∈ S.arrows c_1 d_1
⊢ ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c_1) (hb : φ.obj b = φ.obj d_1) (_ : g_1 ∈ S.arrows a b),
    φ.map g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb

Tactic:
⟨_, _, g, rfl, rfl, hg, eq_conj_eqToHom _⟩

Premises used: CategoryTheory.eq_conj_eqToHom, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
g : c_1 ⟶ d_1
hg : g ∈ S.arrows c_1 d_1
⊢ ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c_1) (hb : φ.obj b = φ.obj d_1) (_ : g_1 ∈ S.arrows a b),
    φ.map g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb

Tactic:
exact ⟨_, _, g, rfl, rfl, hg, eq_conj_eqToHom _⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
D : Type u_1
inst_1 : Groupoid.{u_3, u_1} D
φ : Functor.{u_2, u_3, u, u_1} C D
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
mpr : Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)

Tactic:
rw [← eq_conj_eqToHom]

Premises used: CategoryTheory.eq_conj_eqToHom