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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
⊢ (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
    (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f

Tactic:
ext (a : coyoneda.obj (op X) ⟶ F)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : coyoneda.obj (op X) ⟶ F
⊢ (ConcreteCategory.hom ((coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun a =
    (ConcreteCategory.hom ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f)).toFun a
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ ∀ (X : ↑(typeToCat.obj X✝)),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.obj X = F.toFunctor.obj X

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
s : Set C
inst✝¹ : Small.{w, u} ↑s
inst✝ : LocallySmall.{w, v, u} C
⊢ Function.Injective fun x ↦ ⟨x.obj, ⋯⟩

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
K : J ⥤ C
c d : Cone K
f : c ⟶ d
i : IsIso f.hom
⊢ f ≫ { hom := inv f.hom, w := ⋯ } = 𝟙 c ∧ { hom := inv f.hom, w := ⋯ } ≫ f = 𝟙 d

Tactic:
by cat_disch

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

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
D : Type u₄
inst✝² : Category.{v₄, u₄} D
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F : J ⥤ C
s : Cone F
X : C
f : X ⟶ s.pt
inst✝ : IsIso f
⊢ s.extendHom f ≫ (s.extendIso (asIso' f)).hom = 𝟙 (s.extend f) ∧ (s.extendIso (asIso' f)).hom ≫ s.extendHom f = 𝟙 s

Tactic:
by cat_disch

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

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
D : Type u₄
inst✝³ : Category.{v₄, u₄} D
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : J ⥤ C
G : C ⥤ D
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
⊢ (functoriality F G).map { hom := G.preimage t.hom, w := ⋯ } = t

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.LeftInverse (fun l ↦ { l := (adj.homEquiv B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }) fun l ↦
    { l := (adj.homEquiv B X) l.l, fac_left := ⋯, fac_right := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ Function.RightInverse (fun l ↦ { l := (adj.homEquiv B X).symm l.l, fac_left := ⋯, fac_right := ⋯ }) fun l ↦
    { l := (adj.homEquiv B X) l.l, fac_left := ⋯, fac_right := ⋯ }

Tactic:
by cat_disch

Goal state after:
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ Function.LeftInverse (fun s ↦ { section_ := F.preimage s.section_, id := ⋯ }) fun f_1 ↦ f_1.map F

Tactic:
by cat_disch

Goal state after:
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
x : SplitEpi (F.map f)
⊢ (fun f_1 ↦ f_1.map F) ((fun s ↦ { section_ := F.preimage s.section_, id := ⋯ }) x) = x

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a : x ⟶ y
⊢ ∀ (b : x ⟶ y), a = b

Tactic:
b

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ a = b
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ (Functor.empty C).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → (Functor.empty C).obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ (X : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj Y).obj X ⟶ F.obj X

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
t : IsLimit { pt := Y, π := { app := fun X ↦ id (Discrete.casesOn X fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X ⟶ Y
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }
X : C
f : X✝ ⟶ X
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ (X : Discrete PEmpty.{w + 1}) → ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).obj X ⟶ F₁.obj X

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ (X : Discrete PEmpty.{w + 1}) → F₁.obj X ⟶ ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).obj X

Tactic:
by cat_disch

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

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap α ≫ limMap (inv α) = 𝟙 (limit F)

Tactic:
by cat_disch

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

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap (inv α) ≫ limMap α = 𝟙 (limit G)

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
X : C
f : X ⟶ c.pt
⊢ lift F (c.extend f) = f ≫ lift F c

Tactic:
by cat_disch

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

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
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ s.isLimit.lift (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv

Tactic:
by cat_disch

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

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
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.LeftInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
by cat_disch

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

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
inst✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.RightInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
F : J' ⥤ C
⊢ HasLimit F

Tactic:
apply hasLimit_of_equivalence_comp e

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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePullbackShape J
a : x✝¹ ⟶ x✝
⊢ ∀ (b : x✝¹ ⟶ x✝), a = b

Tactic:
b

Goal state after:
J : Type w
x✝¹ x✝ : WidePullbackShape J
a b : x✝¹ ⟶ x✝
⊢ a = b
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
j : WidePullbackShape J
⊢ F.obj j = (wideCospan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.term j)).obj j

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = colim.map F.leftUnitor.hom

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePushoutShape J
a : x✝¹ ⟶ x✝
⊢ ∀ (b : x✝¹ ⟶ x✝), a = b

Tactic:
b

Goal state after:
J : Type w
x✝¹ x✝ : WidePushoutShape J
a b : x✝¹ ⟶ x✝
⊢ a = b
Module: Mathlib.CategoryTheory.Limits.HasLimits

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
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.LeftInverse (fun g ↦ colimit.desc f { pt := c, ι := g }) fun g ↦
    { app := fun x ↦ colimit.ι f x ≫ g, naturality := ⋯ }

Tactic:
by cat_disch

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

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
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
f : J ⥤ C
c : C
⊢ Function.RightInverse (fun g ↦ colimit.desc f { pt := c, ι := g }) fun g ↦
    { app := fun x ↦ colimit.ι f x ≫ g, naturality := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasLimit F₁
⊢ (X : Discrete PEmpty.{w' + 1}) → ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).obj X ⟶ F₂.obj X

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasColimit F₁
⊢ (X : Discrete PEmpty.{w' + 1}) → F₂.obj X ⟶ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).obj X

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty.{1} ⥤ C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty.{1} ⥤ C
⊢ (X_1 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasTerminal C
j : J
⊢ limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j = terminal.from (⊤_ C)

Tactic:
by cat_disch

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasInitial C
j : J
⊢ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to (⊥_ C)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f : F.obj { as := left } ⟶ G.obj { as := left }
g : F.obj { as := right } ⟶ G.obj { as := right }
x✝² x✝¹ : Discrete WalkingPair
X Y : WalkingPair
x✝ : { as := X } ⟶ { as := Y }
u : { as := X }.as = { as := Y }.as
⊢ (F.map { down := { down := u } } ≫
      match { as := Y } with
      | { as := left } => f
      | { as := right } => g) =
    (match { as := X } with
      | { as := left } => f
      | { as := right } => g) ≫
      G.map { down := { down := u } }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f✝ : F.obj { as := left } ⟶ G.obj { as := left }
g✝ : F.obj { as := right } ⟶ G.obj { as := right }
f : F.obj { as := left } ≅ G.obj { as := left }
g : F.obj { as := right } ≅ G.obj { as := right }
X✝ Y✝ : Discrete WalkingPair
x✝ : X✝ ⟶ Y✝
u : X✝.as = Y✝.as
⊢ F.map { down := { down := u } } ≫
      (match Y✝ with
        | { as := left } => f
        | { as := right } => g).hom =
    (match X✝ with
        | { as := left } => f
        | { as := right } => g).hom ≫
      G.map { down := { down := u } }

Tactic:
by cat_disch

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

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
⊢ (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt

Tactic:
exact Cofan.IsColimit.desc hc' fun i ↦ Cofan.IsColimit.desc (hc i) fun j ↦ t.inj (i, j)

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

Goal state before:
pp: X Y : WalkingSpan
a : X ⟶ Y
⊢ ∀ (b : X ⟶ Y), a = b

Tactic:
b

Goal state after:
X Y : WalkingSpan
a b : X ⟶ Y
⊢ 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 S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
⊢ f = mk (f.hom ≫ T.map (𝟙 f.right))

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ ∀ (s : PushoutCocone f g) (m : pushout f g ⟶ s.pt),
    pushout.inl f g ≫ m = s.inl → pushout.inr f g ≫ m = s.inr → m = pushout.desc s.inl s.inr ⋯

Tactic:
by cat_disch

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
f✝ g : Over X
φ : f✝ ⟶ g
A✝ B✝ : Over X
f : A✝ ⟶ B✝
x✝ : IsIso ((forget X).map f)
⊢ f ≫ homMk (inv ((forget X).map f)) ⋯ = 𝟙 A✝ ∧ homMk (inv ((forget X).map f)) ⋯ ≫ f = 𝟙 B✝

Tactic:
by cat_disch

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
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ (post F).map (homMk a ⋯) = f

Tactic:
by cat_disch

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

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

Tactic:
by
  simp [← Under.comp_right]

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

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

Tactic:
by
  simp [← Under.comp_right]

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

Goal state before:
pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U : Under Z
⊢ ∀ (Y_1 : Under Z) (f_1 : U ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯

Tactic:
V

Goal state after:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
⊢ ∀ (f_1 : U ⟶ V), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯
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
Y Z : Under X
f : Y ⟶ Z
t : IsIso ((forget X).map f)
⊢ f ≫ homMk (inv ((forget X).map f)) ⋯ = 𝟙 Y ∧ homMk (inv ((forget X).map f)) ⋯ ≫ f = 𝟙 Z

Tactic:
by cat_disch

Goal state after:
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
f : CostructuredArrow S T
⊢ mk (S.map (𝟙 f.left) ≫ f.hom) = f

Tactic:
by cat_disch

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
F : D ⥤ T
Y : T
X : D
⊢ ∀ {X_1 Y_1 : StructuredArrow Y (Under.forget X ⋙ F)} (f : X_1 ⟶ Y_1),
    (ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofStructuredArrowProjEquivalence.inverse F Y X ⋙ ofStructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (StructuredArrow Y (Under.forget X ⋙ F))).map f

Tactic:
by cat_disch

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 × T
⊢ ∀ {X_1 Y : StructuredArrow X.2 (Under.forget X.1)} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (StructuredArrow X.2 (Under.forget X.1))).map f

Tactic:
by cat_disch

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
F : T ⥤ D
Y : D
X : T
⊢ ∀ {X_1 Y_1 : CostructuredArrow (Over.forget X ⋙ F) Y} (f : X_1 ⟶ Y_1),
    (ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).map f ≫
        (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              Y_1)).hom =
      (Iso.refl
            ((ofCostructuredArrowProjEquivalence.inverse F Y X ⋙ ofCostructuredArrowProjEquivalence.functor F Y X).obj
              X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X ⋙ F) Y)).map f

Tactic:
by cat_disch

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 × T
⊢ ∀ {X_1 Y : CostructuredArrow (Over.forget X.1) X.2} (f : X_1 ⟶ Y),
    (ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).map f ≫
        (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj Y)).hom =
      (Iso.refl ((ofDiagEquivalence.inverse X ⋙ ofDiagEquivalence.functor X).obj X_1)).hom ≫
        (𝟭 (CostructuredArrow (Over.forget X.1) X.2)).map f

Tactic:
by cat_disch

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
⊢ (h ≫ x) ≫ t.inl = g ≫ t.inr

Tactic:
← hhy,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
⊢ (h ≫ x) ≫ t.inl = (h ≫ y) ≫ t.inr
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk X✝.hom.left).hom

Tactic:
rw [← w φ, comp_left]
    simp

Goal state after: