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
F : (c : C) × (d : C) × (c ⟶ d)
⊢ F ∈ S ↔
    Membership.mem (γ :=
      Set
        (F.fst (β := fun (c : C) ↦ (d : C) × (c ⟶ d)) ⟶
          F.snd (β := fun (c : C) ↦ (d : C) × (c ⟶ d)).fst (β := fun (d : C) ↦
            F.fst (β := fun (c : C) ↦ (d : C) × (c ⟶ d)) ⟶ d)))
      (S.arrows (F.fst (β := fun (c : C) ↦ (d : C) × (c ⟶ d)))
        (F.snd (β := fun (c : C) ↦ (d : C) × (c ⟶ d)).fst (β := fun (d : C) ↦
          F.fst (β := fun (c : C) ↦ (d : C) × (c ⟶ d)) ⟶ d)))
      (F.snd (β := fun (c : C) ↦ (d : C) × (c ⟶ d)).snd (β := fun (d : C) ↦
        F.fst (β := fun (c : C) ↦ (d : C) × (c ⟶ d)) ⟶ d))

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, CategoryTheory.Subgroupoid.toSet
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
rw :
  (∀ (a : C) (b : (d : C) × (a ⟶ d)),
      Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ S →
        Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ T) ↔
    ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d
⊢ S ≤ T ↔ ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
rw [SetLike.le_def, Sigma.forall]

Premises used: SetLike.le_def, Sigma.forall
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)),
      Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ S →
        Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ T) ↔
    ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
forall_congr' fun c => Sigma.forall

Premises used: Sigma.forall, forall_congr'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
⊢ (∀ (a : C) (b : (d : C) × (a ⟶ d)),
      Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ S →
        Sigma.mk (β := fun (a : C) ↦ (d : C) × (a ⟶ d)) a b ∈ T) ↔
    ∀ {c d : C}, S.arrows c d ⊆ T.arrows c d

Tactic:
exact forall_congr' fun c => Sigma.forall

Premises used: Sigma.forall, forall_congr'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
p : c ⟶ d
h : Membership.mem (γ := Set (c ⟶ d)) univ p
⊢ Membership.mem (γ := Set (d ⟶ c)) univ (Groupoid.inv p)

Tactic:
trivial
-- 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
p : c ⟶ d
h : Membership.mem (γ := Set (c ⟶ d)) univ p
q : d ⟶ e
h_1 : Membership.mem (γ := Set (d ⟶ e)) univ q
⊢ Membership.mem (γ := Set (c ⟶ e)) univ (p ≫ q)

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
f : c ⟶ d
⊢ Membership.mem (γ := Set (c ⟶ d)) (arrows ⊤ c d) f

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c : C
⊢ Set.Nonempty.{u_1} (α := c ⟶ c) univ

Tactic:
simp only [univ_nonempty]

Premises used: Set.univ_nonempty
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
c d : C
p : c ⟶ d
hp : Membership.mem (γ := Set (c ⟶ d)) (⋂ S ∈ s, S.arrows c d) p
rw :
  ∀ (hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s),
    Groupoid.inv p ∈ i.arrows d c
⊢ Membership.mem (γ := Set (d ⟶ c)) (⋂ S ∈ s, S.arrows d c) (Groupoid.inv p)

Tactic:
rw [mem_iInter₂] at hp ⊢

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

Tactic:
fun S hS => S.inv (hp S hS)

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
s : Set (Subgroupoid.{u, u_1} C)
c d : C
p : c ⟶ d
hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d
⊢ ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), Groupoid.inv p ∈ i.arrows d c

Tactic:
exact fun S hS => S.inv (hp S hS)
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
c d e : C
p : c ⟶ d
hp : Membership.mem (γ := Set (c ⟶ d)) (⋂ S ∈ s, S.arrows c d) p
x : d ⟶ e
hq : Membership.mem (γ := Set (d ⟶ e)) (⋂ S ∈ s, S.arrows d e) x
rw :
  ∀ (hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d) (x : d ⟶ e)
    (hq : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), x ∈ i.arrows d e) (i : Subgroupoid.{u, u_1} C) (j : i ∈ s),
    p ≫ x ∈ i.arrows c e
⊢ Membership.mem (γ := Set (c ⟶ e)) (⋂ S ∈ s, S.arrows c e) (p ≫ x)

Tactic:
rw [mem_iInter₂] at hp hq ⊢

Premises used: Set.mem_iInter₂
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
c d e : C
p : c ⟶ d
hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d
x : d ⟶ e
hq : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), x ∈ i.arrows d e
⊢ ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ≫ x ∈ i.arrows c e

Tactic:
fun S hS => S.mul (hp S hS) (hq S hS)

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
s : Set (Subgroupoid.{u, u_1} C)
c d e : C
p : c ⟶ d
hp : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ∈ i.arrows c d
x : d ⟶ e
hq : ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), x ∈ i.arrows d e
⊢ ∀ (i : Subgroupoid.{u, u_1} C) (j : i ∈ s), p ≫ x ∈ i.arrows c e

Tactic:
exact fun S hS => S.mul (hp S hS) (hq S hS)
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
c d : C
p : c ⟶ d
⊢ p ∈ (sInf s).arrows c d ↔ ∀ S ∈ s, p ∈ S.arrows c d

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
s : Set (Subgroupoid.{u, u_1} C)
p : (c : C) × (d : C) × (c ⟶ d)
⊢ p ∈ sInf s ↔ ∀ S ∈ s, p ∈ S

Tactic:
mem_sInf_arrows

Premises used: iInf, Set.Mem, Set.iInter, setOf, CategoryTheory.Subgroupoid.toSet, CategoryTheory.Subgroupoid.mem_sInf_arrows
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ ∀ (s : Set (Subgroupoid.{u, u_1} C)), IsGLB s (sInf s)

Tactic:
fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩

Premises used: IsGreatest, IsGLB, And.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
refine_1 : ∀ (s : Set (Subgroupoid.{u, u_1} C)) (S : Subgroupoid.{u, u_1} C) (Ss : S ∈ s), ∀ F ∈ sInf s, F ∈ S
refine_2 :
  ∀ (s : Set (Subgroupoid.{u, u_1} C)) (T : Subgroupoid.{u, u_1} C) (Tl : T ∈ lowerBounds s)
    (F : (c : C) × (d : C) × (c ⟶ d)) (fT : F ∈ T), F ∈ sInf s
⊢ ∀ (s : Set (Subgroupoid.{u, u_1} C)), IsGLB s (sInf s)

Tactic:
refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
S : Subgroupoid.{u, u_1} C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
refine_1 : (∀ S ∈ s, F ∈ S) → F ∈ S
⊢ F ∈ sInf s → F ∈ S

Tactic:
simp only [mem_sInf]

Premises used: CategoryTheory.Subgroupoid.mem_sInf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
T : Subgroupoid.{u, u_1} C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
refine_2 : ∀ S ∈ s, F ∈ S
⊢ F ∈ sInf s

Tactic:
simp only [mem_sInf]

Premises used: CategoryTheory.Subgroupoid.mem_sInf
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
S : Subgroupoid.{u, u_1} C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ (∀ S ∈ s, F ∈ S) → F ∈ S

Tactic:
fun hp => hp S Ss

Premises used: Set.Mem
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
T : Subgroupoid.{u, u_1} C
Tl : T ∈ lowerBounds s
F : (c : C) × (d : C) × (c ⟶ d)
fT : F ∈ T
⊢ ∀ S ∈ s, F ∈ S

Tactic:
fun S Ss => Tl Ss fT

Premises used: Set.Mem
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S_1 : Subgroupoid.{u, u_1} C
s : Set (Subgroupoid.{u, u_1} C)
S : Subgroupoid.{u, u_1} C
Ss : S ∈ s
F : (c : C) × (d : C) × (c ⟶ d)
⊢ (∀ S ∈ s, F ∈ S) → F ∈ S

Tactic:
exacts [fun hp => hp S Ss, fun S Ss => Tl Ss fT]
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
⊢ S.objs ⊆ T.objs

Tactic:
fun s ⟨γ, hγ⟩ =>
  ⟨γ, @h ⟨s, s, γ⟩ hγ⟩

Premises used: Membership.mem, _private.0.CategoryTheory.Subgroupoid.le_objs.match_1, Set.Subset, Exists.intro, CategoryTheory.Subgroupoid.objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
x x_1 : (↑S.objs : Type u)
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ (inclusion h).obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) s hs) =
      (inclusion h).obj (Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) t ht) →
    Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) s hs = Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) t ht

Tactic:
simpa only [inclusion, Subtype.mk_eq_mk] using id

Premises used: id, Subtype.mk_eq_mk, CategoryTheory.Subgroupoid.inclusion
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
dsimp :
  Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) f ⋯ =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) g ⋯ →
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg
⊢ Eq.{u_1 + 1} (α := (inclusion h).obj s ⟶ (inclusion h).obj t)
      ((fun (f : s ⟶ t) ↦ (inclusion h).map f)
        (Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
          Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf))
      ((fun (f : s ⟶ t) ↦ (inclusion h).map f)
        (Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
          Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg)) →
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg

Tactic:
dsimp only [inclusion]

Premises used: CategoryTheory.Subgroupoid.inclusion
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
rw : f = g → f = g
⊢ Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) f ⋯ =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (T.arrows (↑s : C) (↑t : C)) x) g ⋯ →
    Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) f hf =
      Subtype.mk (p := fun (x : (↑s : C) ⟶ (↑t : C)) ↦
        Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) x) g hg

Tactic:
rw [Subtype.mk_eq_mk, 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 T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
⊢ f = g → f = g

Tactic:
id

Premises used: id
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
s t : (↑S.objs : Type u)
x x_1 : s ⟶ t
f : (↑s : C) ⟶ (↑t : C)
hf : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) f
g : (↑s : C) ⟶ (↑t : C)
hg : Membership.mem (γ := Set ((↑s : C) ⟶ (↑t : C))) (S.arrows (↑s : C) (↑t : C)) g
⊢ f = g → f = g

Tactic:
exact id

Premises used: id
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ inclusion ⋯ = 𝟭 (↑S.objs : Type u)

Tactic:
Functor.hext (fun _ => rfl) fun _ _ _ => HEq.refl _

Premises used: le_refl, CategoryTheory.Functor.hext, HEq.refl, CategoryTheory.Functor.map, CategoryTheory.Subgroupoid.inclusion, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
R S T : Subgroupoid.{u, u_1} C
k : R ≤ S
h : S ≤ T
⊢ inclusion ⋯ = inclusion k ⋙ inclusion h

Tactic:
rfl

Premises used: Set.Mem, setOf, CategoryTheory.Functor.comp, Set.Nonempty, CategoryTheory.Subgroupoid.inclusion, CategoryTheory.Subgroupoid.objs, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S T : Subgroupoid.{u, u_1} C
h : S ≤ T
⊢ inclusion h ⋙ T.hom = S.hom

Tactic:
rfl

Premises used: CategoryTheory.Subgroupoid.hom, Set.Mem, setOf, CategoryTheory.Functor.comp, Set.Nonempty, CategoryTheory.Subgroupoid.objs, 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
simp : Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (Groupoid.inv (𝟙 c))

Tactic:
simp only [inv_eq_inv, IsIso.inv_id]

Premises used: CategoryTheory.IsIso.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
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)

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_1 d : C
rw : Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c ≫ 𝟙 c)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d_1 d : C
⊢ Membership.mem (γ := Set (c ⟶ c)) {p : c ⟶ c | Discrete.Arrows c c p} (𝟙 c)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
⊢ ∃ (h : c = c), Eq.{u_1 + 1} (α := c ⟶ c) (𝟙 c) (eqToHom h)

Tactic:
⟨rfl, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
c d : C
⊢ ∃ (h : c = c), Eq.{u_1 + 1} (α := c ⟶ c) (𝟙 c) (eqToHom h)

Tactic:
exact ⟨rfl, rfl⟩
-- 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) (eqToHom ⋯)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
mp : S.IsWide → S.objs = univ
mpr : S.objs = univ → S.IsWide
⊢ S.IsWide ↔ S.objs = univ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
mp : ∀ (x : C), x ∈ S.objs ↔ Membership.mem (γ := Set C) univ x
⊢ S.objs = univ

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
mp : x ∈ S.objs → Membership.mem (γ := Set C) univ x
mp₁ : Membership.mem (γ := Set C) univ x → x ∈ S.objs
⊢ x ∈ S.objs ↔ Membership.mem (γ := Set C) univ x

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
⊢ x ∈ S.objs → Membership.mem (γ := Set C) univ x

Tactic:
simp only [mem_univ, imp_true_iff, forall_true_left]

Premises used: forall_true_left, imp_true_iff, Set.mem_univ
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
mp : x ∈ S.objs
⊢ Membership.mem (γ := Set C) univ x → x ∈ S.objs

Tactic:
simp only [mem_univ, imp_true_iff, forall_true_left]

Premises used: forall_true_left, imp_true_iff, Set.mem_univ
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.IsWide
x : C
⊢ x ∈ S.objs

Tactic:
apply mem_objs_of_src S (h.wide x)

Premises used: CategoryTheory.Subgroupoid.IsWide.wide, CategoryTheory.Subgroupoid.mem_objs_of_src
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
⊢ S.IsWide

Tactic:
⟨fun c => ?_⟩

Premises used: CategoryTheory.Subgroupoid.IsWide.mk
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
mpr : ∀ (c : C), 𝟙 c ∈ S.arrows c c
⊢ S.IsWide

Tactic:
refine ⟨fun c => ?_⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
c : C
mpr : ∀ (γ : c ⟶ c) (γS : γ ∈ S.arrows c c), 𝟙 c ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
obtain ⟨γ, γS⟩ := (le_of_eq h.symm : ⊤ ⊆ S.objs) (Set.mem_univ c)

Premises used: Set.mem_univ, le_of_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : S.objs = univ
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
id_mem_of_src S γS

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

Tactic:
exact id_mem_of_src S γS

Premises used: CategoryTheory.Subgroupoid.id_mem_of_src
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c : C
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
Sw.wide c

Premises used: CategoryTheory.Subgroupoid.IsWide.wide
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c d : C
h : c = d
refl : eqToHom ⋯ ∈ S.arrows c c
⊢ eqToHom h ∈ S.arrows c d

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c : C
refl : 𝟙 c ∈ S.arrows c c
⊢ eqToHom ⋯ ∈ S.arrows c c

Tactic:
simp only [eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sw : S.IsWide
c : C
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
apply Sw.id_mem c

Premises used: CategoryTheory.Subgroupoid.IsWide.id_mem
-- 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 : d ⟶ c
γ : c ⟶ c
hs : γ ∈ S.arrows c c
⊢ Groupoid.inv (Groupoid.inv p) ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d

Tactic:
Sn.conj (Groupoid.inv p) hs

Premises used: CategoryTheory.Groupoid.inv, 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 d : C
p : d ⟶ c
γ : c ⟶ c
hs : γ ∈ S.arrows c c
h : p = Groupoid.inv (Groupoid.inv p)
⊢ p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d

Tactic:
convert! Sn.conj (Groupoid.inv p) hs

Premises used: CategoryTheory.Groupoid.inv, 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 d : C
p : d ⟶ c
γ : c ⟶ c
hs : γ ∈ S.arrows c c
⊢ p = Groupoid.inv (Groupoid.inv p)

Tactic:
simp
-- 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
⊢ BijOn (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

Tactic:
⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
    ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩

Premises used: CategoryTheory.Groupoid.inv, And.intro, CategoryTheory.Subgroupoid.IsNormal.conj', Set.BijOn, Exists.intro, CategoryTheory.CategoryStruct.comp, 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 d : C
p : c ⟶ d
refine_1 :
  ∀ γ₁ ∈ S.arrows c c,
    ∀ γ₂ ∈ S.arrows c c,
      ∀
        (h :
          Eq.{u_1 + 1} (α := d ⟶ d) ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₁)
            ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₂)),
        γ₁ = γ₂
refine_2 :
  ∀ (δ : d ⟶ d) (δS : δ ∈ S.arrows d d), (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ
⊢ BijOn (fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

Tactic:
refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
    ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩
-- 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
γ₁ : c ⟶ c
h_1 : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
h_2 : γ₂ ∈ S.arrows c c
h :
  Eq.{u_1 + 1} (α := d ⟶ d) ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₁)
    ((fun (γ : c ⟶ c) ↦ Groupoid.inv p ≫ γ ≫ p) γ₂)
⊢ γ₁ = γ₂

Tactic:
simpa only [inv_eq_inv, Category.assoc, IsIso.hom_inv_id, Category.comp_id,
      IsIso.hom_inv_id_assoc] using p ≫= h =≫ inv p

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.inv, CategoryTheory.Groupoid.inv_eq_inv