Theorem: Groupoid.left_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' → h = h'
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'
⊢ h = h'

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 => g ⁻¹ ≫ x) (g ≫ h) = (fun x => g ⁻¹ ≫ x) (g ≫ h')
⊢ h = h'
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 : h = h'
⊢ h = h'

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 : h = h'
⊢ h = h'
Tactic:
assumption
State after:
no goals