mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : K ≌ J
s : Cone (e.functor ⋙ F)
k : K
⊢ (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app k =
    (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt).hom ≫
      ((𝟭 (Cone (e.functor ⋙ F))).obj s).π.app k

Tactic:
simpa [e.counit_app_functor] using s.w (e.unitInv.app k)

Goal state after:
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
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j j' : WidePullbackShape J
f : j ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match j with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j' : WidePullbackShape J
f : none ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
j' : WidePullbackShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match some val✝ with
      | none => f✝
      | some j => π j) ≫
      F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj j ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      j

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePullbackShape J)).obj none ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePullbackShape J)).obj (some val✝) ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      j ≅
    (𝟭 (WidePullbackShape J')).obj j

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      none ≅
    (𝟭 (WidePullbackShape J')).obj none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePullbackShape J')).obj (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

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

Tactic:
cases j

Goal state after:
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

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: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j j' : WidePushoutShape J
f : j ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match j with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j' : WidePushoutShape J
f : none ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match none with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j' : WidePushoutShape J
val✝ : J
f : some val✝ ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match some val✝ with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
⊢ (𝟭 (WidePushoutShape J)).obj j ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      j

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePushoutShape J)).obj none ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePushoutShape J)).obj (some val✝) ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      j ≅
    (𝟭 (WidePushoutShape J')).obj j

Tactic:
cases j

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      none ≅
    (𝟭 (WidePushoutShape J')).obj none

case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) ≅
    (𝟭 (WidePushoutShape J')).obj (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
⊢ lift t ≫ s.π.app j = t.π.app j

Tactic:
cases j

Goal state after:
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
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ lift t ≫ s.π.app none = t.π.app none

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
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

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

Tactic:
cases j

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

case right
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        right) =
    right
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

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

Tactic:
cases j

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

case right
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        right) =
    right
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 Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv

Tactic:
simpa [← cancel_mono e.hom] using hm default

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

Goal state before:
pp: case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
rw [← cancel_epi f]

Goal state after:
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ f ≫ c.inl ≫ m = f ≫ c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ inl ≫ i₁ = inl ≫ i₂

Tactic:
rw [← cancel_epi f]

Goal state after:
case h₁
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ f ≫ inl ≫ i₁ = f ≫ inl ≫ i₂
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
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
w : m ≫ s.swap.π.app { as := WalkingPair.swap j } = t.π.app { as := WalkingPair.swap j }
⊢ m ≫ s.π.app { as := j } = (BinaryFan.swap t).π.app { as := j }

Tactic:
cases j

Goal state after:
case left
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
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.left } = t.π.app { as := WalkingPair.swap WalkingPair.left }
⊢ m ≫ s.π.app { as := WalkingPair.left } = (BinaryFan.swap t).π.app { as := WalkingPair.left }

case right
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
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
w : m ≫ s.swap.π.app { as := WalkingPair.swap WalkingPair.right } = t.π.app { as := WalkingPair.swap WalkingPair.right }
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.swap t).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

Goal state after:
case none.none.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id none) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

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

Goal state before:
pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : none ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

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

Goal state before:
pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

Goal state after:
case some.left.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.left) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

Goal state after:
case some.left.some.left.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.left))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

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

Goal state before:
pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ none
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

Goal state after:
case some.right.none.term
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (term WalkingPair.right) ≫
      Option.casesOn none (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (term WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.left) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

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

Goal state before:
pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
j : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (((Functor.const WalkingCospan).obj W).map j ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map j

Tactic:
cases j

Goal state after:
case some.right.some.right.id
C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ (((Functor.const WalkingCospan).obj W).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
    (Option.casesOn (some WalkingPair.right) (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫
      (cospan f g).map (WidePullbackShape.Hom.id (some WalkingPair.right))
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Over X
⊢ Hom.left (mkIdTerminal.from Y) = Y.hom

Tactic:
rw [mkIdTerminal.hom_ext (mkIdTerminal.from Y) (homMk Y.hom)]

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
Y : Over X
⊢ Hom.left (homMk Y.hom ⋯) = Y.hom
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
⊢ (Hom.left f ≫ Y.hom).unop = Z.hom.unop

Tactic:
Over.w

Goal state after:
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
⊢ Z.hom.unop = Z.hom.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: j : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).obj j = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j

Tactic:
cases j

Goal state after:
case zero
⊢ (𝟭 WalkingParallelPair).obj zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero

case one
⊢ (𝟭 WalkingParallelPair).obj one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op.zero
j : WalkingParallelPair
f : op zero ⟶ op j
g : unop (op j) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
cases j

Goal state after:
case op.op.zero.zero
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.zero.one
f : op zero ⟶ op one
g : unop (op one) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op