awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
X : Type u
⊢ Eq (α := yoneda'.obj X ⟶ yoneda'.obj X)
    (CategoryStruct.comp (Y :=
        yoneda'.obj
          (Functor.obj
            (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
            (yoneda'.obj X)))
        (yoneda'.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (_α : Type u) ↦
                  { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                    inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
          (yoneda'.obj X)) :
      yoneda'.obj X ⟶ yoneda'.obj X)
    (𝟙 (yoneda'.obj X) : yoneda'.obj X ⟶ yoneda'.obj X)
have h : InducedCategory.Hom.hom
    (CategoryStruct.comp (Y :=
      yoneda'.obj
        (Functor.obj
          (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
            Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
          (yoneda'.obj X)))
      (yoneda'.map
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (_α : Type u) ↦
                { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                  inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                  hom_inv_id := sorry, inv_hom_id := sorry })
              sorry))
          X))
      (NatTrans.app
        (Iso.hom
          (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) sorry)))
        (yoneda'.obj X))) =
  InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
X : Type u
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        yoneda'.obj
          (Functor.obj
            (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
            (yoneda'.obj X)))
        (yoneda'.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (_α : Type u) ↦
                  { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                    inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
          (yoneda'.obj X))) =
    InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))
have h : Eq (α := (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
  ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          yoneda'.obj
            (Functor.obj
              (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
              (yoneda'.obj X)))
          (yoneda'.map
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (_α : Type u) ↦
                    { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                      inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                      hom_inv_id := sorry, inv_hom_id := sorry })
                  sorry))
              X))
          (NatTrans.app
            (Iso.hom
              (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) sorry)))
            (yoneda'.obj X)))) :
    (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
  ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
      (InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))) :
    (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
Tactic: apply yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
X : Type u
⊢ Eq (α := (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            yoneda'.obj
              (Functor.obj
                (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                  Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
                (yoneda'.obj X)))
            (yoneda'.map
              (NatTrans.app
                (Iso.hom
                  (NatIso.ofComponents
                    (fun (_α : Type u) ↦
                      { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                        inv :=
                          ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                        hom_inv_id := ⋯, inv_hom_id := ⋯ })
                    ⋯))
                X))
            (NatTrans.app
              (Iso.hom
                (Iso.symm
                  (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
              (yoneda'.obj X)))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
have h : Eq (α := X ⟶ X)
  (typesGlue (Functor.obj yoneda X) sorry X
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ ↾fun (x : X) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x)) :
        (a : X) → PUnit.{u + 1} ⟶ X) :
    Functor.obj (Functor.obj yoneda X) (op X))
  (𝟙 X : X ⟶ X)
Tactic: dsimp [yoneda', yonedaEquiv, equivYoneda, evalEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)
have refine : Membership.mem (γ := Set (GrothendieckTopology (Type u))) (Sheaf.finestTopologySingle '' Set.range (Functor.obj yoneda))
  typesGrothendieckTopology
Tactic: refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
⊢ Membership.mem (γ := Set (GrothendieckTopology (Type u)))
    (Sheaf.finestTopologySingle '' Set.range (Functor.obj yoneda)) typesGrothendieckTopology
have refine : (⇑(Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool))) : (a : Type u) → Set (Sieve a)) =
  (⇑typesGrothendieckTopology : (a : Type u) → Set (Sieve a))
Tactic: refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
⊢ (⇑(Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool))) : (a : Type u) → Set (Sieve a)) =
    (⇑typesGrothendieckTopology : (a : Type u) → Set (Sieve a))
have h : ∀ (α : Type u),
  (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α =
    (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
Tactic: funext α
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
α : Type u
⊢ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α =
    (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
have h : ∀ (S : Sieve α),
  S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α ↔
    S ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
Tactic: ext S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
α : Type u
S : Sieve α
⊢ S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α ↔
    S ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
have h : ∀ (hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α)
  (x : α), S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
Tactic: refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs (f y)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
⊢ S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
have h : ∀ (hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)), False
Tactic: by_contra hsx
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda (ULift.{u, 0} Bool)) f.op) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op PUnit.{u + 1}))) →
            (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op β)))
        (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := true }) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda (ULift.{u, 0} Bool)) f.op) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op PUnit.{u + 1}))) →
            (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op β)))
        (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := false }) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))
have dsimp : Eq (α := β ⟶ ULift.{u, 0} Bool) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true })
  (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false })
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (goal)
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
⊢ Eq (α := β ⟶ ULift.{u, 0} Bool) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true })
    (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false })
have h : ∀ (y : β),
  Eq (α := Bool)
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true : ULift.{u, 0} Bool }))
        y))
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false : ULift.{u, 0} Bool }))
        y))
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Types (hypothesis)
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
⊢ False
have this : Eq.{u + 1} (α := unop (op PUnit.{u + 1}) ⟶ ULift.{u, 0} Bool) (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := true })
  (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := false })
Tactic: have : (↾fun _ => ULift.up true) = ↾fun _ => ULift.up false :=
    (hs PUnit (↾fun _ => x)).isSeparatedFor.ext
      fun β f hf => by
        dsimp
        ext y
        exact hsx.elim <| S.2 hf (↾fun _ => y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf.{v₁, v₂, u₁, u₂} J A
f : G₁ ⟶ G₂
h : IsIso ((sheafCompose J F).map f)
⊢ IsIso f
have rw : IsIso (X := obj (obj (whiskeringRight Cᵒᵖ A B) F) (obj (sheafToPresheaf J A) G₁))
  (map (obj (whiskeringRight Cᵒᵖ A B) F) (map (sheafToPresheaf J A) f))
Tactic: rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _),
      ← isIso_iff_of_reflects_iso _ ((whiskeringRight Cᵒᵖ A B).obj F)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
inst_6 : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf.{v₁, v₂, u₁, u₂} J A
f : G₁ ⟶ G₂
h : IsIso ((sheafCompose J F).map f)
⊢ IsIso (X := obj (obj (whiskeringRight Cᵒᵖ A B) F) (obj (sheafToPresheaf J A) G₁))
    (map (obj (whiskeringRight Cᵒᵖ A B) F) (map (sheafToPresheaf J A) f))
have change : IsIso (X := obj (sheafToPresheaf J B) ((sheafCompose J F).obj G₁))
  (map (sheafToPresheaf J B) ((sheafCompose J F).map f))
Tactic: change IsIso ((sheafToPresheaf _ _).map ((sheafCompose J F).map f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)
have rw : ∀ (hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) (X : C) (S : J.Cover X),
  Nonempty (IsLimit (S.multifork (P ⋙ F)))
Tactic: rw [Presheaf.isSheaf_iff_multifork] at hP ⊢
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))
have obtain : ∀ (h : IsLimit (S.multifork P)), Nonempty (IsLimit (S.multifork (P ⋙ F)))
Tactic: obtain ⟨h⟩ := hP X S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit (S.multifork P)
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))
have replace : ∀ (h : IsLimit (F.mapCone (S.multifork P))), Nonempty (IsLimit (S.multifork (P ⋙ F)))
Tactic: replace h := isLimitOfPreserves F h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Whiskering (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
B : Type u₃
inst_2 : Category.{v₃, u₃} B
J : GrothendieckTopology.{v₁, u₁} C
U : C
R : Presieve.{v₁, u₁} U
F_1 G H : Functor.{v₂, v₃, u₂, u₃} A B
η : F_1 ⟶ G
γ : G ⟶ H
inst_3 : J.HasSheafCompose F_1
inst_4 : J.HasSheafCompose G
inst_5 : J.HasSheafCompose H
F : Functor.{v₂, v₃, u₂, u₃} A B
inst_6 : ∀ (X : C) (S : J.Cover X) (P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A), PreservesLimit (S.index P).multicospan F
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
h : IsLimit (F.mapCone (S.multifork P))
⊢ Nonempty (IsLimit (S.multifork (P ⋙ F)))
have replace : ∀ (h : IsLimit ((Cone.postcompose (GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (S.multifork (P ⋙ F)))),
  Nonempty (IsLimit (S.multifork (P ⋙ F)))
Tactic: replace h := Limits.IsLimit.ofIsoLimit h (S.mapMultifork F P)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Skeletal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Skeleton.{v₁, u₁} C
h : X ≅ Y
⊢ X = Y
have this : Quotient.out X ≈ Quotient.out Y
Tactic: have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Skeletal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
⊢ ∀ (a : ThinSkeleton.{v₁, u₁} C), Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) ⋯ a a
have refine : ∀ (a : C), Quotient.lift₂ (fun (X Y : C) ↦ Nonempty.{v₁ + 1} (X ⟶ Y)) sorry ⟦a⟧ ⟦a⟧
Tactic: refine Quotient.ind fun a => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
⊢ Eq (α := ∐ functorObjSrcFamily f πX ⟶ S) (functorObjTop f πX ≫ πX : ∐ functorObjSrcFamily f πX ⟶ S)
    (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
        (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
        (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S) :
      ∐ functorObjSrcFamily f πX ⟶ S)
have h : ∀ (b : FunctorObjIndex f πX),
  CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
      (functorObjTop f πX ≫ πX : ∐ functorObjSrcFamily f πX ⟶ S) =
    CategoryStruct.comp (Y := ∐ functorObjSrcFamily f πX)
      (Sigma.ι (functorObjSrcFamily f πX) b : functorObjSrcFamily f πX b ⟶ ∐ functorObjSrcFamily f πX)
      (CategoryStruct.comp (Y := ∐ functorObjTgtFamily f πX)
          (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
          (π'FunctorObj f πX : ∐ functorObjTgtFamily f πX ⟶ S) :
        ∐ functorObjSrcFamily f πX ⟶ S)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Construction (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst_1 : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst_2 :
  HasPushout (X := ∐ functorObjSrcFamily f πX) (Z := ∐ functorObjTgtFamily f πX)
    (functorObjTop f πX : ∐ functorObjSrcFamily f πX ⟶ X)
    (functorObjLeft f πX : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX)
inst_3 : LocallySmall.{t, v, u} C
inst_4 : Small.{t, w} I
φ : (x : FunctorObjIndex f πX) →
  (i : Shrink.{t, w} I) ×
    Shrink.{t, v}
      ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
        (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)) :=
  fun (x : FunctorObjIndex f πX) ↦
    Sigma.mk (β := fun (i : Shrink.{t, w} I) ↦
      Shrink.{t, v}
        ((A ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ X) ×
          (B ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I) i) ⟶ S)))
      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)
      ((equivShrink
            ((A
                  ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I)
                    ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i : Shrink.{t, w} I)) ⟶
                X) ×
              (B
                  ((Equiv.symm (equivShrink I) : (a : Shrink.{t, w} I) → I)
                    ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i : Shrink.{t, w} I)) ⟶
                S)) :
          (a :
              (A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)) →
            Shrink.{t, v}
              ((A
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  X) ×
                (B
                    (((equivShrink I).symm : (a : Shrink.{t, w} I) → I)
                      ((equivShrink I : (a : I) → Shrink.{t, w} I) x.i)) ⟶
                  S)))
        (eqToHom ⋯ ≫ x.t, eqToHom ⋯ ≫ x.b))
i₁ : I
t₁ : A i₁ ⟶ X
b₁ : B i₁ ⟶ S
w : t₁ ≫ πX = f i₁ ≫ b₁
i₂ : I
t₂ : A i₂ ⟶ X
b₂ : B i₂ ⟶ S
w_1 : t₂ ≫ πX = f i₂ ≫ b₂
h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₂, t := t₂, b := b₂, w := w_1 }
⊢ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = { i := i₂, t := t₂, b := b₂, w := w_1 }
have obtain : ∀ (t₂ : A i₁ ⟶ X) (b₂ : B i₁ ⟶ S) (w_2 : t₂ ≫ πX = f i₁ ≫ b₂)
  (h : φ { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = φ { i := i₁, t := t₂, b := b₂, w := w_2 }),
  { i := i₁, t := t₁, b := b₁, w := w : FunctorObjIndex f πX } = { i := i₁, t := t₂, b := b₂, w := w_2 }
Tactic: obtain rfl : i₁ = i₂ := by simpa [φ] using congr_arg Sigma.fst h
Cleared hypotheses: i₂, t₂, b₂, w_1, h