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
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)
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)
⊢ 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)

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} (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)
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)
⊢ 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)

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} (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
f : Quiver.Hom (V := WidePullbackShape J) Option.none Option.none
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)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (C := WidePullbackShape J) (Functor.obj (Functor.const (WidePullbackShape J)) X)
        Option.none)
      (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) (Hom.id Option.none))
      (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 (Hom.id 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)

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} (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 : none ⟶ some val
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (C := WidePullbackShape J) (Functor.obj (Functor.const (WidePullbackShape J)) X) 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
      | 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 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} (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
val : J
f : Option.some val ⟶ none
some :
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) (Option.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
      | 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 (Hom.term val))
⊢ 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)

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} (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
val val_1 : J
f : Option.some val ⟶ Option.some val_1
some :
  Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) (Option.some val) ⟶
      F.obj (Option.some val))
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (WidePullbackShape J)) X) (Option.some val))
      (Functor.map (Functor.obj (Functor.const (WidePullbackShape J)) X) (Hom.id (Option.some val)))
      (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))
    ((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 (Hom.id (Option.some val)))
⊢ 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 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} (WidePullbackShape J) C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ 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
      | 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
      | some j => π j) ≫
      F.map (Hom.id none))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePullbackShape J) C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val : J
⊢ 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
      | 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
      | some j => π j) ≫
      F.map (Hom.term val))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
F : Functor.{w, v, w, u} (WidePullbackShape J) C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val : J
⊢ 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
      | 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
      | some j => π j) ≫
      F.map (Hom.id (some val)))

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
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) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.term ((h : (a : J) → J') j))
        (wideCospan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j)))
      Option.none)
some :
  (val : J) →
    Functor.obj (𝟭 (WidePullbackShape J)) (Option.some val) ≅
      Functor.obj
        (Functor.comp.{w, w', w, w, w', w} (D := WidePullbackShape J')
          (wideCospan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
            Hom.term ((h : (a : J) → J') j))
          (wideCospan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j)))
        (Option.some val)
⊢ Functor.obj (𝟭 (WidePullbackShape J)) j ≅
    Functor.obj
      (Functor.comp.{w, w', w, w, w', w} (D := WidePullbackShape J')
        (wideCospan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.term ((h : (a : J) → J') j))
        (wideCospan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j)))
      j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Eq.{w + 1} (α := 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ 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:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J
⊢ Functor.obj (𝟭 (WidePullbackShape J)) (some val) =
    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)))
      (some val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : J
⊢ Functor.obj (𝟭 (WidePullbackShape J)) (some val) ≅
    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)))
      (some val)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
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') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j))
        (wideCospan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.term ((h : (a : J) → J') j)))
      Option.none)
    (Functor.obj (𝟭 (WidePullbackShape J')) Option.none)
some :
  (val : J') →
    Functor.obj
        (Functor.comp.{w', w, w', w', w, w'} (D := WidePullbackShape J)
          (wideCospan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j))
          (wideCospan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
            Hom.term ((h : (a : J) → J') j)))
        (Option.some val) ≅
      Functor.obj (𝟭 (WidePullbackShape J')) (Option.some val)
⊢ Functor.obj
      (Functor.comp.{w', w, w', w', w, w'} (D := WidePullbackShape J)
        (wideCospan Option.none (fun (j : J') ↦ Option.some (h.invFun j)) fun (j : J') ↦ Hom.term (h.invFun j))
        (wideCospan Option.none (fun (j : J) ↦ Option.some ((h : (a : J) → J') j)) fun (j : J) ↦
          Hom.term ((h : (a : J) → J') j)))
      j ≅
    Functor.obj (𝟭 (WidePullbackShape J')) j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ Eq.{w' + 1} (α := 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ 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:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : 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)))
      (some val) =
    Functor.obj (𝟭 (WidePullbackShape J')) (some val)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val : 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)))
      (some val) ≅
    Functor.obj (𝟭 (WidePullbackShape J')) (some val)

Tactic:
exact eqToIso (by simp)

Premises used: CategoryTheory.eqToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
ι : Type u_1
ι' : Type u_2
e : ι ≃ ι'
⊢ (equivalenceOfEquiv ι' e).functor.obj none = none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
ι : Type u_1
ι' : Type u_2
e : ι ≃ ι'
i : ι
⊢ (equivalenceOfEquiv ι' e).functor.obj (some i) = some ((e : (a : ι) → ι') i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
Goal:
ι : Type u_1
ι' : Type u_2
e : ι ≃ ι'
i : ι
⊢ (equivalenceOfEquiv ι' e).functor.map (Hom.term i) = Hom.term ((e : (a : ι) → ι') i)

Tactic:
rfl

Premises used: rfl