awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePushoutShape J
⊢ Subsingleton.{w + 1} (x ⟶ x_1)
have allEq : ∀ (a b : x ⟶ x_1), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
x x_1 : WidePushoutShape J
a b : x ⟶ x_1
⊢ a = b
have allEq : Eq.{w + 1} (α := Quiver.Hom (V := WidePushoutShape J) none none) (Hom.id none) (Hom.id none)
Tactic: casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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)
⊢ a = b
have allEq₁ : ∀ (b : J), Hom.init b = Hom.init b
Tactic: casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
⊢ a = b
have allEq₂ : ∀ (x : J), Hom.id (some x) = Hom.id (some x)
Tactic: casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)
Cleared hypotheses: x, x_1, a, b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
⊢ 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)
have 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)
Tactic: obtain - | j := f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePushoutShape J) C
j : WidePushoutShape J
⊢ F.obj j =
    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)) j
have none : 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: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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 (some j)) fun (j : J) ↦ F.map (Hom.init j)) Option.none
⊢ F.obj j =
    Functor.obj.{w, v, w, u}
      (wideSpan (F.obj Option.none) (fun (j : J) ↦ F.obj (some j)) fun (j : J) ↦ F.map (Hom.init j)) j
have some : ∀ (val : J),
  F.obj (some val) =
    Functor.obj.{w, v, w, u}
      (wideSpan (F.obj Option.none) (fun (j : J) ↦ F.obj (some j)) fun (j : J) ↦ F.map (Hom.init j)) (some val)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
j j' : WidePushoutShape J
f : j ⟶ j'
⊢ 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
      | 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)
        j with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
have none : ∀ (f : none ⟶ j'),
  Eq (α := F.obj 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
      | 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)
        none with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
Tactic: cases j
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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 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
        | 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 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
      | 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
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
have some : ∀ (val : J) (f : some val ⟶ j'),
  Eq (α := F.obj (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
      | 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
      | Option.none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
Tactic: cases j
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
j' : WidePushoutShape J
f : none ⟶ j'
⊢ Eq (α := F.obj 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
      | 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)
        none with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
have none : ∀ (f : Quiver.Hom (V := WidePushoutShape J) none none),
  Eq (α :=
    F.obj none ⟶
      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)
        none with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
Tactic: cases j'
Cleared hypotheses: j', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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)
⊢ 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)
have 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)
Tactic: cases j'
Cleared hypotheses: j', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
j' : WidePushoutShape J
val : J
f : some val ⟶ j'
⊢ Eq (α := F.obj (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
      | 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)
have some : ∀ (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 j'
Cleared hypotheses: j', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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)
⊢ 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)
have 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)
Tactic: cases j'
Cleared hypotheses: j', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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
f : Quiver.Hom (V := WidePushoutShape J) none none
⊢ Eq (α :=
    F.obj none ⟶
      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)
        none with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
have none : Eq (α :=
  F.obj none ⟶
    Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
  (F.map (Hom.id none) ≫
    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)
  (CategoryStruct.comp (Y :=
    Functor.obj.{w, v, w, u} (C := WidePushoutShape J) (Functor.obj (Functor.const (WidePushoutShape J)) X) none)
    (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)
    (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id none)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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 : none ⟶ some val
⊢ Eq (α := F.obj 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
      | 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)
        none with
      | none => f_1
      | some j => ι j) ≫
      Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) f)
have none : Eq (α := F.obj 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
    | 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) none)
    (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)
    (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.init val)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
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 val_1 : J
f : some val ⟶ some val_1
⊢ Eq (α :=
    F.obj (some val) ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (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)
        some val_1 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)
have some : Eq (α := F.obj (some val) ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some val))
  (F.map (Hom.id (some 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
    | none => f_1
    | some j => ι j)
  (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePushoutShape J)) X) (some 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
    | none => f_1
    | some j => ι j)
    (Functor.map (Functor.obj (Functor.const (WidePushoutShape J)) X) (Hom.id (some val))))
Tactic: cases f
Cleared hypotheses: val_1, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
⊢ Functor.obj (𝟭 (WidePushoutShape J)) j ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      j
have none : Iso (C := WidePushoutShape J) (Functor.obj (𝟭 (WidePushoutShape J)) none)
  (Functor.obj (C := WidePushoutShape J)
    (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
      (wideSpan none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
      (wideSpan none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
    none)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
none :
  Iso (C := WidePushoutShape J) (Functor.obj (𝟭 (WidePushoutShape J)) Option.none)
    (Functor.obj (C := WidePushoutShape J)
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      Option.none)
⊢ Functor.obj (𝟭 (WidePushoutShape J)) j ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      j
have some : (val : J) →
  Functor.obj (𝟭 (WidePushoutShape J)) (some val) ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePushoutShape J')
        (wideSpan Option.none (fun (j : J) ↦ some ((h : (a : J) → J') j)) fun (j : J) ↦ Hom.init ((h : (a : J) → J') j))
        (wideSpan Option.none (fun (j : J') ↦ some (h.invFun j)) fun (j : J') ↦ Hom.init (h.invFun j)))
      (some val)
Tactic: cases j
Cleared hypotheses: j