awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
X₁ X₂ Y₁ Y₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf : J.W f
hg : J.W g
simp :
  ∀
    (hf :
      ∀ (Φ : P.FullSubcategory),
        IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber X₁) (Functor.map Φ.obj (P := P).presheafFiber f))
    (hg :
      ∀ (Φ : P.FullSubcategory),
        IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber Y₁) (Functor.map Φ.obj (P := P).presheafFiber g))
    (Φ : P.FullSubcategory),
    IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₁ Y₁))
      (Functor.map Φ.obj (P := P).presheafFiber (f ⊗ₘ g))
⊢ J.W (X := tensorObj (𝒞 := Functor.category) X₁ Y₁) (f ⊗ₘ g)

Tactic:
simp only [hP.W_iff (A := A)] at hf hg ⊢

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
X₁ X₂ Y₁ Y₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf :
  ∀ (Φ : P.FullSubcategory),
    IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber X₁) (Functor.map Φ.obj (P := P).presheafFiber f)
hg :
  ∀ (Φ : P.FullSubcategory),
    IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber Y₁) (Functor.map Φ.obj (P := P).presheafFiber g)
Φ : P.FullSubcategory
rw :
  IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₁ Y₁)) (Y :=
    Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₂ Y₂))
    (CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst_2) (Functor.obj Φ.obj (P := P).presheafFiber X₁)
        (Functor.obj Φ.obj (P := P).presheafFiber Y₁))
      (Functor.OplaxMonoidal.δ Φ.obj (P := P).presheafFiber X₁ Y₁)
      ((Functor.map Φ.obj (P := P).presheafFiber f ⊗ₘ Functor.map Φ.obj (P := P).presheafFiber g) ≫
        Functor.LaxMonoidal.μ Φ.obj (P := P).presheafFiber X₂ Y₂))
⊢ IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₁ Y₁))
    (Functor.map Φ.obj (P := P).presheafFiber (f ⊗ₘ g))

Tactic:
rw [Functor.Monoidal.map_tensor]

Premises used: CategoryTheory.Functor.Monoidal.map_tensor
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
X₁ X₂ Y₁ Y₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
hf :
  ∀ (Φ : P.FullSubcategory),
    IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber X₁) (Functor.map Φ.obj (P := P).presheafFiber f)
hg :
  ∀ (Φ : P.FullSubcategory),
    IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber Y₁) (Functor.map Φ.obj (P := P).presheafFiber g)
Φ : P.FullSubcategory
⊢ IsIso (X := Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₁ Y₁)) (Y :=
    Functor.obj Φ.obj (P := P).presheafFiber (tensorObj (𝒞 := Functor.category) X₂ Y₂))
    (CategoryStruct.comp (Y :=
      tensorObj.{v', u'} (𝒞 := inst_2) (Functor.obj Φ.obj (P := P).presheafFiber X₁)
        (Functor.obj Φ.obj (P := P).presheafFiber Y₁))
      (Functor.OplaxMonoidal.δ Φ.obj (P := P).presheafFiber X₁ Y₁)
      ((Functor.map Φ.obj (P := P).presheafFiber f ⊗ₘ Functor.map Φ.obj (P := P).presheafFiber g) ≫
        Functor.LaxMonoidal.μ Φ.obj (P := P).presheafFiber X₂ Y₂))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (Point.{w, v, u} J)
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_14 : J.HasEnoughPoints
obtain :
  ∀ (P : ObjectProperty (Point.{w, v, u} J)),
    ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P →
      ∀ (hP : P.IsConservativeFamilyOfPoints), MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W
⊢ MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W

Tactic:
obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J

Premises used: CategoryTheory.GrothendieckTopology.HasEnoughPoints.exists_objectProperty
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P_1 : ObjectProperty (Point.{w, v, u} J)
hP_1 : P_1.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_14 : J.HasEnoughPoints
P : ObjectProperty (Point.{w, v, u} J)
left : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W

Tactic:
hP.isMonoidal_W A

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W
-- Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
J : GrothendieckTopology.{v, u} C
P_1 : ObjectProperty (Point.{w, v, u} J)
hP_1 : P_1.IsConservativeFamilyOfPoints
A : Type u'
inst_2 : Category.{v', u'} A
inst_3 : MonoidalCategory.{v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v', u'} A
inst_5 : HasProducts.{w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w
inst_6 : (X Y : A) → FunLike.{u_1 + 1, w + 1, w + 1} (FC X Y) (CC X) (CC Y)
inst_7 : ConcreteCategory.{w, v', u', u_1} A FC (CC := CC)
inst_8 : HasWeakSheafify.{v, v', u, u'} J A
inst_9 : Functor.ReflectsIsomorphisms.{v', u', w, w + 1} (forget A (FC := FC) (CC := CC))
inst_10 : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A (FC := FC) (CC := CC))
inst_11 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst_12 : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst_13 : HasSheafCompose.{v, v', w, u, u', w + 1} J (forget A (FC := FC) (CC := CC))
inst_14 : J.HasEnoughPoints
P : ObjectProperty (Point.{w, v, u} J)
left : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W

Tactic:
exact hP.isMonoidal_W A

Premises used: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
X : D
R : Sieve.{v', u'} X
hR : R ∈ (K : (a : D) → Set (Sieve a)) X
u : Φ.fiber.Elements
f : (CategoryOfElements.π Φ.fiber ⋙ F).obj u ⟶ X
obtain :
  ∀ (U : C) (u : Φ.fiber.obj U)
    (f : (CategoryOfElements.π Φ.fiber ⋙ F).obj (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) ⟶ X),
    ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q :
      v ⟶ Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) (a : F.obj (v.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y),
      a ≫ g = F.map (↑q : v.fst ⟶ ⟨U, u⟩.fst) ≫ f
⊢ ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q : v ⟶ u) (a :
    F.obj (v.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y), a ≫ g = F.map (↑q : v.fst ⟶ u.fst) ≫ f

Tactic:
obtain ⟨U, u⟩ := u
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
X : D
R : Sieve.{v', u'} X
hR : R ∈ (K : (a : D) → Set (Sieve a)) X
U : C
u : Φ.fiber.obj U
f : (CategoryOfElements.π Φ.fiber ⋙ F).obj (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) ⟶ X
dsimp :
  ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q :
    v ⟶ Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) (a : F.obj (v.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y),
    a ≫ g = F.map (↑q : v.fst ⟶ U) ≫ f
⊢ ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q :
    v ⟶ Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) (a : F.obj (v.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y),
    a ≫ g = F.map (↑q : v.fst ⟶ ⟨U, u⟩.fst) ≫ f

Tactic:
dsimp at f ⊢
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
X : D
R : Sieve.{v', u'} X
hR : R ∈ (K : (a : D) → Set (Sieve a)) X
U : C
u : Φ.fiber.obj U
f : F.obj U ⟶ X
obtain :
  ∀ (V : C) (g : V ⟶ U) (hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g) (v : Φ.fiber.obj V),
    ∃ (Y : D) (g_1 : Y ⟶ X) (_ : R.arrows g_1) (v_1 : Φ.fiber.Elements) (q :
      v_1 ⟶
        Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
            v))
      (a : F.obj (v_1.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y), a ≫ g_1 = F.map (↑q : v_1.fst ⟶ U) ≫ f
⊢ ∃ (Y : D) (g : Y ⟶ X) (_ : R.arrows g) (v : Φ.fiber.Elements) (q :
    v ⟶ Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U u) (a : F.obj (v.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y),
    a ≫ g = F.map (↑q : v.fst ⟶ U) ≫ f

Tactic:
obtain ⟨V, g, hg, v, rfl⟩ :=
    Φ.jointly_surjective _ (F.cover_lift J K (K.pullback_stable f hR)) u

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.GrothendieckTopology.Point.jointly_surjective, CategoryTheory.Functor.cover_lift, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
X : D
R : Sieve.{v', u'} X
hR : R ∈ (K : (a : D) → Set (Sieve a)) X
U : C
f : F.obj U ⟶ X
V : C
g : V ⟶ U
hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g
v : Φ.fiber.obj V
⊢ ∃ (Y : D) (g_1 : Y ⟶ X) (_ : R.arrows g_1) (v_1 : Φ.fiber.Elements) (q :
    v_1 ⟶
      Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) U
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj V)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj U))
          v))
    (a : F.obj (v_1.fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ⟶ Y), a ≫ g_1 = F.map (↑q : v_1.fst ⟶ U) ≫ f

Tactic:
exact ⟨_, F.map g ≫ f, hg, Φ.fiber.elementsMk _ v, ⟨g, rfl⟩, 𝟙 _, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
inst_3 : LocallySmall.{w, v', u'} D
A : Type u''
inst_4 : Category.{v'', u''} A
inst_5 : HasColimitsOfSize.{w, w, v'', u''} A
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
P : Functor.{v', v'', u', u''} Dᵒᵖ A
⊢ Eq (α := P.obj (op (F.obj Y)) ⟶ Functor.obj (Φ.map F K).presheafFiber P)
    (P.map (F.map f).op ≫ Φ.toPresheafFiberMap F K P X x)
    (Φ.toPresheafFiberMap F K P Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y))
        x))

Tactic:
toPresheafFiberOfIsCofiltered_w _ (Φ.map_aux F K)
    (V := ⟨X, x⟩) (U := ⟨Y, Φ.fiber.map f x⟩) ⟨f, rfl⟩ P

Premises used: Subtype.mk, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap, CategoryTheory.GrothendieckTopology.Point.map_aux, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_w, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
inst_3 : LocallySmall.{w, v', u'} D
A : Type u''
inst_4 : Category.{v'', u''} A
inst_5 : HasColimitsOfSize.{w, w, v'', u''} A
P Q : Functor.{v', v'', u', u''} Dᵒᵖ A
g : P ⟶ Q
X : C
x : Φ.fiber.obj X
⊢ Eq (α := P.obj (op (F.obj X)) ⟶ Functor.obj (Φ.map F K).presheafFiber Q)
    (Φ.toPresheafFiberMap F K P X x ≫ Functor.map (Φ.map F K).presheafFiber g)
    (g.app (op (F.obj X)) ≫ Φ.toPresheafFiberMap F K Q X x)

Tactic:
toPresheafFiberOfIsCofiltered_naturality _ _ _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered_naturality, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
inst_3 : LocallySmall.{w, v', u'} D
A : Type u''
inst_4 : Category.{v'', u''} A
inst_5 : HasColimitsOfSize.{w, w, v'', u''} A
P : Functor.{v', v'', u', u''} Dᵒᵖ A
T : A
f g : Functor.obj (Φ.map F K).presheafFiber P ⟶ T
h : ∀ (X : C) (x : Φ.fiber.obj X), Φ.toPresheafFiberMap F K P X x ≫ f = Φ.toPresheafFiberMap F K P X x ≫ g
⊢ f = g

Tactic:
(Φ.isColimitPresheafFiberMapCocone F K P).hom_ext (fun _ ↦ h _ _)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Sigma.fst, CategoryTheory.Limits.colimit, Sigma.snd, Opposite.unop, CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
inst_3 : LocallySmall.{w, v', u'} D
A : Type u''
inst_4 : Category.{v'', u''} A
inst_5 : HasColimitsOfSize.{w, w, v'', u''} A
P : Functor.{v', v'', u', u''} Dᵒᵖ A
X : C
x : Φ.fiber.obj X
⊢ Eq (α := P.obj (op (F.obj X)) ⟶ Functor.obj Φ.presheafFiber (F.op ⋙ P))
    (CategoryStruct.comp (Y := Functor.obj (Φ.map F K).presheafFiber P) (Φ.toPresheafFiberMap F K P X x)
      (Iso.hom (Φ.presheafFiberMapObjIso F K P)))
    (Φ.toPresheafFiber X x (F.op ⋙ P))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom
    (Φ.isColimitPresheafFiberMapCocone F K P) _ ⟨X, x⟩

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberOfIsCofiltered, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, Opposite.op, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap, Sigma.mk, CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Sites.Point.Map
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
F : Functor.{v, v', u, u'} C D
K : GrothendieckTopology.{v', u'} D
inst_2 : F.IsCocontinuous J K
inst_3 : LocallySmall.{w, v', u'} D
A : Type u''
inst_4 : Category.{v'', u''} A
inst_5 : HasColimitsOfSize.{w, w, v'', u''} A
P : Functor.{v', v'', u', u''} Dᵒᵖ A
X : C
x : Φ.fiber.obj X
⊢ Eq (α := (F.op ⋙ P).obj (op X) ⟶ Functor.obj (Φ.map F K).presheafFiber P)
    (Φ.toPresheafFiber X x (F.op ⋙ P) ≫ Iso.inv (Φ.presheafFiberMapObjIso F K P)) (Φ.toPresheafFiberMap F K P X x)

Tactic:
simpa [-toPresheafFiberMap_presheafFiberMapObjIso_hom] using
    (Φ.toPresheafFiberMap_presheafFiberMapObjIso_hom F K ..).symm =≫
      (Φ.presheafFiberMapObjIso F K P).inv

Premises used: CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso, CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom, Eq.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
    Eq (α :=
      (tensorObj (𝒞 := category) P₁ P₂).obj (Opposite.op Y) ⟶
        tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber P₁) (obj Φ.presheafFiber P₂))
      ((tensorObj (𝒞 := category) P₁ P₂).map f.op ≫
        (fun (X : C) (x : Φ.fiber.obj X) ↦
            (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ :
              tensorObj.{v', u'} (𝒞 := inst_1) (P₁.obj (Opposite.op X)) (P₂.obj (Opposite.op X)) ⟶
                tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber P₁) (obj Φ.presheafFiber P₂)))
          X x)
      ((fun (X : C) (x : Φ.fiber.obj X) ↦
          (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ :
            tensorObj.{v', u'} (𝒞 := inst_1) (P₁.obj (Opposite.op X)) (P₂.obj (Opposite.op X)) ⟶
              tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber P₁) (obj Φ.presheafFiber P₂)))
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y))
          x))

Tactic:
simp [tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom
-- Module: Mathlib.CategoryTheory.Sites.Point.Monoidal
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : MonoidalCategory.{v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
x : X ⟶ Y
x_1 : Functor.{v, v', u, u'} Cᵒᵖ A
h :
  ∀ (X_1 : C) (x_2 : Φ.fiber.obj X_1),
    Eq (α :=
      (tensorObj (𝒞 := category) X x_1).obj (Opposite.op X_1) ⟶
        tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber Y) (obj Φ.presheafFiber x_1))
      (CategoryStruct.comp (Y := obj Φ.presheafFiber (tensorObj (𝒞 := category) X x_1))
        (Φ.toPresheafFiber X_1 x_2 (tensorObj (𝒞 := category) X x_1))
        (Φ.presheafFiberDesc
            (fun (X_2 : C) (x : Φ.fiber.obj X_2) ↦ Φ.toPresheafFiber X_2 x X ⊗ₘ Φ.toPresheafFiber X_2 x x_1) ⋯ ≫
          map Φ.presheafFiber x ▷ obj Φ.presheafFiber x_1))
      (CategoryStruct.comp (Y := obj Φ.presheafFiber (tensorObj (𝒞 := category) X x_1))
        (Φ.toPresheafFiber X_1 x_2 (tensorObj (𝒞 := category) X x_1))
        (map Φ.presheafFiber (x ▷ x_1) ≫
          Φ.presheafFiberDesc (fun (X : C) (x : Φ.fiber.obj X) ↦ Φ.toPresheafFiber X x Y ⊗ₘ Φ.toPresheafFiber X x x_1)
            ⋯))
⊢ Eq (α :=
    obj Φ.presheafFiber (tensorObj (𝒞 := category) X x_1) ⟶
      tensorObj.{v', u'} (𝒞 := inst_1) (obj Φ.presheafFiber Y) (obj Φ.presheafFiber x_1))
    (Φ.presheafFiberDesc
        (fun (X_1 : C) (x : Φ.fiber.obj X_1) ↦ Φ.toPresheafFiber X_1 x X ⊗ₘ Φ.toPresheafFiber X_1 x x_1) ⋯ ≫
      map Φ.presheafFiber x ▷ obj Φ.presheafFiber x_1)
    (map Φ.presheafFiber (x ▷ x_1) ≫
      Φ.presheafFiberDesc (fun (X : C) (x : Φ.fiber.obj X) ↦ Φ.toPresheafFiber X x Y ⊗ₘ Φ.toPresheafFiber X x x_1) ⋯)

Tactic:
ext