Theorem: Groupoid.left_inv_cancel (Complexes/Structures/Groupoid.lean)

State before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ g ⁻¹ ≫ g ≫ h = h
Tactic:
rw [← comp_assoc]
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (g ⁻¹ ≫ g) ≫ h = h

State before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
⊢ (g ⁻¹ ≫ g) ≫ h = h
Tactic:
simp
State after:
no goals