awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ F₂ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : F₁ ⟶ F₂
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) → (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₂))
hF₂ : ∃ (U : C), F₂ = Functor.obj shrinkYoneda.{w, v, u} U
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
have obtain : ∀ (U : C) (f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U) [Mono f]
  (hf :
    ∀ (Φ : P.FullSubcategory),
      Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
        (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
            (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))),
  Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
Tactic: obtain ⟨U, rfl⟩ := hF₂
Cleared hypotheses: F₂, f, inst_2, hf, hF₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
this :
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
V : C
g : ToType (FC := TypeCat.Fun) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op V))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f g ∈ (J : (a : C) → Set (Sieve a)) V
have obtain : ∀ (g : unop (op V) ⟶ U),
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
    (J : (a : C) → Set (Sieve a)) V
Tactic: obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
this :
  Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
V : C
g : unop (op V) ⟶ U
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
    (J : (a : C) → Set (Sieve a)) V
have this₁ : Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
  (Sieve.pullback g
    (Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U))))
Tactic: replace this := J.pullback_stable g this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
V : C
g : unop (op V) ⟶ U
this :
  Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
    (Sieve.pullback g
      (Presheaf.imageSieve (FA := TypeCat.Fun) f
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
          (𝟙 U))))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op V) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op V)) g) ∈
    (J : (a : C) → Set (Sieve a)) V
have this₁ : Membership.mem (γ := Set (Sieve.{v, u} (unop (op V)))) ((J : (a : C) → Set (Sieve a)) (unop (op V)))
  (Presheaf.imageSieve (FA := TypeCat.Fun) f
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} U) g.op) :
        (a : (shrinkYoneda.{w, v, u}.obj U).obj (op U)) → (shrinkYoneda.{w, v, u}.obj U).obj (op (unop (op V))))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U) :
        Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} U) (op U))))
Tactic: rw [Presheaf.pullback_imageSieve] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
⊢ Presheaf.IsLocallySurjective J (FA := TypeCat.Fun) f
have suffices : Presheaf.imageSieve (FA := TypeCat.Fun) f
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
  (J : (a : C) → Set (Sieve a)) U
Tactic: suffices Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U from ⟨by
    intro V g
    obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
    replace this := J.pullback_stable g this
    rw [Presheaf.pullback_imageSieve] at this
    have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)
    simp only [Quiver.Hom.unop_op, Category.comp_id] at hg
    simpa [← hg]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
F₁ : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
U : C
f : F₁ ⟶ Functor.obj shrinkYoneda.{w, v, u} U
inst_2 : Mono f
hf :
  ∀ (Φ : P.FullSubcategory),
    Function.Surjective (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber F₁)) (β :=
      (fun (X : Type w) ↦ X) (Functor.obj Φ.obj (P := P).presheafFiber (Functor.obj shrinkYoneda.{w, v, u} U)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.obj (P := P).presheafFiber f)) :
        (a : (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj F₁)) →
          (fun (X : Type w) ↦ X) (Φ.obj.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj U)))
⊢ Presheaf.imageSieve (FA := TypeCat.Fun) f
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U)) (𝟙 U)) ∈
    (J : (a : C) → Set (Sieve a)) U
have refine : ∀ (Φ : P.FullSubcategory) (u : Φ.obj (P := P).fiber.obj U),
  ∃ (Y : C) (g : Y ⟶ U) (_ :
    Sieve.arrows
      (Presheaf.imageSieve (FA := TypeCat.Fun) f
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op U) ⟶ U) → (shrinkYoneda.{w, v, u}.obj U).obj (op U))
          (𝟙 U)))
      g)
    (y : Φ.obj (P := P).fiber.obj Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
          (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj U))
        y =
      u
Tactic: refine hP _ (fun Φ u ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
⊢ Epi f
have rw : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) f
Tactic: rw [← Sheaf.isLocallySurjective_iff_epi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Conservative (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
P : ObjectProperty (GrothendieckTopology.Point.{w, v, u} J)
inst_1 : LocallySmall.{w, v, u} C
inst_2 : HasSheafify J (Type w)
hP :
  ∀ ⦃X : C⦄ (S : Sieve.{v, u} X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj (P := P).fiber.obj X),
        ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := P).fiber.obj Y),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := P).fiber.map g) :
                (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
              y =
            x) →
      S ∈ (J : (a : C) → Set (Sieve a)) X
x x_1 : Sheaf J (Type w)
f : x ⟶ x_1
h : Mono f
hf :
  ∀ (i : P.FullSubcategory),
    IsIso (X := Functor.obj i.obj (P := P).sheafFiber x) (Functor.map i.obj (P := P).sheafFiber f)
⊢ IsIso f
have this : Epi f
Tactic: have : Epi f := by
          rw [← Sheaf.isLocallySurjective_iff_epi]
          exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.IsMonoidalW (goal)
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
⊢ J.W (X := tensorObj (𝒞 := Functor.category) X₁ Y₁) (f ⊗ₘ g)
have 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))
Tactic: simp only [hP.W_iff (A := A)] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.IsMonoidalW (goal)
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₁))
    (Functor.map Φ.obj (P := P).presheafFiber (f ⊗ₘ g))
have 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₂))
Tactic: rw [Functor.Monoidal.map_tensor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.IsMonoidalW (goal)
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
⊢ MorphismProperty.IsMonoidal (C := Functor.{v, v', u, u'} Cᵒᵖ A) J.W
have 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
Tactic: obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Map (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨U, u⟩ := u
Cleared hypotheses: u, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Map (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨V, g, hg, v, rfl⟩ :=
    Φ.jointly_surjective _ (F.cover_lift J K (K.pullback_stable f hR)) u
Cleared hypotheses: u