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
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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
h : α = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom
⊢ IsIso α

Tactic:
convert! (sheafIso (asIso (whiskerLeft G.op α.hom))).isIso_hom using 1

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.IsCoverDense.sheafIso, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Iso.isIso_hom, CategoryTheory.InducedCategory.Hom.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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
h : α.hom = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom.hom
⊢ α = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom

Tactic:
ext1
-- 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
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ α.hom = (sheafIso (asIso (G.op.whiskerLeft α.hom))).hom.hom

Tactic:
apply (sheafHom_eq _ _).symm

Premises used: CategoryTheory.Functor.IsCoverDense.sheafHom_eq, Eq.symm
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
compatible :
  ∀ (ℱ : Sheaf K (Type u_5)) {Z : C} {T : Presieve.{v_1, u_1} Z}
    {x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T},
    x.Compatible (R := T) →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                (x g₁ hg₁) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                (x g₂ hg₂) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
⊢ CompatiblePreserving K G

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
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
compatible :
  ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
    Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                  (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
              (x g₁ hg₁) :
            (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f.op) :
            (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                  (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
              (x g₂ hg₂) :
            (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
        (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj Y))))
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
        (x g₁ hg₁) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
        (x g₂ hg₂) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X)))

Tactic:
apply Functor.IsCoverDense.ext G

Premises used: CategoryTheory.Functor.IsCoverDense.ext
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
            (x g₁ hg₁) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
            (x g₂ hg₂) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W))))

Tactic:
IsLocallyFull.ext G _ (i ≫ f₁) fun V₁ iVW iV₁Y₁ e₁ ↦ ?_

Premises used: CategoryTheory.Functor.IsLocallyFull.ext, CategoryTheory.CategoryStruct.comp
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
⊢ Eq (α := (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₁.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₁)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                (x g₁ hg₁) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map iVW).op) :
          (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W)))) →
            (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj V₁))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map i.op) :
              (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X))) → (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj W))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map f₂.op) :
                  (a : (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op (G.obj Y₂)))) →
                    (fun (X : Type u_5) ↦ X) (ℱ.obj.obj (op X)))
                (x g₂ hg₂) :
              (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op X))) :
          (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj W)))) :
      (fun (X : Type u_5) ↦ X) (ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₁))))

Tactic:
IsLocallyFull.ext G _ (G.map iVW ≫ i ≫ f₂) fun V₂ iV₂V₁ iV₂Y₂ e₂ ↦ ?_

Premises used: CategoryTheory.Functor.IsLocallyFull.ext, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ G.map (iV₂V₁ ≫ iV₁Y₁ ≫ g₁) = G.map (iV₂Y₂ ≫ g₂)

Tactic:
simp [e₁, e₂, eq]
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
compatible : (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁) ≫ g₁ = (iV₃ ≫ iV₂Y₂) ≫ g₂
⊢ Eq (α := ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁)).op) :
          (a : ℱ.obj.obj (op (G.obj Y₁))) → ℱ.obj.obj (op (G.obj V₃)))
        (x g₁ hg₁) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ℱ.obj (P := Presheaf.IsSheaf K).map (G.map (iV₃ ≫ iV₂Y₂)).op) :
          (a : ℱ.obj.obj (op (G.obj Y₂))) → ℱ.obj.obj (op (G.obj V₃)))
        (x g₂ hg₂) :
      ℱ.obj (P := Presheaf.IsSheaf K).obj (op (G.obj V₃)))

Tactic:
apply hx
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve.{v_1, u_1} Z
x : FamilyOfElements (G.op ⋙ ℱ.obj (P := Presheaf.IsSheaf K)) T
hx : x.Compatible (R := T)
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
⊢ (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁) ≫ g₁ = (iV₃ ≫ iV₂Y₂) ≫ g₂

Tactic:
simpa using e₄
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
inst_4 : G.IsLocallyFaithful K
Hp : CoverPreserving J K G
⊢ G.IsContinuous J K

Tactic:
isContinuous_of_coverPreserving (compatiblePreserving K G) Hp

Premises used: CategoryTheory.Functor.isContinuous_of_coverPreserving, CategoryTheory.Functor.IsCoverDense.compatiblePreserving
-- 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
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e :
  Eq (α := obj (G.sheafPushforwardContinuous A J K) ℱ ⟶ obj (G.sheafPushforwardContinuous A J K) ℱ')
    (map (G.sheafPushforwardContinuous A J K) α) (map (G.sheafPushforwardContinuous A J K) β)
h : α.hom = β.hom
⊢ α = β

Tactic:
ext1
-- 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
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e :
  Eq (α := obj (G.sheafPushforwardContinuous A J K) ℱ ⟶ obj (G.sheafPushforwardContinuous A J K) ℱ')
    (map (G.sheafPushforwardContinuous A J K) α) (map (G.sheafPushforwardContinuous A J K) β)
⊢ Eq (α :=
    (obj (G.sheafPushforwardContinuous A J K) ℱ).obj (P := Presheaf.IsSheaf J) ⟶
      (obj (G.sheafPushforwardContinuous A J K) ℱ').obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (map (G.sheafPushforwardContinuous A J K) α))
    (InducedCategory.Hom.hom (map (G.sheafPushforwardContinuous A J K) β))

Tactic:
apply_fun fun e => e.hom at e
-- 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
inst_6 : G.IsContinuous J K
ℱ ℱ' : Sheaf.{v_2, v_4, u_2, u_4} K A
α β : ℱ ⟶ ℱ'
e : G.op.whiskerLeft α.hom = G.op.whiskerLeft β.hom
h : sheafHom (G.op.whiskerLeft α.hom) = β.hom
h₁ : sheafHom (G.op.whiskerLeft α.hom) = sheafHom (G.op.whiskerLeft β.hom)
h₂ h₃ : sheafHom (G.op.whiskerLeft β.hom) = sheafHom (G.op.whiskerLeft β.hom)
⊢ α.hom = β.hom

Tactic:
rw [← sheafHom_eq G α.hom, ← sheafHom_eq G β.hom, e]

Premises used: CategoryTheory.Functor.IsCoverDense.sheafHom_eq, CategoryTheory.InducedCategory.Hom.hom
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : G.IsCoverDense K
inst_3 : G.IsLocallyFull K
A : Type u_4
inst_4 : Category.{v_4, u_4} A
P Q : Functor.{v_2, v_4, u_2, u_4} Dᵒᵖ A
hQ : Presheaf.IsSheaf K Q
⊢ Function.Bijective (α := P ⟶ Q) (β :=
    obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) P ⟶ obj (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op) Q)
    (map (obj (whiskeringLeft Cᵒᵖ Dᵒᵖ A) G.op))

Tactic:
(IsCoverDense.restrictHomEquivHom (ℱ' := ⟨Q, hQ⟩)).symm.bijective

Premises used: Equiv.bijective, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, Equiv.symm
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
S : Sieve.{v_1, u_1} X
inst_2 : IsDenseSubsite J K G
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
      (Sieve.functorPushforward G S) ↔
    S ∈ (J : (a : C) → Set (Sieve a)) X

Tactic:
IsDenseSubsite.functorPushforward_mem_iff

Premises used: CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsDenseSubsite J K G
⊢ G.IsCoverDense K

Tactic:
isCoverDense' J

Premises used: CategoryTheory.Functor.IsDenseSubsite.isCoverDense'
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsDenseSubsite J K G
⊢ G.IsLocallyFull K

Tactic:
isLocallyFull' J

Premises used: CategoryTheory.Functor.IsDenseSubsite.isLocallyFull'
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsDenseSubsite J K G
⊢ G.IsLocallyFaithful K

Tactic:
isLocallyFaithful' J

Premises used: CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful'
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsDenseSubsite J K G
⊢ CoverPreserving J K G

Tactic:
⟨functorPushforward_mem_iff.mpr⟩

Premises used: Iff.mpr, CategoryTheory.CoverPreserving.mk, CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_3 : Category.{v_4, u_4} A
inst_4 : IsDenseSubsite J K G
⊢ G.IsContinuous J K

Tactic:
letI := IsDenseSubsite.isCoverDense J K G
  letI := IsDenseSubsite.isLocallyFull J K G
  letI := IsDenseSubsite.isLocallyFaithful J K G
  IsCoverDense.isContinuous J K G (IsDenseSubsite.coverPreserving J K G)

Premises used: CategoryTheory.Functor.IsDenseSubsite.coverPreserving, CategoryTheory.Functor.IsCoverDense.isContinuous
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_3 : Category.{v_4, u_4} A
inst_4 : IsDenseSubsite J K G
⊢ Full (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)

Tactic:
letI := IsDenseSubsite.isCoverDense J K G
  letI := IsDenseSubsite.isLocallyFull J K G
  inferInstance

Premises used: inferInstance
-- 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
G : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_4
inst_3 : Category.{v_4, u_4} A
inst_4 : IsDenseSubsite J K G
⊢ Faithful (C := Sheaf.{v_2, v_4, u_2, u_4} K A) (G.sheafPushforwardContinuous A J K)

Tactic:
letI := IsDenseSubsite.isCoverDense J K G
  letI := IsDenseSubsite.isLocallyFull J K G
  inferInstance

Premises used: inferInstance
-- 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
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : IsDenseSubsite J K G
U V : C
f : G.obj U ⟶ G.obj V
⊢ G.imageSieve f ∈ (J : (a : C) → Set (Sieve a)) U

Tactic:
letI := IsDenseSubsite.isLocallyFull J K G
  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_imageSieve_mem K f)

Premises used: CategoryTheory.Functor.functorPushforward_imageSieve_mem, CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff, Iff.mp