awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ (f.unop ≫
        (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op =
    (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
have w : Eq (α := unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
  (f.unop ≫
    (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op)
  (f.unop ≫
    x ≫
      ℱ.map (Nonempty.some hf').map.op ≫
        α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op)
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ Eq (α := unop Y ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (f.unop ≫
      (ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op)
    (f.unop ≫
      x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op)
have w : Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
  (x ≫
      ℱ.map (Nonempty.some hf').map.op ≫
        α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
have rw : ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
        (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
      x ≫
    ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
  unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
Tactic: rw [← hf'.some.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map f'.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
have w : Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
  (x ≫
      ℱ.map (Nonempty.some hf').map.op ≫
        α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
Tactic: conv_lhs => rw [← hf'.some.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map ((Nonempty.some hf').lift ≫ (Nonempty.some hf').map).op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
    (x ≫
        ℱ.map (Nonempty.some hf').map.op ≫
          α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op :
      unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op Y'))
have w : ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op) ≫
    ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op =
  ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
    ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
Tactic: simp only [← Category.assoc, op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ obj (whiskeringLeft Dᵒᵖ A (Type v_4)) ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : Sieve.arrows (Sieve.coverByImage G (unop U)) f'
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
            (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
          x ≫
        ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op =
    ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').lift.op
have w : Eq (α := unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (appHom (homOver α (unop X)) (unop U)) :
          (a : unop X ⟶ ℱ.obj U) → unop X ⟶ ℱ'.obj.obj U)
        x ≫
      ℱ'.obj (P := Presheaf.IsSheaf K).map (Nonempty.some hf').map.op :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').obj)))
  ((x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1) :
    unop X ⟶ ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (Nonempty.some hf').1)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
U V : Dᵒᵖ
i : U ⟶ V
⊢ ((ℱ ⋙ yoneda).map i ≫
      let α_1 := sheafCoyonedaHom α;
      { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := ⋯ }) =
    (let α_1 := sheafCoyonedaHom α;
      { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := ⋯ :
        NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
      (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i
have w : ∀ (X : Aᵒᵖ) (x : ((ℱ ⋙ yoneda).obj U).obj X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((ℱ ⋙ yoneda).map i ≫
            let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app V, naturality := sorry :
              NatTrans ((ℱ ⋙ yoneda).obj V) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj V) })
          X))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((let α_1 := sheafCoyonedaHom α;
            { app := fun (X : Aᵒᵖ) ↦ (α_1.app X).app U, naturality := sorry :
              NatTrans ((ℱ ⋙ yoneda).obj U) ((ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).obj U) }) ≫
            (ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda).map i)
          X))
      x
Tactic: ext X x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ IsIso ((sheafHom i.hom).app X)
have rw : IsIso (X := obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (map yoneda ((sheafHom i.hom).app X))
Tactic: rw [← isIso_iff_of_reflects_iso _ yoneda]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ IsIso (X := obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (map yoneda ((sheafHom i.hom).app X))
have h : Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4))
      (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
    (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
    (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))) ∧
  (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
    𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
Tactic: use (sheafYonedaHom i.inv).app X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ Eq (α :=
      Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4))
        (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
      (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
      (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))) ∧
    (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
      𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
have h : Eq (α :=
  Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))
    (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
  (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
  (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4))
      (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
    (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
    (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
⊢ Eq (α :=
      Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4))
        (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
      (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
      (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))) ∧
    (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
      𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
have h₁ : (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
  𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4))
      (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
    (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X)
    (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)))
have h : ∀ (x : Aᵒᵖ),
  Eq (α :=
    obj (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) x ⟶
      obj (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) x)
    (NatTrans.app (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X) x)
    (NatTrans.app (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))) x)
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
⊢ (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
    𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
have h : ∀ (x : Aᵒᵖ),
  NatTrans.app ((sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X)) x =
    NatTrans.app (𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))) x
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
x : Aᵒᵖ
⊢ Eq (α :=
    obj (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) x ⟶
      obj (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) x)
    (NatTrans.app (map yoneda ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X) x)
    (NatTrans.app (𝟙 (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X))) x)
have h : ((sheafYonedaHom i.hom).app X).app x ≫ ((sheafYonedaHom i.inv).app X).app x =
  𝟙 (obj (obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) x)
Tactic: simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
X : Dᵒᵖ
x : Aᵒᵖ
⊢ NatTrans.app ((sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X)) x =
    NatTrans.app (𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))) x
have h : ((sheafYonedaHom i.inv).app X).app x ≫ ((sheafYonedaHom i.hom).app X).app x =
  𝟙 (obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X)) x)
Tactic: simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
⊢ ℱ.obj (P := Presheaf.IsSheaf K) ≅ ℱ'.obj (P := Presheaf.IsSheaf K)
have this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
Tactic: have : ∀ X : Dᵒᵖ, IsIso ((sheafHom i.hom).app X) := by
    intro X
    rw [← isIso_iff_of_reflects_iso _ yoneda]
    use (sheafYonedaHom i.inv).app X
    constructor <;> ext x : 2 <;>
      simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]
    · exact ((Types.presheafIso (isoOver i (unop x))).app X).hom_inv_id
    · exact ((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
E : Type u_3
inst_2 : Category.{v_3, u_3} E
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
L : GrothendieckTopology.{v_3, u_3} E
A : Type u_4
inst_3 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.IsCoverDense K
inst_5 : G.IsLocallyFull K
ℱ_1 : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
ℱ'_1 ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
i : G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K) ≅ G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)
this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
⊢ ℱ.obj (P := Presheaf.IsSheaf K) ≅ ℱ'.obj (P := Presheaf.IsSheaf K)
have this₁ : IsIso (sheafHom i.hom)
Tactic: haveI : IsIso (sheafHom i.hom) := by apply NatIso.isIso_of_isIso_app