awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫
        Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
          Cofan.IsColimit.desc (hc (↑x : J) ⋯) fun (x_1 : (↑(p ⁻¹' {(↑x : J)}) : Type u_1)) ↦
            s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) (↑x_1 : I) ⋯))
have h : Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶ s.pt)
  (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ≫
    c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫ m)
  (Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c')
      (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) : I)
        sorry) ≫
    m)
Tactic: rw [Cofan.IsColimit.fac, Cofan.IsColimit.fac, ← hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c')
        (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)})
          (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) : I) ⋯) ≫
      m)
have h : Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶ s.pt)
  (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ≫
    c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫ m)
  (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) sorry))
      (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) :
        X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶
          Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
            (Discrete.functor (X.mapObjFun p (p i)) :
              Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
            (c (p i) sorry : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
      (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) :
        Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
            Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) : J)}) : Type u_1))
            (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) : J) sorry) ⟶
          c'.pt) ≫
    m)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) ⋯))
        (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) :
          X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶
            Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
              (Discrete.functor (X.mapObjFun p (p i)) :
                Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
              (c (p i) ⋯ : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
        (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) :
          Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
              Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J)}) : Type u_1))
              (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J) ⋯) ⟶
            c'.pt) ≫
      m)
have h : Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶ s.pt)
  (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ≫
    c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫ m)
  (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) sorry))
    (Cofan.inj (c (p i) sorry) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) :
      X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i sorry) ⟶
        Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
          (Discrete.functor (X.mapObjFun p (p i)) :
            Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
          (c (p i) sorry : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
    (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) sorry) ≫ m :
      Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) sorry) ⟶ s.pt))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
inst_3 : HasZeroMorphisms.{v_1, u_4} C
inst_4 : DecidableEq J
i : I
j : J
⊢ Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
    (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)
have pos : ∀ (h : p i = j),
  Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
    (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)
Tactic: by_cases h : p i = j
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject (goal)
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
inst_3 : HasZeroMorphisms.{v_1, u_4} C
inst_4 : DecidableEq J
i : I
j : J
pos :
  ∀ (h : p i = j),
    Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
      (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (mapMap φ p j))
      (φ i ≫ Y.ιMapObjOrZero p i j)
⊢ Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
    (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)
have neg : ∀ (h : ¬p i = j),
  Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
    (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)
Tactic: by_cases h : p i = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
⊢ (F.map g.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber
have rw : (F.map g.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber
Tactic: rw [w_base]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
w_fiber : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g
have mk : ∀ (base : X.base ⟶ Y.base) (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber)
  (w_base : { base := base, fiber := fiber : X.Hom Y }.base = g.base)
  (w_fiber : eqToHom sorry ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = g.fiber),
  { base := base, fiber := fiber : X.Hom Y } = g
Tactic: cases f
Cleared hypotheses: f, w_base, w_fiber
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base : X.base ⟶ Y.base
fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base, fiber := fiber : X.Hom Y }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = g.fiber
⊢ { base := base, fiber := fiber : X.Hom Y } = g
have mk : ∀ (base_1 : X.base ⟶ Y.base) (fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber)
  (w_base : { base := base, fiber := fiber : X.Hom Y }.base = { base := base_1, fiber := fiber_1 }.base)
  (w_fiber : eqToHom sorry ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = { base := base_1, fiber := fiber_1 }.fiber),
  { base := base, fiber := fiber : X.Hom Y } = { base := base_1, fiber := fiber_1 }
Tactic: cases g
Cleared hypotheses: g, w_base, w_fiber
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base : X.base ⟶ Y.base
fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber
base_1 : X.base ⟶ Y.base
fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base, fiber := fiber : X.Hom Y }.base = { base := base_1, fiber := fiber_1 }.base
w_fiber : eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = { base := base_1, fiber := fiber_1 }.fiber
⊢ { base := base, fiber := fiber : X.Hom Y } = { base := base_1, fiber := fiber_1 }
have mk : fiber ≍ fiber_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ comp X.id f = f
have w_base : (comp X.id f).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_base : (comp X.id f).base = f.base
⊢ comp X.id f = f
have w_fiber : eqToHom sorry ≫ (comp X.id f).fiber = f.fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ comp f Y.id = f
have w_base : (comp f Y.id).base = f.base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_base : (comp f Y.id).base = f.base
⊢ comp f Y.id = f
have w_fiber : eqToHom sorry ≫ (comp f Y.id).fiber = f.fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber
have w_fiber : eqToHom sorry ≫ eqToHom sorry ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom sorry = f.fiber
Tactic: dsimp [comp, id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom ⋯ = f.fiber
have w_fiber : eqToHom sorry ≫
    eqToHom sorry ≫
      (NatTrans.app (Iso.hom (Cat.Hom.toNatIso (eqToIso sorry) ≪≫ eqToIso sorry)) ((F.map f.base).toFunctor.obj X.fiber) ≫
          map (𝟭 (↑(F.obj Y.base) : Type u₂)) f.fiber ≫
            NatTrans.app (Iso.inv (Cat.Hom.toNatIso (eqToIso sorry) ≪≫ eqToIso sorry)) Y.fiber) ≫
        eqToHom sorry =
  f.fiber
Tactic: rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ comp (comp f g) h = comp f (comp g h)
have w_base : (comp (comp f g) h).base = (comp f (comp g h)).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
w_base : (comp (comp f g) h).base = (comp f (comp g h)).base
⊢ comp (comp f g) h = comp f (comp g h)
have w_fiber : eqToHom sorry ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber
have subst : (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
⊢ f.fiber = eqToHom ⋯ ≫ g.fiber
have subst : f.fiber = eqToHom sorry ≫ f.fiber
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ Hom.base (eqToHom h) = eqToHom ⋯
have subst : Hom.base (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ (F.map (Hom.base (eqToHom h))).toFunctor.obj X.fiber = Y.fiber
have subst : (F.map (Hom.base (eqToHom sorry))).toFunctor.obj X.fiber = X.fiber
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
h : X = Y
⊢ Hom.fiber (eqToHom h) = eqToHom ⋯
have subst : Hom.fiber (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ X.base = Y.base
have subst : X.base = X.base
Tactic: subst hF
Cleared hypotheses: Y, hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ (F.map (eqToHom ⋯)).toFunctor.obj X.fiber = Y.fiber
have subst : (F.map (eqToHom sorry)).toFunctor.obj X.fiber = X.fiber
Tactic: subst hF
Cleared hypotheses: Y, hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
hF : X = Y
⊢ eqToHom hF = { base := eqToHom ⋯, fiber := eqToHom ⋯ : X.Hom Y }
have subst : eqToHom sorry = { base := eqToHom sorry, fiber := eqToHom sorry : X.Hom X }
Tactic: subst hF
Cleared hypotheses: Y, hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber
have rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
Tactic: rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber
have rw₁ : (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber
Tactic: rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
rw₁ : (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber
have rw₂ : (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber
Tactic: rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
rw₁ : (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber
rw₂ : (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber
have rw₃ : (Cat.Hom.toFunctor (𝟙 (F.obj X.base))).obj X.fiber = X.fiber
Tactic: rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
rw : (F.map e₁.hom ≫ F.map e₁.inv).toFunctor.obj X.fiber = X.fiber
rw₁ : (F.map (e₁.hom ≫ e₁.inv)).toFunctor.obj X.fiber = X.fiber
rw₂ : (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber
rw₃ : (Cat.Hom.toFunctor (𝟙 (F.obj X.base))).obj X.fiber = X.fiber
⊢ (F.map e₁.inv).toFunctor.obj ((F.map e₁.hom).toFunctor.obj X.fiber) = X.fiber
have rw₄ : X.fiber = X.fiber
Tactic: rw [← Cat.Hom.comp_obj, ← F.map_comp,e₁.hom_inv_id,F.map_id,Cat.Hom.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ eqToHom ⋯ ≫
      Hom.fiber
        ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ : Y.Hom X } ≫
          { base := e₁.hom, fiber := e₂.hom : X.Hom Y }) =
    Hom.fiber (𝟙 Y)
have this : Eq (α :=
  Quiver.Hom (V := (↑(F.obj Y.base) : Type u₂))
    (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) Y.fiber)
    (obj (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) ((F.map e₁.hom).toFunctor.obj X.fiber)))
  (map (Cat.Hom.toFunctor ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom)) e₂.inv)
  (eqToHom sorry ≫ map (Cat.Hom.toFunctor (𝟙 (F.obj Y.base))) e₂.inv ≫ eqToHom sorry)
Tactic: have := Functor.congr_hom congr($((F.mapIso e₁).inv_hom_id).toFunctor) e₂.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)
have h_obj : ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = obj (𝟭 (Grothendieck F)) X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
h_obj : ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = obj (𝟭 (Grothendieck F)) X
⊢ map (𝟙 F) = 𝟭 (Grothendieck F)
have h_map : autoParam
  (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom sorry ≫ Functor.map (𝟭 (Grothendieck F)) f ≫ eqToHom sorry)
  ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (𝟙 F)).map f = eqToHom ⋯ ≫ Functor.map (𝟭 (Grothendieck F)) f ≫ eqToHom ⋯
have h_map : { base := f.base, fiber := f.fiber : ((map (𝟙 F)).obj X).Hom ((map (𝟙 F)).obj Y) } = f
Tactic: simp [map_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ map (α ≫ β) = map α ⋙ map β
have h_obj : ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
h_obj : ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X
⊢ map (α ≫ β) = map α ⋙ map β
have h_map : autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom sorry ≫ (map α ⋙ map β).map f ≫ eqToHom sorry)
  ext._auto_1
Tactic: fapply Functor.ext