awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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)
α' : ℱ ⋙ yoneda ⟶ ℱ'.obj (P := Presheaf.IsSheaf K) ⋙ yoneda := sheafYonedaHom α
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda (ℱ.obj X))
      (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj Y)))
    (map yoneda (ℱ.map f ≫ preimage yoneda (α'.app Y)))
    (map yoneda (preimage yoneda (α'.app X) ≫ ℱ'.obj (P := Presheaf.IsSheaf K).map f))

Tactic:
simpa using α'.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
rw : IsIso (X := obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (map yoneda ((sheafHom i.hom).app X))
⊢ IsIso ((sheafHom i.hom).app X)

Tactic:
rw [← isIso_iff_of_reflects_iso _ yoneda]

Premises used: CategoryTheory.yoneda, CategoryTheory.isIso_iff_of_reflects_iso
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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))) ∧
    (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
      𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))
⊢ IsIso (X := obj yoneda (ℱ.obj (P := Presheaf.IsSheaf K).obj X)) (map yoneda ((sheafHom i.hom).app X))

Tactic:
use (sheafYonedaHom i.inv).app X

Premises used: CategoryTheory.Functor.IsCoverDense.sheafYonedaHom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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)))
h₁ :
  (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).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))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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 :
  ∀ (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)
⊢ 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:
ext x : 2
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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 :
  ∀ (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
⊢ (sheafYonedaHom i.inv).app X ≫ map yoneda ((sheafHom i.hom).app X) =
    𝟙 (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj X))

Tactic:
ext x : 2
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
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)
⊢ 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:
simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]

Premises used: CategoryTheory.Functor.IsCoverDense.sheafHom, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
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)
⊢ 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:
simp only [sheafHom, NatTrans.comp_app, NatTrans.id_app, Functor.map_preimage]

Premises used: CategoryTheory.Functor.IsCoverDense.sheafHom, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
⊢ ((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:
((Types.presheafIso (isoOver i (unop x))).app X).hom_inv_id

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.IsCoverDense.Types.presheafIso, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.IsCoverDense.isoOver, CategoryTheory.Iso.app, Opposite.unop, CategoryTheory.Functor.IsCoverDense.homOver
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
⊢ ((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:
exact ((Types.presheafIso (isoOver i (unop x))).app X).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.IsCoverDense.Types.presheafIso, CategoryTheory.Functor.IsCoverDense.isoOver, CategoryTheory.Iso.app, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
⊢ ((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:
((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.comp, CategoryTheory.Functor.IsCoverDense.Types.presheafIso, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.IsCoverDense.isoOver, CategoryTheory.Iso.app, Opposite.unop, CategoryTheory.Functor.IsCoverDense.homOver
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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ᵒᵖ
⊢ ((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:
exact ((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.IsCoverDense.Types.presheafIso, CategoryTheory.Functor.IsCoverDense.isoOver, CategoryTheory.Iso.app, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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)

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
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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)
⊢ IsIso (sheafHom i.hom)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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)
⊢ IsIso (sheafHom i.hom)

Tactic:
haveI : IsIso (sheafHom i.hom) := by apply NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
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_1 : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
this : IsIso (sheafHom i.hom)
⊢ ℱ.obj (P := Presheaf.IsSheaf K) ≅ ℱ'.obj (P := Presheaf.IsSheaf K)

Tactic:
apply asIso (sheafHom i.hom)

Premises used: CategoryTheory.Functor.IsCoverDense.sheafHom, CategoryTheory.Iso.hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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)
w : ∀ (X : Cᵒᵖ), (G.op.whiskerLeft (sheafHom α)).app X = α.app X
⊢ G.op.whiskerLeft (sheafHom α) = α

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
w :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda ((G.op ⋙ ℱ).obj X))
      (obj yoneda ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj X)))
    (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) (map yoneda (α.app X))
⊢ (G.op.whiskerLeft (sheafHom α)).app X = α.app X

Tactic:
apply yoneda.map_injective

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
w :
  ∀ (U : Aᵒᵖ) (x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) U))
        x =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_4, v_4, u_4, v_4 + 1} Aᵒᵖ (Type v_4)) (obj yoneda ((G.op ⋙ ℱ).obj X))
      (obj yoneda ((G.op ⋙ ℱ'.obj (P := Presheaf.IsSheaf K)).obj X)))
    (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) (map yoneda (α.app X))

Tactic:
ext U
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
w :
  Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (map yoneda (preimage yoneda ((sheafYonedaHom α).app (op (G.obj (unop X)))))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda ((G.op.whiskerLeft (sheafHom α)).app X)) U))
      x =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U)) x

Tactic:
dsimp [sheafHom, -yoneda_obj_obj, -yoneda_map_app]

Premises used: CategoryTheory.yoneda_map_app, CategoryTheory.Functor.IsCoverDense.sheafHom, CategoryTheory.yoneda_obj_obj
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
K : GrothendieckTopology.{v_2, u_2} D
A : Type u_4
inst_2 : Category.{v_4, u_4} A
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : G.IsCoverDense K
inst_4 : 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 : Cᵒᵖ
U : Aᵒᵖ
x : obj (obj yoneda ((G.op ⋙ ℱ).obj X)) U
w :
  Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((sheafYonedaHom α).app (op (G.obj (unop X)))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
⊢ Eq (α := obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (map yoneda (preimage yoneda ((sheafYonedaHom α).app (op (G.obj (unop X)))))) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map yoneda (α.app X)) U) :
          (a : (yoneda.obj (ℱ.obj (op (G.obj (unop X))))).obj U) →
            (yoneda.obj (ℱ'.obj.obj (op (G.obj (unop X))))).obj U)
        x :
      obj (obj yoneda (ℱ'.obj (P := Presheaf.IsSheaf K).obj (op (G.obj (unop X))))) U)

Tactic:
rw [yoneda.map_preimage]

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_preimage