Theorem: Groupoid.inv_comp (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) ⁻¹ = h ⁻¹ ≫ g ⁻¹
Tactic:
have := left_cancel_inv (g ≫ h)⁻¹ (h⁻¹ ≫ g⁻¹)
State after:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ ≫ (g ≫ h) ⁻¹ ⁻¹ ≫ h ⁻¹ ≫ g ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹

State before:
S : Sort u_2
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h h' : Y ⟶ Z
this : (g ≫ h) ⁻¹ ≫ (g ≫ h) ⁻¹ ⁻¹ ≫ h ⁻¹ ≫ g ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ 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
this : (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹
⊢ (g ≫ h) ⁻¹ = h ⁻¹ ≫ g ⁻¹

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