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

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

Tactic:
by
  rw [← comp_left, e.hom_inv_id, id_left]

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

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

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x'

Tactic:
h

Goal state after:
X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ (ConcreteCategory.hom f) x' = (ConcreteCategory.hom f) x'
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
⊢ f x = f x' → x = x'

Tactic:
h

Goal state after:
case mp
X Y : Type u
f : X → Y
H : Mono (↾f)
x x' : X
h : f x = f x'
⊢ x = x'
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
⊢ (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
⊢ (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝ → a₁✝ = a₂✝

Tactic:
h

Goal state after:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
h : (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝
⊢ a₁✝ = a₂✝
Module: Mathlib.CategoryTheory.Adjunction.Basic

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
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : adj.unit.app A ≫ G.map f = g
⊢ f = F.map g ≫ adj.counit.app B

Tactic:
by simp [← h]

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

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
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : F.map g ≫ adj.counit.app B = f
⊢ g = adj.unit.app A ≫ G.map f

Tactic:
by simp [← h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ G.map (lift s) ≫ G.map (t.π.app j) = G.map (s.π.app j)

Tactic:
h

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app j)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = G.map (lift s)

Tactic:
h

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = ht.lift (G.mapCone s)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑p j' = ↑p j ≫ ((const J).obj W).map f

Tactic:
by dsimp; rw [comp_id]; exact p.2 f

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

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
⊢ ∀ (g_1 : Y ⟶ Y'), (e X Y') (g ≫ g_1) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map g_1

Tactic:
h

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ (e X Y') (g ≫ h) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map h
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ x ≤ y

Tactic:
h

Goal state after:
X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ y ≤ y
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.op)) (e.homEquiv (𝟙 Y)) = (ConcreteCategory.hom (F.map f.op)) (e'.homEquiv (𝟙 Y))

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.op)) (e'.homEquiv (𝟙 Y)) = (ConcreteCategory.hom (F.map f.op)) (e'.homEquiv (𝟙 Y))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X✝)) = (ConcreteCategory.hom (F.map f)) (e'.homEquiv (𝟙 X✝))

Tactic:
h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ (ConcreteCategory.hom (F.map f)) (e'.homEquiv (𝟙 X✝)) = (ConcreteCategory.hom (F.map f)) (e'.homEquiv (𝟙 X✝))
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (α_ (f ≫ g) (𝟙 c) (𝟙 c)).inv ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c

Tactic:
triangle_assoc_comp_right,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ (α_ g (𝟙 c) (𝟙 c)).inv ≫ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ ((α_ g (𝟙 c) (𝟙 c)).inv ≫ (ρ_ g).hom ▷ 𝟙 c) ≫ (α_ f g (𝟙 c)).inv =
    (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom

Tactic:
triangle_assoc_comp_right,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ g ◁ (λ_ (𝟙 c)).hom ≫ (α_ f g (𝟙 c)).inv = (α_ f g (𝟙 c ≫ 𝟙 c)).inv ≫ (f ≫ g) ◁ (λ_ (𝟙 c)).hom
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yonedaEquiv.symm (yonedaEquiv (yoneda.map f.unop ≫ u)) = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)

Tactic:
Equiv.symm_apply_apply,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yoneda.map f.unop ≫ u = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g : F.obj Y ⟶ Z
⊢ ∀ (h : F.obj Y ⟶ Z), F.map f ≫ g = F.map f ≫ h → g = h

Tactic:
h

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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
⊢ F.map f ≫ g = F.map f ≫ h → g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
m :
  (mk c.pt fun x ↦
        match x with
        | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
    t.pt
⊢ (∀ (j : (a : α) × β a),
      (mk c.pt fun x ↦
                match x with
                | ⟨a, b⟩ => π a b ≫ c.inj a).inj
            j ≫
          m =
        t.inj j) →
    m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
h

Goal state after:
case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
m :
  (mk c.pt fun x ↦
        match x with
        | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
⊢ m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ Hom.right f = Hom.right g

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ Hom.right g = Hom.right g
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' Y'' : C
T T' : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ X.right = Y.right

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y✝ Y' Y'' : C
T T' : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ Y.right = Y.right
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ I.lift (BinaryFan.swap t) = I.lift (BinaryFan.swap t)

C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m = R.lift (BinaryFan.assocInv P t)

Tactic:
h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ R.lift (BinaryFan.assocInv P t) = R.lift (BinaryFan.assocInv P t)

C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j
Module: Mathlib.CategoryTheory.Comma.Over.Basic

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

Tactic:
h

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
h : f = g
⊢ g.left = g.left
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
h : f = g
⊢ f.right = g.right

Tactic:
h

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
h : f = g
⊢ g.right = g.right
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g✝ : Under X✝
φ : f✝ ⟶ g✝
X Y : T
f g : X ⟶ Y
h : f = g
A : Under Y
⊢ (map f).obj A = (map g).obj A

Tactic:
h

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g✝ : Under X✝
φ : f✝ ⟶ g✝
X Y : T
f g : X ⟶ Y
h : f = g
A : Under Y
⊢ (map g).obj A = (map g).obj A
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ f.left = g.left

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
f g : X ⟶ Y
h : f = g
⊢ g.left = g.left
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' Y'' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ X.left = Y.left

Tactic:
h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y✝ Y' Y'' : C
S S' : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ Y.left = Y.left
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
X : C
⊢ ((S.leftUnitor.hom ≫ S.rightUnitor.inv) ≫ S.whiskerLeft G.unitIso.hom).app X =
    (Functor.whiskerRight F.unitIso.hom S ≫
          (F.functor.associator F.inverse S).hom ≫
            F.functor.whiskerLeft α' ≫
              (F.functor.associator U G.inverse).inv ≫
                Functor.whiskerRight α G.inverse ≫ (S.associator G.functor G.inverse).hom).app
      X

Tactic:
simpa using congr($(hα'α).app X)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Over (op X)
f : Z ⟶ Y
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop

Tactic:
rw [← unop_comp, Over.w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ x ≫ h = t.snd ≫ g

Tactic:
← hyh,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
⊢ t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ data.i.app f ≫ data.p.app f = f.hom

Tactic:
by
  rw [← NatTrans.comp_app, fac, Arrow.leftToRight_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

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.Full
inst✝ : F.Faithful
X : C
hX : IsZero (F.obj X)
h : F.FullyFaithful
this✝ : (Y : C) → Unique (F.obj X ⟶ F.obj Y)
this : (Y : C) → Unique (F.obj Y ⟶ F.obj X)
⊢ IsZero X

Tactic:
exact ⟨fun Y ↦ ⟨h.homEquiv.unique⟩, fun Y ↦ ⟨h.homEquiv.unique⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f

Tactic:
h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
simp [← Category.assoc, fac]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'

Tactic:
by
    rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.47, 0} J)
⊢ HasLimitsOfShape J C

Tactic:
apply @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ l.symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
h

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')

Tactic:
h

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
⊢ (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure

Tactic:
ext X
  simp only [prop_sup_iff]
  constructor
  · rintro ⟨Y, hY, ⟨e⟩⟩
    simp only [prop_sup_iff] at hY
    obtain hY | hY := hY
    · exact Or.inl ⟨Y, hY, ⟨e⟩⟩
    · exact Or.inr ⟨Y, hY, ⟨e⟩⟩
  · rintro (hY | hY)
    · exact monotone_isoClosure le_sup_left _ hY
    · exact monotone_isoClosure le_sup_right _ hY

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : CancelMonoid M
⊢ m₁.toRightCancelMonoid = m₂.toRightCancelMonoid → m₁ = m₂

Tactic:
h

Goal state after:
M : Type u
m₁ m₂ : CancelMonoid M
h : m₁.toRightCancelMonoid = m₂.toRightCancelMonoid
⊢ m₁ = m₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : f = 0
W'✝ : C
x✝² : W'✝ ⟶ X
x✝¹ : x✝² ≫ f = 0
x✝ : W'✝ ⟶ X
hb : x✝ ≫ 𝟙 X = x✝²
⊢ x✝ = x✝²

Tactic:
by simp only [← hb, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ parallelPair g 0 ≅ parallelPair g 0