[GOAL]
C : Type u_1
inst✝ : Groupoid C
⊢ Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)
[PROOFSTEP]
refine' ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => _⟩
[GOAL]
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g
[PROOFSTEP]
haveI := h d
[GOAL]
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = g
[PROOFSTEP]
calc
  f = f ≫ inv g ≫ g := by simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
  _ = f ≫ inv f ≫ g := by
    congr 1
    simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
  _ = g := by simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f = f ≫ inv g ≫ g
[PROOFSTEP]
simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv g ≫ g = f ≫ inv f ≫ g
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ inv g ≫ g = inv f ≫ g
[PROOFSTEP]
simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
[GOAL]
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
this : Subsingleton (d ⟶ d)
⊢ f ≫ inv f ≫ g = g
[PROOFSTEP]
simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]
