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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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
f : X ≅ Y
⊢ F.map f.hom ≫ F.map f.inv = 𝟙 (F.obj X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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
f : X ≅ Y
⊢ F.map f.inv ≫ F.map f.hom = 𝟙 (F.obj Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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 Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ⟶ F.obj Y
g : F.obj Y ⟶ F.obj Z
⊢ F.map (F.preimage (f ≫ g)) = F.map (F.preimage f ≫ F.preimage g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ⟶ Y
⊢ F.map (F.preimage (F.map f)) = F.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.hom ≫ F.preimage f.inv) = F.map (𝟙 X)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ofObj X ≤ P
i : ι
⊢ ofObj X (X i)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
⊢ ofObj Subtype.val = P

Tactic:
ext X
  exact ⟨by rintro ⟨X, hX⟩; exact hX,
    fun hX ↦ ofObj_apply Subtype.val ⟨X, hX⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
inst✝¹ : F.Full
inst✝ : F.Faithful
f : F.obj X ≅ F.obj Y
⊢ F.map (F.preimage f.inv ≫ F.preimage f.hom) = F.map (𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
inst✝¹ : F.Full
inst✝ : F.Faithful
f : X ≅ Y
⊢ (F.preimageIso (F.mapIso f)).hom = f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
x✝ : X ⟶ Y
⊢ hF.preimage (F.map x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
x✝ : F.obj X ⟶ F.obj Y
⊢ F.map (hF.preimage x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
⊢ F.map (hF.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Category

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
F G : C ⥤ D
H : D ⥤ E
α : F ⟶ G
X : C
⊢ (α ◫ 𝟙 H).app X = H.map (α.app X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Category

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
F G : C ⥤ D
H : E ⥤ C
α : F ⟶ G
X : E
⊢ (𝟙 H ◫ α).app X = α.app (H.obj X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.hom ≫ hF.preimage e.inv) = F.map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app X)
⊢ inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
X✝¹ Y✝¹ : C
F : C ⥤ D
X✝ Y✝ Z : C
hF : F.FullyFaithful
X Y : C
e : F.obj X ≅ F.obj Y
⊢ F.map (hF.preimage e.inv ≫ hF.preimage e.hom) = F.map (𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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 Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
inst✝ : ∀ (X : C), IsIso (α.app X)
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (asIso (α.app Y)).hom = (asIso (α.app X)).hom ≫ G.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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 Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ IsIso (F₁.map f) → IsIso (F₂.map f)

Tactic:
hf

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)
Module: Mathlib.CategoryTheory.NatIso

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 Y : C
e : X ≅ Y
⊢ F.map e.inv ≫ α.app X ≫ G.map e.hom = α.app Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

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 Y : C
e : X ≅ Y
⊢ F.map e.hom ≫ α.app Y ≫ G.map e.inv = α.app X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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
F F' : C ⥤ D
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : G.Full
X✝ Y✝ : C
f : (F ⋙ G).obj X✝ ⟶ (F ⋙ G).obj Y✝
⊢ (F ⋙ G).map (F.preimage (G.preimage f)) = f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
x✝ : CC X
⊢ (ConcreteCategory.hom (𝟙 X)) x✝ = id x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : CC X
⊢ (ConcreteCategory.hom (f ≫ g)) x✝ = (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)

Tactic:
← h X,

Goal state after:
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.obj X ⟶ τ (σ Y)
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.map f ≍ ⋯ ▸ ⋯ ▸ φ.map f

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
hzero : p.length = 0
⊢ a = b

Tactic:
cases p
  · rfl
  · cases Nat.succ_ne_zero _ hzero

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case nil
V : Type u_2
inst✝¹ : Quiver V
inst✝ : HasReverse V
a b c : V
p : Path a b
⊢ (p.comp nil).reverse = nil.reverse.comp p.reverse

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case nil
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
⊢ nil.reverse.reverse = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_2
V : Type u_1
inst✝ : Quiver V
a b c : V
p' : Path a c
e : c ⟶ b
⊢ (p'.cons e).length ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (p.comp nil).toList = nil.toList ++ p.toList

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C✝ : Type u₁
D✝ : Type u₂
E : Type u₃
inst✝⁷ : Category.{v₁, u₁} C✝
inst✝⁶ : Category.{v₂, u₂} D✝
inst✝⁵ : Category.{v₃, u₃} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ E
J : Type u_1
C : Type u_2
D : Type u_3
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} C
inst✝² : Category.{v_3, u_3} D
G : J ⥤ D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
x✝ : J
⊢ F.map
      (F.preimage
        ((F.toEssImage.objObjPreimageIso { obj := G.obj x✝, property := ⋯ }).hom.hom ≫
          G.map (𝟙 x✝) ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj x✝, property := ⋯ }).inv.hom)) =
    F.map (𝟙 (F.toEssImage.objPreimage { obj := G.obj x✝, property := ⋯ }))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C✝ : Type u₁
D✝ : Type u₂
E : Type u₃
inst✝⁷ : Category.{v₁, u₁} C✝
inst✝⁶ : Category.{v₂, u₂} D✝
inst✝⁵ : Category.{v₃, u₃} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ E
J : Type u_1
C : Type u_2
D : Type u_3
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} C
inst✝² : Category.{v_3, u_3} D
G : J ⥤ D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hG : ∀ (j : J), F.essImage (G.obj j)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ F.map
      (F.preimage
        ((F.toEssImage.objObjPreimageIso { obj := G.obj X✝, property := ⋯ }).hom.hom ≫
          G.map (x✝¹ ≫ x✝) ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Z✝, property := ⋯ }).inv.hom)) =
    F.map
      (F.preimage
          ((F.toEssImage.objObjPreimageIso { obj := G.obj X✝, property := ⋯ }).hom.hom ≫
            G.map x✝¹ ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Y✝, property := ⋯ }).inv.hom) ≫
        F.preimage
          ((F.toEssImage.objObjPreimageIso { obj := G.obj Y✝, property := ⋯ }).hom.hom ≫
            G.map x✝ ≫ (F.toEssImage.objObjPreimageIso { obj := G.obj Z✝, property := ⋯ }).inv.hom))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
X : C
e : F.obj X ≅ Y
⊢ ⊤ X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X : C
f g : W ⟶ X
⊢ f = eqToHom ⋯ ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ z j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast ⋯ q = eqToHom ⋯ ≫ q

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ ⋯.mpr q = eqToHom ⋯ ≫ q

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ cast ⋯ p = p ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ eqToHom p ≫ eqToHom ⋯ = 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
X Y : C
p : X = Y
⊢ eqToHom ⋯ ≫ eqToHom p = 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso ⋯)).hom = (eqToIso ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ e (e.symm X✝) = X✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ Y✝ = e (e.symm Y✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x✝ : InducedCategory D ⇑e
⊢ (𝟭 (InducedCategory D ⇑e)).obj x✝ =
    (inducedFunctor ⇑e ⋙
          { obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ }).obj
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : Type u_2
e : T ≃ D
x✝ : D
⊢ ({ obj := ⇑e.symm, map := fun {X Y} f ↦ InducedCategory.homMk (eqToHom ⋯ ≫ f ≫ eqToHom ⋯), map_id := ⋯,
            map_comp := ⋯ } ⋙
          inducedFunctor ⇑e).obj
      x✝ =
    (𝟭 D).obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Const

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : C ⥤ D
X : C
⊢ ∀ {X_1 Y : J} (f : X_1 ⟶ Y),
    ((F ⋙ const J).obj X).map f ≫ (Iso.refl (((F ⋙ const J).obj X).obj Y)).hom =
      (Iso.refl (((F ⋙ const J).obj X).obj X_1)).hom ≫ ((const J ⋙ (whiskeringRight J C D).obj F).obj X).map f

Tactic:
simp

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
e : C ≌ D
X : C
⊢ e.unit.app X ≫ e.unitInv.app X = 𝟙 X

Tactic:
simp

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
e : C ≌ D
X : C
⊢ e.unitInv.app X ≫ e.unit.app X = 𝟙 (e.inverse.obj (e.functor.obj X))

Tactic:
simp

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
e : C ≌ D
Y : D
⊢ e.counit.app Y ≫ e.counitInv.app Y = 𝟙 (e.functor.obj (e.inverse.obj Y))

Tactic:
simp

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
e : C ≌ D
Y : D
⊢ e.counitInv.app Y ≫ e.counit.app Y = 𝟙 Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
x✝ : C
⊢ (𝟙 F ◫ α).app x✝ = (F.whiskerLeft α).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
x✝ : C
⊢ (α ◫ 𝟙 F).app x✝ = (whiskerRight α F).app x✝

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).1 ⟶ (P, S).1
hfg₁ : f.1 ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.1 = 𝟙 Q
g₂ : (Q, T).2 ⟶ (P, S).2
hfg₂ : f.2 ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.2 = 𝟙 T
⊢ IsIso f

Tactic:
refine ⟨⟨(g₁, g₂), by aesop_cat, by aesop_cat⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
x✝ : C
⊢ (F.whiskerLeft β ≫ whiskerRight α K).app x✝ = (whiskerRight α H ≫ G.whiskerLeft β).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ⟶ G
β : H ⟶ K
x✝ : C
⊢ (α ◫ β).app x✝ = (F.whiskerLeft β ≫ whiskerRight α K).app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

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
F G : C ⥤ D
H K : D ⥤ E
α : F ≅ G
β : H ≅ K
x✝ : C
⊢ (F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K).hom.app x✝ = (isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β).hom.app x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f.op ≫ (inv f).op).unop = (𝟙 (op Y)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ((inv f).op ≫ f.op).unop = (𝟙 (op X)).unop

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ (f ≫ (inv f.op).unop).op = (𝟙 X).op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ ((inv f.op).unop ≫ f).op = (𝟙 Y).op

Tactic:
simp

Goal state after:
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)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f' ≫
        fun b ↦ 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))) x✝

Tactic:
simp

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

Goal state before:
pp: case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1

Tactic:
intro ⟨X⟩

Goal state after:
case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
X : I
⊢ ∀ (Y : Discrete I) (f : { as := X } ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯