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

Goal state before:
pp: case fst.mk
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✝ F : J ⥤ C
fst✝ : C
snd✝ : F.cocones.obj fst✝
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun ⟨fst✝, snd✝⟩).fst

Tactic:
rfl

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

Goal state before:
pp: case snd
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✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).snd

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f }
⊢ { left := s, right := t, hom := f } = { left := s, right := t, hom := f }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
j✝ j'✝ : C
φ : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (𝟙 X ≫ τ.app j'✝)) default = (ConcreteCategory.hom (τ.app j'✝)) default

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
x✝ : C
x : X
⊢ (ConcreteCategory.hom
          (((fun s ↦ { app := fun j ↦ ↾fun x ↦ ↑s j, naturality := ⋯ })
                ((fun τ ↦ ⟨fun j ↦ (ConcreteCategory.hom (τ.app j)) default, ⋯⟩) τ)).app
            x✝)).toFun
      default =
    (ConcreteCategory.hom (τ.app x✝)).toFun default

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
x : ↑F.sections
⊢ (G.sectionsEquivHom X) ((ConcreteCategory.hom ((sectionsFunctor C).map f)) x) = (F.sectionsEquivHom X) x ≫ f

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Type u₂
f : F ⟶ G
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ (G.sectionsEquivHom X).symm (τ ≫ f) =
    (ConcreteCategory.hom ((sectionsFunctor C).map f)) ((F.sectionsEquivHom X).symm τ)

Tactic:
rfl

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
⊢ Function.RightInverse (fun u ↦ { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ }) fun t X_1 ↦
    {
      default :=
        t.desc { pt := X_1, ι := { app := fun X_2 ↦ id (Discrete.casesOn X_2 fun as ↦ ⋯.elim), naturality := ⋯ } },
      uniq := ⋯ }

Tactic:
grind

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 : J ⥤ C
inst✝ : HasLimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl

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 : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl

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 G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cone.postcompose α).obj c).π.app j✝

Tactic:
rfl

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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)

Tactic:
rfl

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
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝

Tactic:
rfl

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
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)

Tactic:
rfl

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

Goal state before:
pp: case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

Tactic:
rfl

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

Goal state before:
pp: case some.none.term.term
J : Type w
b : J
⊢ Hom.term b = Hom.term b

Tactic:
rfl

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

Goal state before:
pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
rfl

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
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝

Tactic:
rfl

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
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (E.whiskerLeft α).app j✝ ≫ ι G (E.obj j✝)

Tactic:
rfl

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

Goal state before:
pp: case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

pp: case none.some.init.init
J : Type w
b : J
⊢ Hom.init b = Hom.init b

pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
rfl

Goal state after:
case none.some.init.init
J : Type w
b : J
⊢ Hom.init b = Hom.init b

case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.some.init.init
J : Type w
b : J
⊢ Hom.init b = Hom.init b

pp: case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)

Tactic:
rfl

Goal state after:
case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:

Tactic:
rfl

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✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι G j✝)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : EssentiallySmall.{u₁, v₂, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
by
  have := HasColimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} J)
  exact hasColimitsOfShape_of_equivalence (equivSmallModel.{u₁} J).symm

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = m.unop.op

Tactic:
rfl

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (t.op.ι.app (Opposite.op j) ≫ m).unop

Tactic:
rfl

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
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
⊢ m = m.unop.op

Tactic:
rfl

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

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

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
val✝ : J
⊢ F.obj (some val✝) = (wideSpan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.init j)).obj (some val✝)

Tactic:
rfl

Goal state after:
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
val✝ : J
⊢ F.obj (some val✝) = (wideSpan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.init j)).obj (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

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

Tactic:
rfl

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
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
j : J
⊢ t.ι.app j ≫ m.unop = (m ≫ t.op.π.app (Opposite.op j)).unop

Tactic:
rfl

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
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ m = m.op.unop

Tactic:
rfl

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
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ m.op ≫ t.π.app j = (t.unop.ι.app (Opposite.unop j) ≫ m).op

Tactic:
rfl

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
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ m = m.op.unop

Tactic:
rfl

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
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
j : Jᵒᵖ
⊢ t.ι.app j ≫ m.op = (m ≫ t.unop.π.app (Opposite.unop j)).op

Tactic:
rfl

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

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ s.π.app none = e.hom ≫ t.π.app none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)

Tactic:
· exact base.symm

Goal state after:
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β✝ : 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
a : α
b : β a
⊢ (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := b } = t.inj ⟨a, b⟩

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ inv (F.map (𝟙 j)) = 𝟙 (F.obj j)

Tactic:
grind

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

Goal state before:
pp: case left
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        left) =
    left

Tactic:
rfl

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

Goal state before:
pp: case right
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        right) =
    right

Tactic:
rfl

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

Goal state before:
pp: case left
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        left) =
    left

Tactic:
rfl

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

Goal state before:
pp: case right
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        right) =
    right

Tactic:
rfl

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

Goal state before:
pp: case false
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) false) =
    false

Tactic:
rfl

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

Goal state before:
pp: case true
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) true) =
    true

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone (pair X Y)
j : Discrete WalkingPair
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
      exacts [fac_left s, fac_right s]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone (pair X Y)
j : Discrete WalkingPair
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
      exacts [fac_left s, fac_right s]

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj none = (cospan (F.map inl) (F.map inr)).obj none

Tactic:
rfl

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.left) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.left)

Tactic:
rfl

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

Goal state before:
pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ F.obj (some WalkingPair.right) = (cospan (F.map inl) (F.map inr)).obj (some WalkingPair.right)

Tactic:
rfl

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj none = (span (F.map fst) (F.map snd)).obj none

Tactic:
rfl

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

Goal state before:
pp: case some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)

Tactic:
rfl

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

Goal state before:
pp: case some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ F.obj (some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.right)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ⟶ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ⟶ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ⟶ G.obj WalkingCospan.right
hl : F.map inl ≫ z = l ≫ G.map inl
hr : F.map inr ≫ z = r ≫ G.map inr
⊢ (X : WalkingCospan) → F.obj X ⟶ G.obj X

Tactic:
rintro (_ | _ | _); exacts [z, l, r]

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
S : D
T : C ⥤ D
x y : StructuredArrow S T
hr : x.right = y.right
hh : x.hom ≫ T.map (eqToHom hr) = y.hom
⊢ x = y

Tactic:
by
  cases x
  cases y
  cases hr
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ (X : WalkingCospan) → F.obj X ≅ G.obj X

Tactic:
rintro (_ | _ | _); exacts [z, l, r]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (X : WalkingSpan) → F.obj X ⟶ G.obj X

Tactic:
rintro (_ | _ | _); exacts [z, l, r]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ (X : WalkingSpan) → F.obj X ≅ G.obj X

Tactic:
rintro (_ | _ | _); exacts [z, l, r]

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

Goal state before:
pp: case left
⊢ left.comp (id one) = left

Tactic:
rfl

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

Goal state before:
pp: case right
⊢ right.comp (id one) = right

Tactic:
rfl

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

Goal state before:
pp: case id
X : WalkingParallelPair
⊢ (id X).comp (id X) = id X

Tactic:
rfl

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

Goal state before:
pp: case left.id.id
⊢ (left.comp (id one)).comp (id one) = left.comp ((id one).comp (id one))

Tactic:
rfl

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

Goal state before:
pp: case right.id.id
⊢ (right.comp (id one)).comp (id one) = right.comp ((id one).comp (id one))

Tactic:
rfl

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

Goal state before:
pp: case id.left.id
⊢ ((id zero).comp left).comp (id one) = (id zero).comp (left.comp (id one))

Tactic:
rfl

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

Goal state before:
pp: case id.right.id
⊢ ((id zero).comp right).comp (id one) = (id zero).comp (right.comp (id one))

Tactic:
rfl

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

Goal state before:
pp: case id.id.left
⊢ ((id zero).comp (id zero)).comp left = (id zero).comp ((id zero).comp left)

Tactic:
rfl

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

Goal state before:
pp: case id.id.right
⊢ ((id zero).comp (id zero)).comp right = (id zero).comp ((id zero).comp right)

Tactic:
rfl

Goal state after: