awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 mpr : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)

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
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ g ∈ S.arrows a b

Tactic:
hg
-- 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
⊢ g ∈ S.arrows a b

Tactic:
exact hg
-- 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
rw :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
    {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (φ.map (Groupoid.inv f))
⊢ Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
    {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (Groupoid.inv (φ.map f))

Tactic:
rw [inv_eq_inv, ← Functor.map_inv, ← inv_eq_inv]

Premises used: CategoryTheory.Functor.map_inv, 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf_1 : f ∈ S.arrows c_1 d_1
hf : Groupoid.inv f ∈ S.arrows d_1 c_1
⊢ Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c_1))
    {x : φ.obj d_1 ⟶ φ.obj c_1 | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c_1) x} (φ.map (Groupoid.inv f))

Tactic:
constructor
-- 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf_1 hf : f ∈ S.arrows c_1 d_1
⊢ Groupoid.inv f ∈ S.arrows d_1 c_1

Tactic:
apply S.inv

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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
⊢ f ∈ S.arrows c_1 d_1

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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
e c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
q : φ.obj d_1 ⟶ e
hq : Membership.mem (γ := Set (φ.obj d_1 ⟶ e)) {x : φ.obj d_1 ⟶ e | Map.Arrows φ hφ S (φ.obj d_1) e x} q
obtain :
  ∀ (c₃ c₄ : C) (g : c₃ ⟶ c₄) (he : φ.obj c₃ = φ.obj d_1) {q : φ.obj d_1 ⟶ φ.obj c₄}
    (hq :
      Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
        {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q)
    (hg : g ∈ S.arrows c₃ c₄) (gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯),
    Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
      {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ e)) {x : φ.obj c_1 ⟶ e | Map.Arrows φ hφ S (φ.obj c_1) e x} (φ.map f ≫ q)

Tactic:
obtain ⟨c₃, c₄, g, he, rfl, hg, gq⟩ := (Map.arrows_iff φ hφ S q).mp hq

Premises used: CategoryTheory.Subgroupoid.Map.arrows_iff, Iff.mp, rfl
-- 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₃ c₄ : C
g : c₃ ⟶ c₄
he : φ.obj c₃ = φ.obj d_1
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
hg : g ∈ S.arrows c₃ c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
refl :
  ∀ (g : d_1 ⟶ c₄) (he : φ.obj d_1 = φ.obj d_1) (hg : g ∈ S.arrows d_1 c₄) (gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯),
    Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
      {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)

Tactic:
cases hφ he
-- 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
refl :
  Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map (f ≫ g))
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map f ≫ q)

Tactic:
rw [gq, ← eq_conj_eqToHom, ← φ.map_comp]

Premises used: CategoryTheory.eq_conj_eqToHom, 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
refl : f ≫ g ∈ S.arrows c_1 c₄
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj c₄))
    {x : φ.obj c_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj c_1) (φ.obj c₄) x} (φ.map (f ≫ g))

Tactic:
constructor
-- 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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ f ≫ g ∈ S.arrows c_1 c₄

Tactic:
S.mul hf hg

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
hφ : Function.Injective φ.obj
S : Subgroupoid.{u, u_2} C
c d : D
c_1 d_1 : C
f : c_1 ⟶ d_1
hf : f ∈ S.arrows c_1 d_1
c₄ : C
q : φ.obj d_1 ⟶ φ.obj c₄
hq :
  Membership.mem (γ := Set (φ.obj d_1 ⟶ φ.obj c₄))
    {x : φ.obj d_1 ⟶ φ.obj c₄ | Map.Arrows φ hφ S (φ.obj d_1) (φ.obj c₄) x} q
g : d_1 ⟶ c₄
he : φ.obj d_1 = φ.obj d_1
hg : g ∈ S.arrows d_1 c₄
gq : q = eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯
⊢ f ≫ g ∈ S.arrows c_1 c₄

Tactic:
exact S.mul hf hg

Premises used: CategoryTheory.Subgroupoid.mul
-- 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
⊢ f ∈ (map φ hφ S).arrows c d ↔
    ∃ (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:
Map.arrows_iff φ hφ S f

Premises used: Set.Mem, setOf, CategoryTheory.Subgroupoid.Map.arrows_iff
-- 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
T : Subgroupoid.{u_1, u_3} D
simp_rw : (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
⊢ map φ hφ S ≤ T ↔ S ≤ comap φ T

Tactic:
simp_rw [le_iff]

Premises used: CategoryTheory.Subgroupoid.le_iff
-- 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
T : Subgroupoid.{u_1, u_3} D
mp : (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
mpr : (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

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
T : Subgroupoid.{u_1, u_3} D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Tactic:
fun h c d f fS => h (Map.Arrows.im f fS)

Premises used: Set.Mem, setOf, Set.Subset, CategoryTheory.Subgroupoid.Map.Arrows.im
-- 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
T : Subgroupoid.{u_1, u_3} D
⊢ (∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) → ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d

Tactic:
exact fun h c d f fS => h (Map.Arrows.im f fS)
-- 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
T : Subgroupoid.{u_1, u_3} D
h : ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
c d : D
c_1 d_1 : C
a : c_1 ⟶ d_1
gφS : a ∈ S.arrows c_1 d_1
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj d_1)) (T.arrows (φ.obj c_1) (φ.obj d_1)) (φ.map a)

Tactic:
h gφS

Premises used: Set.Mem, setOf
-- 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
T : Subgroupoid.{u_1, u_3} D
h : ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
c d : D
c_1 d_1 : C
a : c_1 ⟶ d_1
gφS : a ∈ S.arrows c_1 d_1
⊢ Membership.mem (γ := Set (φ.obj c_1 ⟶ φ.obj d_1)) (T.arrows (φ.obj c_1) (φ.obj d_1)) (φ.map a)

Tactic:
exact h gφS
-- 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 T : Subgroupoid.{u, u_2} C
⊢ S ≤ T → map φ hφ S ≤ map φ hφ T

Tactic:
fun h => (galoisConnection_map_comap φ hφ).monotone_l h

Premises used: GaloisConnection.monotone_l, CategoryTheory.Subgroupoid.galoisConnection_map_comap
-- 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
⊢ S ≤ comap φ (map φ hφ S)

Tactic:
(galoisConnection_map_comap φ hφ).le_u_l S

Premises used: GaloisConnection.le_u_l, CategoryTheory.Subgroupoid.galoisConnection_map_comap
-- 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
T : Subgroupoid.{u_1, u_3} D
⊢ map φ hφ (comap φ T) ≤ T

Tactic:
(galoisConnection_map_comap φ hφ).l_u_le T

Premises used: GaloisConnection.l_u_le, CategoryTheory.Subgroupoid.galoisConnection_map_comap
-- 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
T : Subgroupoid.{u_1, u_3} D
⊢ map φ hφ S ≤ T ↔ S ≤ comap φ T

Tactic:
(galoisConnection_map_comap φ hφ).le_iff_le

Premises used: GaloisConnection.le_iff_le, CategoryTheory.Subgroupoid.galoisConnection_map_comap
-- 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
d : D
mp :
  Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} →
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
mpr :
  (∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d) →
    Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x}
⊢ Set.Nonempty.{u_3} (α := d ⟶ d) {x : d ⟶ d | Map.Arrows φ hφ S d d x} ↔
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d

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
d : D
f : d ⟶ d
hf : Membership.mem (γ := Set (d ⟶ d)) {x : d ⟶ d | Map.Arrows φ hφ S d d x} f
⊢ Map.Arrows φ hφ S d d f

Tactic:
change Map.Arrows φ hφ S d d f at hf

Premises used: CategoryTheory.Subgroupoid.Map.Arrows
-- 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
d : D
f : d ⟶ d
hf : Map.Arrows φ hφ S d d f
⊢ ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
rw [Map.arrows_iff] at hf

Premises used: CategoryTheory.Subgroupoid.Map.arrows_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
d : D
f : d ⟶ d
hf :
  ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b),
    f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb
mp :
  ∀ (c d_1 : C) (g : c ⟶ d_1) (ec : φ.obj c = d) (ed : φ.obj d_1 = d) (eg : g ∈ S.arrows c d_1),
    ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf
-- 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
d_1 : D
c d : C
g : c ⟶ d
ec : φ.obj c = d_1
ed : φ.obj d = d_1
eg : g ∈ S.arrows c d
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d_1

Tactic:
⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩

Premises used: CategoryTheory.Subgroupoid.mem_objs_of_src, And.intro, Exists.intro
-- 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
d_1 : D
c d : C
g : c ⟶ d
ec : φ.obj c = d_1
ed : φ.obj d = d_1
eg : g ∈ S.arrows c d
⊢ ∃ (c : C), (S.arrows c c).Nonempty ∧ φ.obj c = d_1

Tactic:
exact ⟨c, ⟨mem_objs_of_src S eg, ec⟩⟩
-- 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
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ Set.Nonempty.{u_3} (α := φ.obj c ⟶ φ.obj c) {x : φ.obj c ⟶ φ.obj c | Map.Arrows φ hφ S (φ.obj c) (φ.obj c) x}

Tactic:
⟨φ.map γ, ⟨γ, γS⟩⟩

Premises used: CategoryTheory.Functor.map, Set.Nonempty, Exists.intro, CategoryTheory.Subgroupoid.Map.Arrows.im
-- 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
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ Set.Nonempty.{u_3} (α := φ.obj c ⟶ φ.obj c) {x : φ.obj c ⟶ φ.obj c | Map.Arrows φ hφ S (φ.obj c) (φ.obj c) x}

Tactic:
exact ⟨φ.map γ, ⟨γ, γS⟩⟩
-- 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 : ∀ (x : D), x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs
⊢ (map φ hφ S).objs = φ.obj '' S.objs

Tactic:
ext x
-- 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
x : D
⊢ x ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = x

Tactic:
mem_map_objs_iff S φ hφ x

Premises used: CategoryTheory.Subgroupoid.mem_map_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
x : D
⊢ x ∈ (map φ hφ S).objs ↔ x ∈ φ.obj '' S.objs

Tactic:
convert! mem_map_objs_iff S φ hφ x

Premises used: CategoryTheory.Subgroupoid.mem_map_objs_iff
-- 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
c d : D
f : c ⟶ d
⊢ Map.Arrows φ hφ ⊤ c d f ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_ :
      Membership.mem (γ := Set (a ⟶ b)) (arrows ⊤ a b) g), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
Map.arrows_iff φ hφ ⊤ f

Premises used: CategoryTheory.Subgroupoid.Map.arrows_iff, Top.top
-- 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
c d : D
f : c ⟶ d
h :
  ∀ (x x_1 : C) (x_2 : x ⟶ x_1) (x_3 : φ.obj x = c) (x_4 : φ.obj x_1 = d),
    f = eqToHom ⋯ ≫ φ.map x_2 ≫ eqToHom x_4 ↔
      ∃ (_ : Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊤ x x_1) x_2), f = eqToHom ⋯ ≫ φ.map x_2 ≫ eqToHom x_4
⊢ f ∈ (im φ hφ).arrows c d ↔
    ∃ (a : C) (b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
convert! Map.arrows_iff φ hφ ⊤ f

Premises used: CategoryTheory.Subgroupoid.Map.arrows_iff, Top.top
-- 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
c d : D
f : c ⟶ d
x x_1 : C
x_2 : x ⟶ x_1
h : φ.obj x = c
h_1 : φ.obj x_1 = d
⊢ f = eqToHom ⋯ ≫ φ.map x_2 ≫ eqToHom h_1 ↔
    ∃ (_ : Membership.mem (γ := Set (x ⟶ x_1)) (arrows ⊤ x x_1) x_2), f = eqToHom ⋯ ≫ φ.map x_2 ≫ eqToHom h_1

Tactic:
simp only [Top.top, mem_univ, exists_true_left]

Premises used: exists_true_left, Set.mem_univ, Top.top
-- 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
d : D
⊢ d ∈ (im φ hφ).objs ↔ ∃ (c : C), φ.obj c = d

Tactic:
simp only [im, mem_map_objs_iff, mem_top_objs, true_and]

Premises used: CategoryTheory.Subgroupoid.im, CategoryTheory.Subgroupoid.mem_top_objs, CategoryTheory.Subgroupoid.mem_map_objs_iff, true_and
-- 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
hφ' : im φ hφ = ⊤
d : D
rw : Membership.mem (γ := Set D) (objs.{u_1, u_3} ⊤) d
⊢ ∃ (a : C), φ.obj a = d

Tactic:
rw [← mem_im_objs_iff _ hφ, hφ']

Premises used: CategoryTheory.Subgroupoid.mem_im_objs_iff
-- 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
hφ' : im φ hφ = ⊤
d : D
⊢ 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
obtain :
  ∀ (c : C), Membership.mem (γ := Set (φ.obj c ⟶ φ.obj c)) ((map φ hφ S).arrows (φ.obj c) (φ.obj c)) (𝟙 (φ.obj c))
⊢ 𝟙 d ∈ (map φ hφ S).arrows d d

Tactic:
obtain ⟨c, rfl⟩ := obj_surjective_of_im_eq_top φ hφ hφ' d

Premises used: CategoryTheory.Subgroupoid.obj_surjective_of_im_eq_top, 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
rw : Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))

Tactic:
rw [← Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- 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
hf : 𝟙 c ∈ S.arrows c c
⊢ Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))

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 ∈ S.arrows c c

Tactic:
Sn.wide c

Premises used: CategoryTheory.Subgroupoid.IsNormal.toIsWide, CategoryTheory.Subgroupoid.IsWide.wide
-- 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 ∈ S.arrows c c

Tactic:
exact Sn.wide c

Premises used: CategoryTheory.Subgroupoid.IsNormal.toIsWide, CategoryTheory.Subgroupoid.IsWide.wide