awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        none ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none)
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) none)
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app none)
have none : Eq (α :=
  Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
      ((D.mapGlueData F).vPullbackCone i j) ⟶
    (D.mapGlueData F).glued)
  (PullbackCone.fst ((D.mapGlueData F).vPullbackCone i j) ≫ (D.mapGlueData F).ι i)
  (F.map (D.f i j) ≫ (D.mapGlueData F).ι i)
Tactic: simp [e]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        (some WalkingPair.left) ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj
        (some WalkingPair.left))
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.left))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (some WalkingPair.left))
have some : NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.left) = F.map (D.f i j)
Tactic: simp [e]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        (some WalkingPair.right) ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj
        (some WalkingPair.right))
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.right))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (some WalkingPair.right))
have some : NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.right) = F.map (D.t i j) ≫ F.map (D.f j i)
Tactic: simp [e]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
⊢ ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x
have obtain : ∀ (i : (D.mapGlueData F).J) (y : (D.mapGlueData F).U i)
  (eq :
    Eq (α := (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
            (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
          y :
        (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
            (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
          x :
        (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)),
  ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x
Tactic: obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq :
  Eq (α := (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
          (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        y :
      (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
          (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        x :
      (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
⊢ ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x
have eq₁ : Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
        (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
            (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
          y :
        (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
        (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
            (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
          x :
        (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
Tactic: replace eq := congr_arg e.inv eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
              (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            y :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
              (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            x :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
⊢ ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x
have eq₁ : Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i ≫ e.inv) :
        (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      y :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom ≫ e.inv) :
        (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      x :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
Tactic: change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i ≫ e.inv) :
          (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom ≫ e.inv) :
          (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        x :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
⊢ ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x
have eq₁ : Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
        (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      y :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj D.glued)) :
        (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
      x :
    (fun (X : Type v) ↦ X) (F.obj D.glued))
Tactic: rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j : D.J
⊢ Mono.{v, u₁} (C := C) (X := if h : i = j then D.U i else D.V i j h) (Y := D.U i)
    (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)
have pos : ∀ (h : i = j), Mono.{v, u₁} (eqToHom sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j : D.J
pos : ∀ (h : i = j), Mono.{v, u₁} (eqToHom ⋯)
⊢ Mono.{v, u₁} (C := C) (X := if h : i = j then D.U i else D.V i j h) (Y := D.U i)
    (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)
have neg : ∀ (h : ¬i = j), Mono (eqToHom sorry ≫ D.f i j h)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i : D.J
⊢ IsIso (D.f' i i)
have simp : IsIso.{v, u₁} (eqToHom sorry)
Tactic: simp only [GlueData'.f', ↓reduceDIte]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : i = j
⊢ HasPullback (D.f' i j) (D.f' i k)
have inst : IsIso (D.f' i j)
Tactic: apply +allowSynthFailures hasPullback_of_left_iso
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : i = j
⊢ IsIso (D.f' i j)
have inst : IsIso.{v, u₁} (eqToHom sorry)
Tactic: simp only [GlueData'.f', dif_pos hij]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ HasPullback (D.f' i j) (D.f' i k)
have inst : IsIso (D.f' i k)
Tactic: apply +allowSynthFailures hasPullback_of_right_iso
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (D.f' i k)
have inst : IsIso.{v, u₁} (eqToHom sorry)
Tactic: simp only [GlueData'.f', dif_pos hik]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
X Y Z : C
f : X ⟶ Y
e : Z = X
⊢ eqToHom e ≫ f ≍ f
have subst : ∀ (f : Z ⟶ Y), eqToHom sorry ≫ f ≍ f
Tactic: subst e
Cleared hypotheses: X, f, e
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (hypothesis)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
⊢ HasPullback (D.f' i j) (D.f' i k)
have this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
Tactic: have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
⊢ HasPullback (D.f' i j) (D.f' i k)
have h : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
Tactic: convert! D.f_hasPullback i j k hij hik
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
h : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
⊢ HasPullback (D.f' i j) (D.f' i k)
have h₁ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik
Tactic: convert! D.f_hasPullback i j k hij hik
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
h : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
h₁ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik
⊢ HasPullback (D.f' i j) (D.f' i k)
have h₂ : (if h : i = j then D.U i else D.V i j h) = D.V i j hij → D.f' i j ≍ D.f i j hij
Tactic: convert! D.f_hasPullback i j k hij hik
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
h : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
h₁ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik
h₂ : (if h : i = j then D.U i else D.V i j h) = D.V i j hij → D.f' i j ≍ D.f i j hij
⊢ HasPullback (D.f' i j) (D.f' i k)
have h₃ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik → D.f' i k ≍ D.f i k hik
Tactic: convert! D.f_hasPullback i j k hij hik
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
⊢ HasPullback (D.f' i j) (D.f' i k)
have if : ∀ (hik : i = k), HasPullback (D.f' i j) (D.f' i k)
Tactic: if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
if : ∀ (hik : i = k), HasPullback (D.f' i j) (D.f' i k)
⊢ HasPullback (D.f' i j) (D.f' i k)
have if₁ : ∀ (hik : ¬i = k), HasPullback (D.f' i j) (D.f' i k)
Tactic: if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
⊢ HasPullback (D.f' i j) (D.f' i k)
have if : ∀ (hij : i = j), HasPullback (D.f' i j) (D.f' i k)
Tactic: if hij : i = j then
    apply +allowSynthFailures hasPullback_of_left_iso
    simp only [GlueData'.f', dif_pos hij]
    infer_instance
  else if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
if : ∀ (hij : i = j), HasPullback (D.f' i j) (D.f' i k)
⊢ HasPullback (D.f' i j) (D.f' i k)
have if₁ : ∀ (hij : ¬i = j), HasPullback (D.f' i j) (D.f' i k)
Tactic: if hij : i = j then
    apply +allowSynthFailures hasPullback_of_left_iso
    simp only [GlueData'.f', dif_pos hij]
    infer_instance
  else if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]