Theorem: Groupoid.right_cancel_id' (Complexes/Structures/Groupoid.lean)

State before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
have := right_cancel e (𝟙 X) g
State after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = 𝟙 X ≫ g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X

State before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = 𝟙 X ≫ g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
simp at this
State after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X

State before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : X ⟶ X
this : e ≫ g = g ↔ e = 𝟙 X
⊢ e ≫ g = g ↔ e = 𝟙 X
Tactic:
assumption
State after:
no goals