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