mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
s : ColimitCocone (E ⋙ F)
t : ColimitCocone F
⊢ pre F E = (isoColimitCocone s).hom ≫ s.isColimit.desc (Cocone.whisker E t.cocone) ≫ (isoColimitCocone t).inv

Tactic:
cat_disch

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
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:
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:
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.LeftInverse (fun g ↦ colimit.desc f { pt := c, ι := g }) fun g ↦
    { app := fun x ↦ colimit.ι f x ≫ g, naturality := ⋯ }

Tactic:
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:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w

Goal state after:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g : widePushout B objs arrows ⟶ X
⊢ g = desc (head arrows ≫ g) (fun j ↦ ι arrows j ≫ g) ⋯

Tactic:
cat_disch

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

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

Tactic:
intro t m h
    refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_
    erw [hc.fac, (hs a).fac]
    simpa using! h ⟨a, b⟩

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2

Tactic:
intro h1 h2
  apply colimit.hom_ext
  rintro (_ | _)
  · apply h2
  · apply h1

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:
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:
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:
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:
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:
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:
cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct g
p p' : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → f (p' b) ⟶ g b
hp : p = p'
hq : ∀ (b : β), eqToHom ⋯ ≫ q b = q' b
⊢ map' p q = map' p' q'

Tactic:
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:
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:
cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
p p' : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (a : α) → f a ⟶ g (p' a)
hp : p = p'
hq : ∀ (a : α), q a ≫ eqToHom ⋯ = q' a
⊢ map' p q = map' p' q'

Tactic:
cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op).unop = ((Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝).unop

Tactic:
cat_disch

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : C
x✝ : Type v
⊢ ((piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
        { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝)).unop =
    (𝟙 ((piConst.obj X).rightOp.obj x✝)).unop

Tactic:
cat_disch

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProductsOfShape α C
a : α
⊢ (piEquivalenceFunctorDiscreteCompLim α).hom ≫ Pi.functorπ a =
    (piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (lim.π { as := a }) ≫
      (piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom

Tactic:
cat_disch

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproductsOfShape α C
a : α
⊢ (piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (colim.ι { as := a }) ≫
      (piEquivalenceFunctorDiscreteCompColim α).hom =
    (piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom ≫ Sigma.functorι a

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]

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 S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
⊢ f = mk (f.hom ≫ T.map (𝟙 f.right))

Tactic:
cat_disch

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

Goal state before:
pp: case mk.mk.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
left✝¹ : Discrete PUnit.{1}
right✝ : C
hom✝¹ : (Functor.fromPUnit S).obj left✝¹ ⟶ T.obj right✝
left✝ : Discrete PUnit.{1}
hom✝ : (Functor.fromPUnit S).obj left✝ ⟶ T.obj right✝
hh :
  hom { left := left✝¹, right := right✝, hom := hom✝¹ } ≫ T.map (eqToHom ⋯) =
    hom { left := left✝, right := right✝, hom := hom✝ }
⊢ { left := left✝¹, right := right✝, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
cat_disch

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

Goal state before:
pp: case none.none.id
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
⊢ (F.map (WidePullbackShape.Hom.id none) ≫ Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (WidePullbackShape.Hom.id none)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.none.term
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
⊢ (F.map (term WalkingPair.left) ≫ Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (term WalkingPair.left)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.some.left.id
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
⊢ (F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePullbackShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.none.term
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
⊢ (F.map (term WalkingPair.right) ≫ Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (term WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.some.right.id
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
⊢ (F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

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

Goal state before:
pp: case none.none.id
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
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map (WidePullbackShape.Hom.id none)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.none.term
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
⊢ F.map (term WalkingPair.left) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map (term WalkingPair.left)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.some.left.id
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
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (WidePullbackShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.none.term
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
⊢ F.map (term WalkingPair.right) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (term WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.some.right.id
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
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

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

Goal state before:
pp: case none.none.id
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
⊢ (F.map (WidePushoutShape.Hom.id none) ≫ Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (WidePushoutShape.Hom.id none)

Tactic:
cat_disch

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

Goal state before:
pp: case none.some.left.init
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
⊢ (F.map (init WalkingPair.left) ≫ Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (init WalkingPair.left)

Tactic:
cat_disch

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

Goal state before:
pp: case none.some.right.init
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
⊢ (F.map (init WalkingPair.right) ≫ Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (init WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: case some.left.some.left.id
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
⊢ (F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
cat_disch

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

Goal state before:
pp: case some.right.some.right.id
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
⊢ (F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
cat_disch

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

Goal state before:
pp: case none.none.id
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
⊢ F.map (WidePushoutShape.Hom.id none) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ G.map (WidePushoutShape.Hom.id none)

Tactic:
cat_disch

Goal state after: