awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
F G : Functor.{u_1, v, u_1, u} (WidePullbackShape ι) C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X Y : WidePullbackShape ι
f : X ⟶ Y
id :
  F.map (Hom.id X) ≫
      Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          X) =
    Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          X) ≫
      G.map (Hom.id X)
term :
  ∀ (j : ι),
    F.map (Hom.term j) ≫
        Iso.hom
          ((fun (i : WidePullbackShape ι) ↦
              (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
                | none => base
                | some i => comp i :
                F.obj i ≅ G.obj i))
            none) =
      Iso.hom
          ((fun (i : WidePullbackShape ι) ↦
              (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
                | none => base
                | some i => comp i :
                F.obj i ≅ G.obj i))
            (some j)) ≫
        G.map (Hom.term j)
⊢ F.map f ≫
      Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          Y) =
    Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          X) ≫
      G.map f

Tactic:
rcases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
F G : Functor.{u_1, v, u_1, u} (WidePullbackShape ι) C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X : WidePullbackShape ι
⊢ F.map (Hom.id X) ≫
      Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          X) =
    Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          X) ≫
      G.map (Hom.id X)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
ι : Type u_1
F G : Functor.{u_1, v, u_1, u} (WidePullbackShape ι) C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
j : ι
⊢ F.map (Hom.term j) ≫
      Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          none) =
    Iso.hom
        ((fun (i : WidePullbackShape ι) ↦
            (match (motive := (i : WidePullbackShape ι) → F.obj i ≅ G.obj i) i with
              | none => base
              | some i => comp i :
              F.obj i ≅ G.obj i))
          (some j)) ≫
      G.map (Hom.term j)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X Y Z : WidePushoutShape J
f : X.Hom Y
g : Y.Hom Z
id : (g : X.Hom Z) → X.Hom Z
init : (j : J) → (g : Hom (some j) Z) → Hom none Z
⊢ X.Hom Z

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X Z : WidePushoutShape J
g : X.Hom Z
⊢ X.Hom Z

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
Z : WidePushoutShape J
j : J
g : Hom (some j) Z
init : Hom none (some j)
⊢ Hom none Z

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
j : J
⊢ Hom none (some j)

Tactic:
apply Hom.init _

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
x x_1 : WidePushoutShape J
allEq : ∀ (a b : x ⟶ x_1), a = b
⊢ Subsingleton.{w + 1} (x ⟶ x_1)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
x x_1 : WidePushoutShape J
a b : x ⟶ x_1
allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePushoutShape J) none none) (Hom.id none) (Hom.id none)
allEq₁ : ∀ (b : J), Hom.init b = Hom.init b
allEq₂ : ∀ (x : J), Hom.id (some x) = Hom.id (some x)
⊢ a = b

Tactic:
casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)

Premises used: CategoryTheory.Limits.WidePushoutShape
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Quiver.Hom (V := WidePushoutShape J) none none) (Hom.id none) (Hom.id none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
b : J
⊢ Hom.init b = Hom.init b

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
⊢ Eq.{w + 1} (α := Quiver.Hom (V := WidePushoutShape J) none none) (Hom.id none) (Hom.id none)

Tactic:
repeat rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
X : WidePushoutShape J
⊢ Hom.id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X Y : WidePushoutShape J
f : X ⟶ Y
id :
  Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
init :
  (j : J) →
    Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
      (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C)
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) Y B objs : C)

Tactic:
obtain - | j := f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X : WidePushoutShape J
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) X B objs : C)

Tactic:
apply 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j : J
⊢ Quiver.Hom.{v, u} (V := C) (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) none B objs : C)
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ C) (some j) B objs : C)

Tactic:
exact arrows j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j : J
⊢ @Hom.rec _
      (fun (a a_1 : WidePushoutShape J) (x : a.Hom a_1) ↦
        (h : none = a) → (h : some j = a_1) → (h : HEq (α := none ⟶ some j) (Hom.init j ≫ 𝟙 (some j)) x) → B ⟶ objs j)
      (fun (X : WidePushoutShape J) (h : none = X) ↦
        Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : none = x) ↦
          (h : some j = x) → (h : HEq (α := none ⟶ some j) (Hom.init j ≫ 𝟙 (some j)) (β := x.Hom x) (𝟙 x)) → B ⟶ objs j)
          (fun (h : some j = none) ↦
            Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : none = x) ↦
              (f : none ⟶ x) →
                (h : HEq f (β := Hom (J := J) none none) (𝟙 none : Quiver.Hom (V := WidePushoutShape J) none none)) →
                  B ⟶ Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x)
              (fun (f : Quiver.Hom (V := WidePushoutShape J) none none)
                  (h : HEq f (β := Hom (J := J) none none) (𝟙 none : Quiver.Hom (V := WidePushoutShape J) none none)) ↦
                𝟙 B)
              ⋯ (Hom.init j ≫ 𝟙 (some j)))
          h)
      (fun (j_1 : J) (h : Eq.{w + 1} (α := WidePushoutShape J) none none) (h_1 : some j = some j_1) ↦
        Eq.rec (motive := fun (x : WidePushoutShape J) (x_1 : some j_1 = x) ↦
          (f : none ⟶ x) →
            (h : f ≍ Hom.init j_1) →
              B ⟶ Option.rec (motive := fun (x : WidePushoutShape J) ↦ C) B (fun (val : J) ↦ objs val) x)
          (fun (f : none ⟶ some j_1) (h : f ≍ Hom.init j_1) ↦ arrows j_1) ⋯ (Hom.init j ≫ 𝟙 (some j)))
      none (some j) (Hom.init j ≫ 𝟙 (some j)) ⋯ ⋯ ⋯ =
    arrows j

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
j : WidePushoutShape J
none :
  F.obj Option.none =
    Functor.obj.{w, v, w, u} (C := WidePushoutShape J)
      (wideSpan (F.obj Option.none) (fun (j : J) ↦ F.obj (Option.some j)) fun (j : J) ↦ F.map (Hom.init j)) Option.none
some :
  ∀ (val : J),
    F.obj (Option.some val) =
      Functor.obj.{w, v, w, u}
        (wideSpan (F.obj Option.none) (fun (j : J) ↦ F.obj (Option.some j)) fun (j : J) ↦ F.map (Hom.init j))
        (Option.some val)
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (wideSpan (F.obj Option.none) (fun (j : J) ↦ F.obj (Option.some j)) fun (j : J) ↦ F.map (Hom.init j)) j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
⊢ F.obj none =
    Functor.obj.{w, v, w, u} (C := WidePushoutShape J)
      (wideSpan (F.obj none) (fun (j : J) ↦ F.obj (some j)) fun (j : J) ↦ F.map (Hom.init j)) none

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
⊢ F.obj none =
    Functor.obj.{w, v, w, u} (C := WidePushoutShape J)
      (wideSpan (F.obj none) (fun (j : J) ↦ F.obj (some j)) fun (j : J) ↦ F.map (Hom.init j)) none

Tactic:
repeat rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj Option.none ⟶ X
ι : (j : J) → F.obj (Option.some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
j j' : WidePushoutShape J
f : j ⟶ j'
none :
  ∀ (f : Option.none ⟶ j'),
    Eq (α := F.obj Option.none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j')
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          j' with
        | Option.none => f_1
        | Option.some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.none with
        | Option.none => f_1
        | Option.some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
some :
  ∀ (val : J) (f : Option.some val ⟶ j'),
    Eq (α := F.obj (Option.some val) ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j')
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          j' with
        | Option.none => f_1
        | Option.some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.some val with
        | Option.none => f_1
        | Option.some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
⊢ Eq (α := F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j')
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        j' with
      | Option.none => f_1
      | Option.some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        j with
      | Option.none => f_1
      | Option.some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj Option.none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
j' : WidePushoutShape J
f : Option.none ⟶ j'
none :
  ∀ (f : Quiver.Hom (V := WidePushoutShape J) Option.none Option.none),
    Eq (α :=
      F.obj Option.none ⟶
        Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X)
          Option.none)
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.none with
        | Option.none => f_1
        | some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.none with
        | Option.none => f_1
        | some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
none₁ :
  ∀ (val : J) (f : Option.none ⟶ some val),
    Eq (α :=
      F.obj Option.none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          some val with
        | Option.none => f_1
        | some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.none with
        | Option.none => f_1
        | some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
⊢ Eq (α := F.obj Option.none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j')
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        j' with
      | Option.none => f_1
      | some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases j'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj none ⟶ X
ι : (j : J) → F.obj (Option.some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
j' : WidePushoutShape J
val : J
f : Option.some val ⟶ j'
some :
  ∀ (f : Option.some val ⟶ none),
    Eq (α :=
      F.obj (Option.some val) ⟶
        Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          none with
        | none => f_1
        | Option.some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.some val with
        | none => f_1
        | Option.some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
some₁ :
  ∀ (val_1 : J) (f : Option.some val ⟶ Option.some val_1),
    Eq (α :=
      F.obj (Option.some val) ⟶
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (Option.some val_1))
      (F.map f ≫
        match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.some val_1 with
        | none => f_1
        | Option.some j => ι j)
      ((match (motive :=
          (j : WidePushoutShape J) →
            F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
          Option.some val with
        | none => f_1
        | Option.some j => ι j) ≫
        Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
⊢ Eq (α := F.obj (Option.some val) ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j')
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        j' with
      | none => f_1
      | Option.some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.some val with
      | none => f_1
      | Option.some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases j'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj Option.none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
f : Quiver.Hom (V := WidePushoutShape J) Option.none Option.none
none :
  Eq (α :=
    F.obj Option.none ⟶
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X)
        Option.none)
    (F.map (Hom.id Option.none) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X)
        Option.none)
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id Option.none)))
⊢ Eq (α :=
    F.obj Option.none ⟶
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X)
        Option.none)
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj Option.none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
val : J
f : Option.none ⟶ some val
none :
  Eq (α := F.obj Option.none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
    (F.map (Hom.init val) ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | Option.none => f_1
      | some j => ι j)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X)
        Option.none)
      (match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j)
      (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.init val)))
⊢ Eq (α := F.obj Option.none ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | Option.none => f_1
      | some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        Option.none with
      | Option.none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
X : C
f_1 : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f_1
val : J
f : some val ⟶ none
⊢ Eq (α :=
    F.obj (some val) ⟶
      Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
    (F.map f ≫
      match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        none with
      | none => f_1
      | some j => ι j)
    ((match (motive :=
        (j : WidePushoutShape J) →
          F.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) j)
        some val with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)

Tactic:
cases f