awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
⊢ (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) (Cover.Arrow.map i h1) =
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ }
have h : ∀ (Y : C) (f : Y ⟶ X) (hf : (↑(unop (op S)) : Sieve X).arrows f)
  (e :
    (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y)))
        { Y := Y, f := f, hf := hf : (unop (op S)).Arrow } =
      (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }),
  CD (((unop (op S)).index P).left { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }) =
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.Y)) →
    (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y))) ({ Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.map h1) =
      (↑x : (I : S_1.Arrow) → ToType (P.obj (op I.Y)))
        { Y := { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.Y,
          f := { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.f, hf := sorry }
Tactic: cases i
Cleared hypotheses: i, e, e_1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι ((unop (op S)).index P) i) :
        (a : CD (multiequalizer ((unop (op S)).index P))) → CD (((unop (op S)).index P).left i))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.diagram P X).map h2.op) :
            (a : CD ((J.diagram P X).obj (op T))) → CD ((J.diagram P X).obj (op S)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
        CD ((J.diagram P X).obj (op S))) =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
have h : (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
      (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
    ((ConcreteCategory.hom (FC := FD) (CC := CD)
            (Multiequalizer.lift (S.index P) (multiequalizer (T.index P))
              (fun (I : S.Arrow) ↦ Multiequalizer.ι (T.index P) (I.map h2)) sorry) :
          (a : CD (multiequalizer (T.index P))) → CD (multiequalizer (S.index P)))
        ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
          ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
      CD (multiequalizer (S.index P))) =
  (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := sorry : T.Arrow }
Tactic: dsimp [diagram]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (FC := FD) (CC := CD) (Multiequalizer.ι (S.index P) i) :
        (a : CD (multiequalizer (S.index P))) → CD (P.obj (op i.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD)
              (Multiequalizer.lift (S.index P) (multiequalizer (T.index P))
                (fun (I : S.Arrow) ↦ Multiequalizer.ι (T.index P) (I.map h2)) ⋯) :
            (a : CD (multiequalizer (T.index P))) → CD (multiequalizer (S.index P)))
          ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
            ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) :
        CD (multiequalizer (S.index P))) =
    (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : T.Arrow }
have h : ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (Multiequalizer.ι (T.index P) (Cover.Arrow.map i h2)) :
        FD (multiequalizer (T.index P)) (P.obj (op i.Y))) :
      (a : CD (multiequalizer (T.index P))) → CD (P.obj (op i.Y)))
    ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) =
  (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := sorry : T.Arrow }
Tactic: rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
⊢ ((@ConcreteCategory.hom.{t, w', w, u_1} _ inst_1 FD CD _ _ _ _ (Multiequalizer.ι (T.index P) (Cover.Arrow.map i h2)) :
          FD (multiequalizer (T.index P)) (P.obj (op i.Y))) :
        (a : CD (multiequalizer (T.index P))) → CD (P.obj (op i.Y)))
      ((Equiv.symm (Meq.equiv (FD := FD) (CD := CD) P T) : (a : Meq P T) → ToType (multiequalizer (T.index P))) y :
        ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (multiequalizer (T.index P))) =
    (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ : T.Arrow }
have h : (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) (Cover.Arrow.map i h2) =
  (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := sorry }
Tactic: erw [Meq.equiv_symm_eq_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S_1 T : J.Cover X
x : Meq (FD := FD) (CD := CD) P S_1
y : Meq (FD := FD) (CD := CD) P T
S : J.Cover X
h1 : S ⟶ S_1
h2 : S ⟶ T
i : (unop (op S)).shape.L
e :
  (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i =
    (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) i
e_1 : CD (((unop (op S)).index P).left i) = ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op i.Y))
⊢ (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) (Cover.Arrow.map i h2) =
    (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) { Y := i.Y, f := i.f, hf := ⋯ }
have h : ∀ (Y : C) (f : Y ⟶ X) (hf : (↑(unop (op S)) : Sieve X).arrows f)
  (e :
    (↑(x.refine (FD := FD) (CD := CD) h1) : (I : S.Arrow) → ToType (P.obj (op I.Y)))
        { Y := Y, f := f, hf := hf : (unop (op S)).Arrow } =
      (↑(y.refine (FD := FD) (CD := CD) h2) : (I : S.Arrow) → ToType (P.obj (op I.Y))) { Y := Y, f := f, hf := hf }),
  CD (((unop (op S)).index P).left { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }) =
      ToType.{t, w', w, u_1} (FC := FD) (CC := CD) (P.obj (op { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.Y)) →
    (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y))) ({ Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.map h2) =
      (↑y : (I : T.Arrow) → ToType (P.obj (op I.Y)))
        { Y := { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.Y,
          f := { Y := Y, f := f, hf := hf : (unop (op S)).Arrow }.f, hf := sorry }
Tactic: cases i
Cleared hypotheses: i, e, e_1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
x y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          x :
        CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          y :
        CD ((J.plusObj P).obj (op I.Y)))
⊢ x = y
have obtain : ∀ (Sx : J.Cover X) (x : Meq (FD := FD) (CD := CD) P Sx)
  (h :
    ∀ (I : S.Arrow),
      Eq (α := CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            (mk (FD := FD) (CD := CD) x) :
          CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            y :
          CD ((J.plusObj P).obj (op I.Y)))),
  mk (FD := FD) (CD := CD) x = y
Tactic: obtain ⟨Sx, x, rfl⟩ := exists_rep x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S : J.Cover X
y : ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))
Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          (mk (FD := FD) (CD := CD) x) :
        CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          y :
        CD ((J.plusObj P).obj (op I.Y)))
⊢ mk (FD := FD) (CD := CD) x = y
have obtain : ∀ (Sy : J.Cover X) (y : Meq (FD := FD) (CD := CD) P Sy)
  (h :
    ∀ (I : S.Arrow),
      Eq (α := CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            (mk (FD := FD) (CD := CD) x) :
          CD ((J.plusObj P).obj (op I.Y)))
        ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
              (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
            (mk (FD := FD) (CD := CD) y) :
          CD ((J.plusObj P).obj (op I.Y)))),
  Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
Tactic: obtain ⟨Sy, y, rfl⟩ := exists_rep y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          (mk (FD := FD) (CD := CD) x) :
        CD ((J.plusObj P).obj (op I.Y)))
      ((ConcreteCategory.hom (FC := FD) (CC := CD) ((J.plusObj P).map I.f.op) :
            (a : CD ((J.plusObj P).obj (op X))) → CD ((J.plusObj P).obj (op I.Y)))
          (mk (FD := FD) (CD := CD) y) :
        CD ((J.plusObj P).obj (op I.Y)))
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
have h₁ : ∀ (I : S.Arrow),
  Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
    (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
Tactic: simp only [res_mk_eq_mk_pullback] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
have choose : ∀ (W : (I : S.Arrow) → J.Cover I.Y) (h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx)
  (h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy)
  (hh :
    ∀ (I : S.Arrow),
      (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
        (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)),
  Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
Tactic: choose W h1 h2 hh using fun I : S.Arrow => (eq_mk_iff_exists _ _).mp (h I)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
⊢ Eq (α := ToType.{t, w', w, u_1} (FC := FD) (CC := CD) ((J.plusObj P).obj (op X))) (mk (FD := FD) (CD := CD) x)
    (mk (FD := FD) (CD := CD) y)
have rw : ∃ (W : J.Cover X) (h1 : W ⟶ Sx) (h2 : W ⟶ Sy), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
Tactic: rw [eq_mk_iff_exists]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.ConcreteSheafification (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst_2 : (X Y : D) → FunLike.{u_1 + 1, t + 1, t + 1} (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory.{t, w', w, u_1} D FD (CC := CD)
inst_3 : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D (FC := FD) (CC := CD))
inst_4 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_5 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_6 : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D (FC := FD) (CC := CD))
X : C
P : Functor.{v, w', u, w} Cᵒᵖ D
S Sx : J.Cover X
x : Meq (FD := FD) (CD := CD) P Sx
Sy : J.Cover X
y : Meq (FD := FD) (CD := CD) P Sy
h :
  ∀ (I : S.Arrow),
    Eq (α := CD ((J.plusObj P).obj (op I.Y))) (mk (FD := FD) (CD := CD) (x.pullback (FD := FD) (CD := CD) I.f))
      (mk (FD := FD) (CD := CD) (y.pullback (FD := FD) (CD := CD) I.f))
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh :
  ∀ (I : S.Arrow),
    (x.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h1 I) =
      (y.pullback (FD := FD) (CD := CD) I.f).refine (FD := FD) (CD := CD) (h2 I)
B : J.Cover X := S.bind W
⊢ ∃ (W : J.Cover X) (h1 : W ⟶ Sx) (h2 : W ⟶ Sy), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
have h₁ : ∃ (h1 : B ⟶ Sx) (h2 : B ⟶ Sy), x.refine (FD := FD) (CD := CD) h1 = y.refine (FD := FD) (CD := CD) h2
Tactic: use B