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

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

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