-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem Map.arrows_iff (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c d : D} (f : c ⟶ d) :
    Map.Arrows φ hφ S c d f ↔
      ∃ (a b : C) (g : a ⟶ b) (ha : φ.obj a = c) (hb : φ.obj b = d) (_hg : g ∈ S.arrows a b),
        f = eqToHom ha.symm ≫ φ.map g ≫ eqToHom hb

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)

Tactic:
constructor

Result:
case mpr.intro.intro.intro.intro.intro.intro.hf
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ g ∈ S.arrows a b

Proof state:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (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

Tactic:
rintro ⟨a, b, g, rfl, rfl, hg, rfl⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)

Proof state:
case mp.im
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
g : c✝ ⟶ d✝
hg : g ∈ S.arrows c✝ d✝
⊢ ∃ a b g_1,
    ∃ (ha : φ.obj a = φ.obj c✝) (hb : φ.obj b = φ.obj d✝) (_ : g_1 ∈ S.arrows a b),
      φ.map g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb

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

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.hf
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ g ∈ S.arrows a b

Tactic:
exact hg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f ↔
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f →
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ (∃ a b g, ∃ (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

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (eqToHom ⋯ ≫ φ.map g ≫ eqToHom ⋯)

Tactic:
rw [← eq_conj_eqToHom]

Result:
case mpr.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
a b : C
g : a ⟶ b
hg : g ∈ S.arrows a b
⊢ Arrows φ hφ S (φ.obj a) (φ.obj b) (φ.map g)

Proof state:
case mp
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
f : c ⟶ d
⊢ Arrows φ hφ S c d f →
    ∃ a b g, ∃ (ha : φ.obj a = c) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), f = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb

Tactic:
rintro ⟨g, hg⟩

Result:
case mp.im
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
c d : D
c✝ d✝ : C
g : c✝ ⟶ d✝
hg : g ∈ S.arrows c✝ d✝
⊢ ∃ a b g_1,
    ∃ (ha : φ.obj a = φ.obj c✝) (hb : φ.obj b = φ.obj d✝) (_ : g_1 ∈ S.arrows a b),
      φ.map g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb