Theorem: Groupoid.right_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 ≫ h = g' ≫ h → g = g'
Tactic:
intro hyp
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
⊢ g = g'

State before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : (fun x => x ≫ h ⁻¹ ) (g ≫ h) = (fun x => x ≫ h ⁻¹ ) (g' ≫ h)
⊢ g = g'
Tactic:
simp at this
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : g = g'
⊢ g = g'

State before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
hyp : g ≫ h = g' ≫ h
this : g = g'
⊢ g = g'
Tactic:
assumption
State after:
no goals