awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
⊢ S ≤ functorPullback F (functorPushforward F S)

Tactic:
Sieve.le_functorPushforward_pullback _ _

Premises used: CategoryTheory.Sieve.le_functorPushforward_pullback
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
⊢ S ≤ functorPullback F (functorPushforward F S)

Tactic:
exact Sieve.le_functorPushforward_pullback _ _

Premises used: CategoryTheory.Sieve.le_functorPushforward_pullback
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y Z : C
f : Y ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
apply : ∀ (b : Sieve.{v₂, u₂} (F.obj X)), b ≤ functorPushforward F (functorPullback F b)
⊢ GaloisInsertion (α := Sieve.{v₁, u₁} X) (functorPushforward F) (functorPullback F)

Tactic:
apply (functor_galoisConnection F X).toGaloisInsertion

Premises used: GaloisConnection.toGaloisInsertion, CategoryTheory.Sieve.functor_galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
S : Sieve.{v₂, u₂} (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPushforward F (functorPullback F S)).arrows f

Tactic:
⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, ?_⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.objObjPreimageIso, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
S : Sieve.{v₂, u₂} (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
refine :
  (functorPullback F S).arrows (Y := F.objPreimage Y) (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)) ∧
    f =
      CategoryStruct.comp (Y := F.obj (F.objPreimage Y)) (Iso.inv (F.objObjPreimageIso Y))
        (F.map (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)))
⊢ (functorPushforward F (functorPullback F S)).arrows f

Tactic:
refine ⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
S : Sieve.{v₂, u₂} (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPullback F S).arrows (Y := F.objPreimage Y) (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)) ∧
    f =
      CategoryStruct.comp (Y := F.obj (F.objPreimage Y)) (Iso.inv (F.objObjPreimageIso Y))
        (F.map (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)))

Tactic:
simpa using hf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y Z : C
f : Y ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
apply : ∀ (b : Sieve.{v₁, u₁} X), functorPullback F (functorPushforward F b) ≤ b
⊢ GaloisCoinsertion (α := Sieve.{v₁, u₁} X) (functorPushforward F) (functorPullback F)

Tactic:
apply (functor_galoisConnection F X).toGaloisCoinsertion

Premises used: GaloisConnection.toGaloisCoinsertion, CategoryTheory.Sieve.functor_galoisConnection
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = h ≫ F.map g
⊢ F.map f = F.map (F.preimage h ≫ g)

Tactic:
rw [← F.map_preimage h, ← F.map_comp] at h₂

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
rw : S.arrows (F.preimage h ≫ g)
⊢ S.arrows f

Tactic:
rw [F.map_injective h₂]

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows (F.preimage h ≫ g)

Tactic:
S.downward_closed h₁ _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows (F.preimage h ≫ g)

Tactic:
exact S.downward_closed h₁ _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
S : Sieve.{v₁, u₁} X
inst_2 : F.Full
inst_3 : F.Faithful
⊢ functorPullback F (functorPushforward F S) = S

Tactic:
(Sieve.fullyFaithfulFunctorGaloisCoinsertion _ _).u_l_eq _

Premises used: CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion, GaloisCoinsertion.u_l_eq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
h :
  ∀ ⦃Y : D⦄ (iYX : Y ⟶ e.functor.obj X),
    (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)

Tactic:
ext Y iYX
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
h : (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
h₁ : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
Z : C
iZX : Z ⟶ X
iYZ : Y ⟶ e.functor.obj Z
hiZX : S.arrows iZX
⊢ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows (iYZ ≫ e.functor.map iZX)

Tactic:
simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Equivalence.unitInv, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
simpa using H
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ iYX = e.counitInv.app Y ≫ e.functor.map (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX

Tactic:
exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
Y : D
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows f ↔ S.arrows (e.inverse.map f ≫ e.unitInv.app X)

Tactic:
congr($(S.functorPushforward_functor e).arrows f)

Premises used: congrArg, id, CategoryTheory.Sieve.arrows, CategoryTheory.Sieve.functorPushforward_functor, iff_of_eq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : D
S : Sieve.{v₂, u₂} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ functorPushforward e.inverse S = functorPullback e.functor (pullback (e.counit.app X) S)

Tactic:
Sieve.functorPushforward_functor S e.symm

Premises used: CategoryTheory.Sieve.functorPushforward_functor, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
Y : C
X : D
S : Sieve.{v₂, u₂} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
f : Y ⟶ e.inverse.obj X
⊢ (functorPushforward e.inverse S).arrows f ↔ S.arrows (e.functor.map f ≫ e.counit.app X)

Tactic:
congr($(S.functorPushforward_inverse e).arrows f)

Premises used: congrArg, id, CategoryTheory.Sieve.arrows, CategoryTheory.Sieve.functorPushforward_inverse, iff_of_eq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
U : C
S : Sieve.{v₁, u₁} U
h :
  ∀ ⦃Y : C⦄ (f : Y ⟶ e.inverse.obj (e.functor.obj U)),
    (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f ↔ (pullback (e.unitInv.app U) S).arrows f
⊢ functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
U : C
S : Sieve.{v₁, u₁} U
Y : C
f : Y ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f ↔ (pullback (e.unitInv.app U) S).arrows f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : C
S : Sieve.{v₁, u₁} X
h :
  ∀ ⦃Y : C⦄ (f : Y ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X),
    (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f ↔ S.arrows f
⊢ pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f ↔ S.arrows f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

Tactic:
⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, hg⟩ ↦ ?_⟩

Premises used: Exists, _private.0.CategoryTheory.Sieve.mem_functorPushforward_iff_of_full.match_1, CategoryTheory.Sieve.arrows, _private.0.CategoryTheory.Sieve.mem_functorPushforward_iff_of_full.match_2, CategoryTheory.Functor.map, And, Iff.intro, Eq, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
refine_1 :
  Presieve.functorPushforward F R.arrows f →
    ∀ (Z : C) (g : Z ⟶ X) (h : F.obj Y ⟶ F.obj Z) (hg : R.arrows g) (hcomp : f = h ≫ F.map g),
      ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
refine_2 :
  (∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g) →
    ∀ (g : Y ⟶ X) (hcomp : F.map g = f) (hg : R.arrows g), Presieve.functorPushforward F R.arrows f
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

Tactic:
refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, hg⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
refine_1 : ∀ (h' : Y ⟶ Z) (hh' : F.map h' = h), ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
⊢ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

Tactic:
obtain ⟨h', hh'⟩ := F.map_surjective h

Premises used: CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
h₁ : F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)
⊢ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

Tactic:
use h' ≫ g
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
h₁ : R.arrows (h' ≫ g)
⊢ F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)

Tactic:
simp only [Functor.map_comp, hh', hcomp, true_and]

Premises used: CategoryTheory.Functor.map_comp, true_and
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ R.arrows (h' ≫ g)

Tactic:
apply R.downward_closed hg

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h : ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
right : f = 𝟙 (F.obj Y) ≫ F.map g
⊢ Presieve.functorPushforward F R.arrows f

Tactic:
use Y, g, 𝟙 _, hg

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h : ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ f = 𝟙 (F.obj Y) ≫ F.map g

Tactic:
simp [hcomp]
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
rw : (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

Tactic:
rw [Sieve.mem_functorPushforward_iff_of_full]

Premises used: CategoryTheory.Sieve.mem_functorPushforward_iff_of_full
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
⊢ (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f

Tactic:
⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩

Premises used: CategoryTheory.Sieve.arrows, And.intro, Iff.intro, Exists.intro, rfl, _private.0.CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful.match_1
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
refine :
  (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) →
    ∀ (g : Y ⟶ X) (hcomp : F.map g = F.map f) (hg : R.arrows g), R.arrows f
⊢ (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f

Tactic:
refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
h : ∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = F.map f
hg rwa rwa₁ rwa₂ rwa₃ : R.arrows g
⊢ R.arrows f

Tactic:
rwa [← F.map_injective hcomp]

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
I : Type u_1
X : I → C
Y : C
Z : D
f : Z ⟶ F.obj Y
W : C
g₁ : W ⟶ Y
g₂ : Z ⟶ F.obj W
hf : f = g₂ ≫ F.map g₁
i : I
g₃ : W ⟶ X i
⊢ arrows (ofObjects (F.obj ∘ X) (F.obj Y)) f

Tactic:
⟨i, ⟨g₂ ≫ F.map g₃⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
I : Type u_1
X : I → C
Y : C
Z : D
f : Z ⟶ F.obj Y
W : C
g₁ : W ⟶ Y
g₂ : Z ⟶ F.obj W
hf : f = g₂ ≫ F.map g₁
i : I
g₃ : W ⟶ X i
⊢ arrows (ofObjects (F.obj ∘ X) (F.obj Y)) f

Tactic:
exact ⟨i, ⟨g₂ ≫ F.map g₃⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S T : Sieve.{v₁, u₁} X
h : S ≤ T
⊢ natTransOfLe h ≫ T.functorInclusion = S.functorInclusion

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, TypeCat.Fun.comp, CategoryTheory.Sieve.functorInclusion, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
Z_1 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : Z_1 ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
w :
  ∀ (Y : Cᵒᵖ) (y : Z_1.obj Y), (hom (FC := TypeCat.Fun) (f.app Y)).toFun y = (hom (FC := TypeCat.Fun) (g.app Y)).toFun y
⊢ f = g

Tactic:
ext Y y
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z : C
f_1 : Y_1 ⟶ X
S R : Sieve.{v₁, u₁} X
Z_1 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : Z_1 ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
Y : Cᵒᵖ
y : Z_1.obj Y
⊢ (hom (FC := TypeCat.Fun) (f.app Y)).toFun y = (hom (FC := TypeCat.Fun) (g.app Y)).toFun y

Tactic:
simpa [Subtype.ext_iff] using congr_hom (NatTrans.congr_app h Y) y

Premises used: Subtype.ext_iff, CategoryTheory.NatTrans.congr_app, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : R ⟶ Functor.obj yoneda X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ ∃ (t_1 : R.obj (Opposite.op Z)),
    Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
          t_1 :
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      (g ≫
          (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
              (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
                (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
            t :
        Z ⟶ X)

Tactic:
⟨R.map g.op t, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, Exists.intro, DFunLike.coe