Theorem: Groupoid.inv_inv (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
Tactic:
have := left_inv_cancel (g⁻¹) g
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ 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
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ g = g
⊢ g ⁻¹ ⁻¹ = g
Tactic:
rw [inv_comp_id, comp_id] at this
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
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
this : g ⁻¹ ⁻¹ = g
⊢ g ⁻¹ ⁻¹ = g
Tactic:
assumption
State after:
no goals