C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g
C : Type u_1
inst✝ : Groupoid C
⊢ Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)
refine' ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => _⟩
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
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g
haveI := h d
no goals
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
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]
no goals
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
simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
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
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
congr 1
no goals
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
simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
no goals
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
simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]