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

State before:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ⁻¹ ⁻¹ ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h
Tactic:
rw [inv_inv] at this
State after:
S : Sort u_1
G : Groupoid S
X Y Z : S
g g' : X ⟶ Y
h✝ h' : Y ⟶ Z
h : X ⟶ Z
this : g ≫ g ⁻¹ ≫ h = h
⊢ g ≫ g ⁻¹ ≫ h = h

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