mathlib-initiative/mathlib-tactics huggingface dataset:
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)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 (Y i) = 𝟙 (Y i)

Tactic:
]

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
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (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 :
  F.map (G.map (F.map (η.inv.app X))) ≫ ε.hom.app (F.obj X) = ε.hom.app (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X)
⊢ F.map (η.hom.app X) ≫
      F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj 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
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (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
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)

Tactic:
]

Goal state after:
J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
h : f = 𝟙 j
⊢ F.map (𝟙 j) = 𝟙 (F.obj j)
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∀ (b : α), p (discreteEquiv.symm b)) = ∀ (a' : α), p { as := a' }

Tactic:
]

Goal state after:
α : Type u_1
p : Discrete α → Prop
⊢ (∀ (b : α), p (discreteEquiv.symm b)) = ∀ (a' : α), p { as := a' }
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∃ b, p (discreteEquiv.symm b)) = ∃ a', p { as := a' }

Tactic:
]

Goal state after:
α : Type u_1
p : Discrete α → Prop
⊢ (∃ b, p (discreteEquiv.symm b)) = ∃ a', p { as := a' }
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 (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (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 :
  F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X))) = ε.hom.app (F.obj X) ≫ ε.inv.app (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_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ 𝟙 (Opposite.unop (G.obj X)) = 𝟙 (Opposite.unop (G.obj X))

Tactic:
]

Goal state after:
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ᵒᵖ
e : F ≅ G
X : C
⊢ 𝟙 (Opposite.unop (F.obj X)) = 𝟙 (Opposite.unop (F.obj X))

Tactic:
]

Goal state after:
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.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.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ᵒᵖ
⊢ (α.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.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.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
C' : Option J → Type u₁
inst✝ : (i : Option J) → Category.{v₁, u₁} (C' i)
⊢ (pi' fun i ↦
        match i with
        | none => Prod.fst (C' none) ((j : J) → C' (some j))
        | some i => Prod.snd (C' none) ((j : J) → C' (some j)) ⋙ eval (fun j ↦ C' (some j)) i) ⋙
      (eval C' none).prod' (pi' fun i ↦ eval C' (some i)) ≅
    𝟭 (C' none × ((j : J) → C' (some j)))

Tactic:
by exact Iso.refl _

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
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.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X)

Tactic:
]

Goal state after:
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 : F ⟶ G
⊢ ((NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    ({ app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom).op

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 : F ⟶ G
⊢ ((NatIso.ofComponents (fun x ↦ Iso.refl ((unop G).obj x)) ⋯).hom ≫ f.unop).op =
    ({ app := fun X ↦ f.unop.op.unop.app X, naturality := ⋯ } ≫
        (NatIso.ofComponents (fun x ↦ Iso.refl ((unop F).obj x)) ⋯).hom).op
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ 𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj X)

Tactic:
]

Goal state after:
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
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op

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
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ ((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₂ = Hom.left φ₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Y.left = Y.left

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Y.right = Y.right

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W W' : MorphismProperty C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f
X Y : C
f : X ⟶ Y
⊢ W' f = W' f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case mpr
T : Type u
inst✝ : Category.{v, u} T
X Y : T
f f' : X ⟶ Y
h : f = f'
⊢ mk f' = mk f'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → ⊤ ≤ isomorphisms C

Tactic:
]

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → ⊤ ≤ isomorphisms C
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : r.hom ≫ g.hom = f.hom ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom

Tactic:
]

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
l : f.right ≅ g.right
r : f.left ≅ g.left
h : r.hom ≫ g.hom = f.hom ≫ l.hom
⊢ r.hom ≫ g.hom = f.hom ≫ l.hom
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : e₂.hom ≫ g = f ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom

Tactic:
]

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
W X Y Z : T
f : X ⟶ W
g : Z ⟶ Y
e₁ : W ≅ Y
e₂ : X ≅ Z
h : e₂.hom ≫ g = f ≫ e₁.hom
⊢ e₂.hom ≫ g = f ≫ e₁.hom
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)

Tactic:
]

Goal state after:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝¹ : IsIso sq
inst✝ : IsIso f.hom
⊢ IsIso (Hom.left (asIso sq).inv ≫ f.hom ≫ Hom.right (asIso sq).hom)
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
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map 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
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map F
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ g.hom ≫ i = g.hom ≫ i

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ f ≫ h ≫ i' = f ≫ h ≫ i'

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ g.op = g.op

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ f.op = f.op

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ g.unop = g.unop

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f' ∈ P.toSet

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f' ∈ P.toSet
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f ∈ P.toSet

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : Arrow.mk f ∈ P.toSet
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ Arrow.mk f ∈ P.toSet
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A✝ B✝ X✝ Y✝ : C
f✝ : A✝ ⟶ X✝
i✝ : A✝ ⟶ B✝
p✝ : X✝ ⟶ Y✝
g✝ : B✝ ⟶ Y✝
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ f.unop = f.unop

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
A B : C
g : A ⟶ B
i : ι
h : Arrow.mk g = Arrow.mk (f i)
⊢ ofHoms f (f i)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ aux φ ≫ sq = aux ψ ≫ sq

Tactic:
]

Goal state after:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ ↦ { left := φ, right := φ ≫ f.hom, w := ⋯ }
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ aux φ ≫ sq = aux ψ ≫ sq
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ i ≫ l₁.l = i ≫ l₂.l

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
inst✝ : Epi i
l₁ l₂ : sq.LiftStruct
⊢ i ≫ l₁.l = i ≫ l₂.l
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝¹ ≫ x✝)

Tactic:
]

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝¹ ≫ x✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsLeft Q

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsLeft Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsLeft Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝ ≫ x✝¹)

Tactic:
]

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : ∀ W_1 ∈ W, W_1 x✝
⊢ ∀ W_1 ∈ W, W_1 (x✝ ≫ x✝¹)
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsRight Q

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : CategoryStruct.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
Q : MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsRight Q
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsRight Q
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsIso

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
W : ι → MorphismProperty C
inst✝ : ∀ (i : ι), (W i).RespectsIso
⊢ (InfSet.sInf (Set.range fun i ↦ W i)).RespectsIso
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ 𝟙 f.left = 𝟙 f.left

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ 𝟙 g.left = 𝟙 g.left

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
se : SplitEpi f
F : C ⥤ D
⊢ 𝟙 (F.obj Y) = 𝟙 (F.obj Y)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f00x ≫ f0x1 ≫ fx11 = f00x ≫ fx01 ≫ f1x1

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
M000 M001 M010 M011 M100 M101 M110 M111 : C
f00x : M000 ⟶ M001
f01x : M010 ⟶ M011
f10x : M100 ⟶ M101
f11x : M110 ⟶ M111
f0x0 : M000 ⟶ M010
f0x1 : M001 ⟶ M011
f1x0 : M100 ⟶ M110
f1x1 : M101 ⟶ M111
fx00 : M000 ⟶ M100
fx01 : M001 ⟶ M101
fx10 : M010 ⟶ M110
fx11 : M011 ⟶ M111
h0xx : f0x0 ≫ f01x = f00x ≫ f0x1
h1xx : f1x0 ≫ f11x = f10x ≫ f1x1
hx0x : fx00 ≫ f10x = f00x ≫ fx01
hx1x : fx10 ≫ f11x = f01x ≫ fx11
hxx0 : f0x0 ≫ fx10 = fx00 ≫ f1x0
inst✝ : Epi f00x
⊢ f00x ≫ f0x1 ≫ fx11 = f00x ≫ fx01 ≫ f1x1
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.RespectsIso

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.RespectsIso
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
h : P ≤ Q
⊢ Q ≤ Q

Tactic:
]

Goal state after: