-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_map_objs_iff (hφ : Function.Injective φ.obj) (d : D) :
    d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d

Proof state:
case mp.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : Map.Arrows φ hφ S d d f
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
rw [Map.arrows_iff] at hf

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

Proof state:
case mpr.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ {x | Map.Arrows φ hφ S (φ.obj c) (φ.obj c) x}.Nonempty

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

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty

Tactic:
rintro ⟨c, ⟨γ, γS⟩, rfl⟩

Result:
case mpr.intro.intro.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
c : C
γ : c ⟶ c
γS : γ ∈ S.arrows c c
⊢ {x | Map.Arrows φ hφ S (φ.obj c) (φ.obj c) x}.Nonempty

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

Tactic:
obtain ⟨c, d, g, ec, ed, eg, gS, eg⟩ := hf

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d✝ : D
c d : C
g : c ⟶ d
ec : φ.obj c = d✝
ed : φ.obj d = d✝
eg : g ∈ S.arrows c d
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d✝

Proof state:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty ↔ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

case mpr
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ (∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d) → {x | Map.Arrows φ hφ S d d x}.Nonempty

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.refl
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d✝ : D
c d : C
g : c ⟶ d
ec : φ.obj c = d✝
ed : φ.obj d = d✝
eg : g ∈ S.arrows c d
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d✝

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

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ d ∈ (map φ hφ S).objs ↔ ∃ c ∈ S.objs, φ.obj c = d

Tactic:
dsimp [objs, map]

Result:
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty ↔ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Proof state:
case mp
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
⊢ {x | Map.Arrows φ hφ S d d x}.Nonempty → ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Tactic:
rintro ⟨f, hf⟩

Result:
case mp.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : f ∈ {x | Map.Arrows φ hφ S d d x}
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

Proof state:
case mp.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : f ∈ {x | Map.Arrows φ hφ S d d x}
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d

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

Result:
case mp.intro
C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
d : D
f : d ⟶ d
hf : Map.Arrows φ hφ S d d f
⊢ ∃ c, (S.arrows c c).Nonempty ∧ φ.obj c = d