awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ : δ ∈ (map φ hφ S).arrows d d
⊢ ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
rw [mem_map_iff] at hδ

Premises used: CategoryTheory.Subgroupoid.mem_map_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d d' : D
g : d ⟶ d'
δ : d ⟶ d
hδ :
  ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
obtain :
  ∀ (c c' : C) (γ : c ⟶ c') (cd : φ.obj c = d) (cd' : φ.obj c' = d) (γS : γ ∈ S.arrows c c')
    (hγ : δ = eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd'), Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
obtain ⟨c, c', γ, cd, cd', γS, hγ⟩ := hδ
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d d' : D
g : d ⟶ d'
δ : d ⟶ d
c c' : C
γ : c ⟶ c'
cd : φ.obj c = d
cd' : φ.obj c' = d
γS : γ ∈ S.arrows c c'
hγ : δ = eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd'
subst_vars :
  ∀ (g : φ.obj c ⟶ d') (cd' : φ.obj c' = φ.obj c),
    Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
⊢ Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
subst_vars
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c c' : C
γ : c ⟶ c'
γS : γ ∈ S.arrows c c'
g : φ.obj c ⟶ d'
cd' : φ.obj c' = φ.obj c
refl :
  ∀ (γ : c ⟶ c) (γS : γ ∈ S.arrows c c) (cd' : φ.obj c = φ.obj c),
    Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
cases hφ cd'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
rw : Membership.mem (γ := Set D) (objs.{u_1, u_3} ⊤) d'
⊢ d' ∈ (im φ hφ).objs

Tactic:
rw [hφ']
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ Membership.mem (γ := Set D) (objs.{u_1, u_3} ⊤) d'

Tactic:
apply mem_top_objs

Premises used: CategoryTheory.Subgroupoid.mem_top_objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
⊢ d' ∈ (im φ hφ).objs

Tactic:
have : d' ∈ (im φ hφ).objs := by rw [hφ']; apply mem_top_objs
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : d' ∈ (im φ hφ).objs
⊢ ∃ (c : C), φ.obj c = d'

Tactic:
rw [mem_im_objs_iff] at this

Premises used: CategoryTheory.Subgroupoid.mem_im_objs_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
d' : D
c : C
g : φ.obj c ⟶ d'
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
this : ∃ (c : C), φ.obj c = d'
refl :
  ∀ (c' : C) (g : φ.obj c ⟶ φ.obj c'),
    Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
      (Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g)
⊢ Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'

Tactic:
obtain ⟨c', rfl⟩ := this

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
rw : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) (arrows ⊤ (φ.obj c) (φ.obj c')) g
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g

Tactic:
rw [hφ']
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) (arrows ⊤ (φ.obj c) (φ.obj c')) g

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
⊢ Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g

Tactic:
have : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c') := by rw [hφ']; trivial
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
this : Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c')) ((im φ hφ).arrows (φ.obj c) (φ.obj c')) g
⊢ ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'),
    g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb

Tactic:
rw [mem_im_iff] at this

Premises used: CategoryTheory.Subgroupoid.mem_im_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
g : φ.obj c ⟶ φ.obj c'
this :
  ∃ (a : C) (b : C) (g_1 : a ⟶ b) (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'),
    g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb
refl :
  ∀ (b b' : C) (f : b ⟶ b') (hb : φ.obj b = φ.obj c) (hb' : φ.obj b' = φ.obj c'),
    Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
      (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
        (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g)

Tactic:
obtain ⟨b, b', f, hb, hb', _, hf⟩ := this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b b' : C
f : b ⟶ b'
hb : φ.obj b = φ.obj c
hb' : φ.obj b' = φ.obj c'
refl :
  ∀ (f : c ⟶ b') (hb : φ.obj c = φ.obj c),
    Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
      (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
        (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')

Tactic:
cases hφ hb
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' b' : C
hb' : φ.obj b' = φ.obj c'
f : c ⟶ b'
hb : φ.obj c = φ.obj c
refl :
  ∀ (hb' : φ.obj c' = φ.obj c') (f : c ⟶ c'),
    Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
      (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
        (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
⊢ Membership.mem (γ := Set (φ.obj c' ⟶ φ.obj c')) ((map φ hφ S).arrows (φ.obj c') (φ.obj c'))
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')

Tactic:
cases hφ hb'
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
refl : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c')
    (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫
      (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')

Tactic:
simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Groupoid.inv_eq_inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
this : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this

Premises used: CategoryTheory.Functor.map_inv, CategoryTheory.Functor.map_comp, CategoryTheory.Groupoid.inv_eq_inv
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
this : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
this : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
exact this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
refl : Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)

Tactic:
suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
        simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
refl : Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' c'
⊢ Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_2, u} C
S : 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
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
Sn : S.IsNormal
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
cd' : φ.obj c = φ.obj c
c' : C
hb : φ.obj c = φ.obj c
hb' : φ.obj c' = φ.obj c'
f : c ⟶ c'
⊢ Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' c'

Tactic:
apply Sn.conj f γS

Premises used: 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
⊢ S.IsThin ↔ ∀ (c : (↑S.objs : Type u)), Subsingleton.{u_1 + 1} (↑(S.arrows (↑c : C) (↑c : C)) : Type u_1)

Tactic:
isThin_iff _

Premises used: CategoryTheory.Groupoid.isThin_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
mp : S.IsTotallyDisconnected → ∀ (c d : C), (S.arrows c d).Nonempty → c = d
mpr : (∀ (c d : C), (S.arrows c d).Nonempty → c = d) → S.IsTotallyDisconnected
⊢ S.IsTotallyDisconnected ↔ ∀ (c d : C), (S.arrows c d).Nonempty → 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
h : S.IsTotallyDisconnected
c d : C
f : c ⟶ d
fS : f ∈ S.arrows c d
⊢ c = d

Tactic:
congr_arg Subtype.val <| h ⟨c, mem_objs_of_src S fS⟩ ⟨d, mem_objs_of_tgt S fS⟩ ⟨f, fS⟩

Premises used: CategoryTheory.Subgroupoid.mem_objs_of_src, Subtype.mk, congr_arg, Subtype.val, 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
h : S.IsTotallyDisconnected
c d : C
f : c ⟶ d
fS : f ∈ S.arrows c d
⊢ c = d

Tactic:
exact congr_arg Subtype.val <| h ⟨c, mem_objs_of_src S fS⟩ ⟨d, mem_objs_of_tgt S fS⟩ ⟨f, fS⟩

Premises used: CategoryTheory.Subgroupoid.mem_objs_of_src, Subtype.mk, congr_arg, Subtype.val, 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
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
fS :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    f
mpr : 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
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
fS :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    f
⊢ c = d

Tactic:
h c d ⟨f, fS⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
h : ∀ (c d : C), (S.arrows c d).Nonempty → c = d
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
f : (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶ (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)
fS :
  Membership.mem (γ :=
    Set
      ((↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C) ⟶
        (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C)))
    (S.arrows (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) c hc) : C)
      (↑(Subtype.mk (p := fun (x : C) ↦ x ∈ S.objs) d hd) : C))
    f
⊢ c = d

Tactic:
exact h c d ⟨f, fS⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
p : c ⟶ c
h : p ∈ S.arrows c c
⊢ Membership.mem (γ := Set (c ⟶ c)) {f : c ⟶ c | c = c ∧ f ∈ S.arrows c c} (Groupoid.inv p)

Tactic:
⟨rfl, S.inv h⟩

Premises used: Set.Mem, setOf, And.intro, CategoryTheory.Subgroupoid.inv, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
p : c ⟶ c
h : p ∈ S.arrows c c
⊢ Membership.mem (γ := Set (c ⟶ c)) {f : c ⟶ c | c = c ∧ f ∈ S.arrows c c} (Groupoid.inv p)

Tactic:
exact ⟨rfl, S.inv h⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
p : c ⟶ c
h : p ∈ S.arrows c c
q : c ⟶ c
h' : q ∈ S.arrows c c
⊢ Membership.mem (γ := Set (c ⟶ c)) {f : c ⟶ c | c = c ∧ f ∈ S.arrows c c} (p ≫ q)

Tactic:
⟨rfl, S.mul h h'⟩

Premises used: CategoryTheory.Subgroupoid.mul, Set.Mem, setOf, And.intro, rfl
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c : C
p : c ⟶ c
h : p ∈ S.arrows c c
q : c ⟶ c
h' : q ∈ S.arrows c c
⊢ Membership.mem (γ := Set (c ⟶ c)) {f : c ⟶ c | c = c ∧ f ∈ S.arrows c c} (p ≫ q)

Tactic:
exact ⟨rfl, S.mul h h'⟩
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
rw : ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d
⊢ S.disconnect ≤ S

Tactic:
rw [le_iff]

Premises used: CategoryTheory.Subgroupoid.le_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
c d : C
a : c ⟶ d
left : c = d
right : a ∈ S.arrows c d
⊢ a ∈ S.arrows c d

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
Sn : S.IsNormal
⊢ S.disconnect.IsNormal

Tactic:
{ wide := fun c => ⟨rfl, Sn.wide c⟩
    conj := fun _ _ ⟨_, h'⟩ => ⟨rfl, Sn.conj _ h'⟩ }

Premises used: CategoryTheory.Subgroupoid.disconnect, CategoryTheory.Groupoid.inv, CategoryTheory.Subgroupoid.IsNormal.toIsWide, Membership.mem, CategoryTheory.Subgroupoid.IsWide.wide, CategoryTheory.Subgroupoid.IsNormal.mk, CategoryTheory.Subgroupoid.arrows, And.intro, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Subgroupoid.disconnect_normal.match_1, CategoryTheory.Subgroupoid.IsWide.mk, rfl, 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
c : C
⊢ c ∈ S.disconnect.objs ↔ c ∈ S.objs

Tactic:
⟨fun ⟨γ, _, γS⟩ => ⟨γ, γS⟩, fun ⟨γ, γS⟩ => ⟨γ, rfl, γS⟩⟩

Premises used: CategoryTheory.Subgroupoid.disconnect, Membership.mem, _private.0.CategoryTheory.Subgroupoid.le_objs.match_1, And.intro, Iff.intro, _private.0.CategoryTheory.Subgroupoid.mem_disconnect_objs_iff.match_1, Exists.intro, 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
⊢ S.disconnect.objs = S.objs

Tactic:
Set.ext fun _ ↦ mem_disconnect_objs_iff _

Premises used: Set.ext, CategoryTheory.Subgroupoid.mem_disconnect_objs_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
rw : ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d
⊢ S.disconnect.IsTotallyDisconnected

Tactic:
rw [isTotallyDisconnected_iff]

Premises used: CategoryTheory.Subgroupoid.isTotallyDisconnected_iff
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d

Tactic:
fun c d ⟨_, h, _⟩ => h

Premises used: _private.0.CategoryTheory.Subgroupoid.disconnect_isTotallyDisconnected.match_1, Eq
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
⊢ ∀ (c d : C), (S.disconnect.arrows c d).Nonempty → c = d

Tactic:
exact fun c d ⟨_, h, _⟩ => h
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d : C
p : c ⟶ d
left_1 : c ∈ D
right_1 left : d ∈ D
right : c ∈ D
⊢ Membership.mem (γ := Set (d ⟶ c)) {_f : d ⟶ c | d ∈ D ∧ c ∈ D} (Groupoid.inv p)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d : C
p : c ⟶ d
left : c ∈ D
right : d ∈ D
⊢ d ∈ D

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d : C
p : c ⟶ d
left : c ∈ D
right : d ∈ D
⊢ c ∈ D

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d e : C
p : c ⟶ d
left_1 : c ∈ D
right_1 : d ∈ D
q : d ⟶ e
left_2 : d ∈ D
right_2 : e ∈ D
left : c ∈ D
right : e ∈ D
⊢ Membership.mem (γ := Set (c ⟶ e)) {_f : c ⟶ e | c ∈ D ∧ e ∈ D} (p ≫ q)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid
Goal:
C : Type u
inst : Groupoid.{u_1, u} C
S : Subgroupoid.{u, u_1} C
D : Set C
c d e : C
p : c ⟶ d
left : c ∈ D
right : d ∈ D
q : d ⟶ e
left_1 : d ∈ D
right_1 : e ∈ D
⊢ c ∈ D

Tactic:
assumption