Theorem: Groupoid.left_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 : Y ⟶ Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
Tactic:
have := left_cancel g e (𝟙 Y)
State after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ≫ 𝟙 Y ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y

State before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
e : Y ⟶ Y
this : g ≫ e = g ≫ 𝟙 Y ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y
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 : Y ⟶ Y
this : g ≫ e = g ↔ e = 𝟙 Y
⊢ g ≫ e = g ↔ e = 𝟙 Y

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