mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (ε.app (F.obj X)).hom ≫ (ε.app (F.obj X)).inv = 𝟙 ((G ⋙ F).obj (F.obj X))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (ε.app (F.obj X)).hom ≫ (ε.app (F.obj X)).inv = 𝟙 ((G ⋙ F).obj (F.obj X))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝)).op ≫ (α.inv.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝)).op ≫ (α.inv.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝) ≫ α.hom.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝) ≫ α.hom.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ (ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X)) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (G.obj (unop x✝))).op = 𝟙 (op (G.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (G.obj (unop x✝))).op = 𝟙 (op (G.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ C i ≌ C i

Tactic:
;

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ C i ≌ C i
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x✝ = (𝟙 F.op).app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x✝ = (𝟙 F.op).app x✝
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ eval C i ⋙ (eqToEquivalence C ⋯).functor = eval C i

Tactic:
;

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
⊢ eval C i ⋙ (eqToEquivalence C ⋯).functor = eval C i
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝)).op ≫ (α.hom.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝)).op ≫ (α.hom.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' : J
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) ⋯).functor

Tactic:
;

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
f : J → I
i' : J
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) ⋯).functor
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: C : Type u_1
as✝ : C
⊢ { as := as✝ } = { as := { as := as✝ }.as }

Tactic:
;

Goal state after:
C : Type u_1
as✝ : C
⊢ { as := as✝ } = { as := { as := as✝ }.as }
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : ε.hom.app (F.obj X) ≫ ε.inv.app (F.obj X) = 𝟙 (F.obj (G.obj (F.obj X)))
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj ((𝟭 C).obj X))
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : (F.mapIso (η.app X)).hom ≫ (F.mapIso (η.app X)).inv = 𝟙 (F.obj ((𝟭 C).obj X))
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this : F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : IsIso α
⊢ NatTrans.op α ≫ NatTrans.op (inv α) = 𝟙 G.op

Tactic:
simp [← NatTrans.op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X : D
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ 𝟙 X ≫ (F.objObjPreimageIso X).inv)) = F.map (𝟙 (F.objPreimage X))

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X : D
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ 𝟙 X ≫ (F.objObjPreimageIso X).inv)) = F.map (𝟙 (F.objPreimage X))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ (f ≫ g) ≫ (F.objObjPreimageIso Z).inv)) =
    F.map
      (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) ≫
        F.preimage ((F.objObjPreimageIso Y).hom ≫ g ≫ (F.objObjPreimageIso Z).inv))

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ (f ≫ g) ≫ (F.objObjPreimageIso Z).inv)) =
    F.map
      (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv) ≫
        F.preimage ((F.objObjPreimageIso Y).hom ≫ g ≫ (F.objObjPreimageIso Z).inv))
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.left (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯

Tactic:
;

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
X : Arrow T
⊢ Hom.right (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ ((fun i ↦ Groupoid.inv (f i)) ≫ f) i = 𝟙 Y✝ i

Tactic:
;

Goal state after:
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ ((fun i ↦ Groupoid.inv (f i)) ≫ f) i = 𝟙 Y✝ i
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ (f ≫ fun i ↦ Groupoid.inv (f i)) i = 𝟙 X✝ i

Tactic:
;

Goal state after:
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ (f ≫ fun i ↦ Groupoid.inv (f i)) i = 𝟙 X✝ i
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
ι : Type u_3
P : ι → MorphismProperty D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (⨆ i, P i).inverseImage F f✝ ↔ (⨆ i, (P i).inverseImage F) f✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
ι : Type u_3
P : ι → MorphismProperty D
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (⨆ i, P i).inverseImage F f✝ ↔ (⨆ i, (P i).inverseImage F) f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P : Set (MorphismProperty D)
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (sSup P).inverseImage F f✝ ↔ (⨆ P' ∈ P, P'.inverseImage F) f✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
P : Set (MorphismProperty D)
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (sSup P).inverseImage F f✝ ↔ (⨆ P' ∈ P, P'.inverseImage F) f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso g
h : P (f ≫ g)
⊢ P f

Tactic:
simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
x✝ : Fun X Y
⊢ (fun f ↦ { toFun := f }) ((fun f ↦ ⇑f) x✝) = x✝

Tactic:
;

Goal state after:
X Y : Type u
x✝ : Fun X Y
⊢ (fun f ↦ { toFun := f }) ((fun f ↦ ⇑f) x✝) = x✝
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
x✝ : X → Y
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f }) x✝) = x✝

Tactic:
;

Goal state after:
X Y : Type u
x✝ : X → Y
⊢ (fun f ↦ ⇑f) ((fun f ↦ { toFun := f }) x✝) = x✝
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : m α
⊢ (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)))).toFun X = (ConcreteCategory.hom (𝟙 (m α))).toFun X

Tactic:
;

Goal state after:
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : m α
⊢ (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)))).toFun X = (ConcreteCategory.hom (𝟙 (m α))).toFun X
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
⊢ P.map F f → P.map G f

Tactic:
⟨X', Y', f', hf', ⟨e'⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F G : C ⥤ D
e : F ≅ G
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e' : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ P.map G f
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left

Tactic:
;

Goal state after:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right

Tactic:
;

Goal state after:
case refl
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
X : C
g : (End X)ˣ
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { hom := ↑({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g),
      inv := ({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g).inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
X : C
g : (End X)ˣ
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { hom := ↑({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g),
      inv := ({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g).inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : C
val✝¹ inv✝¹ : End X
val_inv✝¹ : val✝¹ * inv✝¹ = 1
inv_val✝¹ : inv✝¹ * val✝¹ = 1
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ {
      hom :=
        ↑({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }),
      inv :=
        ({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }).inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ },
        inv := { val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ }

Tactic:
;

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : C
val✝¹ inv✝¹ : End X
val_inv✝¹ : val✝¹ * inv✝¹ = 1
inv_val✝¹ : inv✝¹ * val✝¹ = 1
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ {
      hom :=
        ↑({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }),
      inv :=
        ({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
            { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }).inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ },
        inv := { val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ }
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ (F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
;

Goal state after:
X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
;

Goal state after:
X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
;

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
;

Goal state after:
X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
;

Goal state after:
X Y : GrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
;

Goal state after:
X Y : GrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
;

Goal state after:
X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
;

Goal state after:
X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝

Tactic:
;

Goal state after:
R S : SemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝

Tactic:
;

Goal state after:
R S : SemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
x✝ : ↑S
⊢ ((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝

Tactic:
;

Goal state after:
R S : RingCat
e : R ≅ S
x✝ : ↑S
⊢ ((RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝