awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
refine_1 :
  ∀ (Z : Over.{v, u} X) (g : Z ⟶ Y) (hg : arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)) g),
    arrows (generate (Presieve.functorPullback (Over.forget X) R)) g
refine_2 :
  LE.le (α := Sieve Y) (generate (Presieve.functorPullback (Over.forget X) R))
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R))
⊢ Eq (α := Sieve Y) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R) : Sieve Y)
    (generate (Presieve.functorPullback (Over.forget X) R) : Sieve Y)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
hg : arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)) g
⊢ (generate R).arrows (Over.Hom.left g)

Tactic:
rw [overEquiv_symm_iff] at hg

Premises used: CategoryTheory.Sieve.overEquiv_symm_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
hg : (generate R).arrows (Over.Hom.left g)
refine_1 :
  ∀ (W : C) (p : Z.left ⟶ W) (q : W ⟶ Y.left) (hq : R q) (hpq : p ≫ q = Over.Hom.left g),
    arrows (generate (Presieve.functorPullback (Over.forget X) R)) g
⊢ arrows (generate (Presieve.functorPullback (Over.forget X) R)) g

Tactic:
obtain ⟨W, p, q, hq, hpq⟩ := hg
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ p ≫ (Over.mk (q ≫ Y.hom)).hom = Z.hom

Tactic:
simp [reassoc_of% hpq]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
refine_1 : CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯) = g
⊢ arrows (generate (Presieve.functorPullback (Over.forget X) R)) g

Tactic:
refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
refine_1 :
  Over.Hom.left (CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯)) = Over.Hom.left g
⊢ CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯) = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ Over.Hom.left (CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯)) = Over.Hom.left g

Tactic:
hpq
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : Over.{v, u} X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ Over.Hom.left (CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯)) = Over.Hom.left g

Tactic:
exact hpq
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
refine_2 :
  LE.le (α := Presieve Y) (Presieve.functorPullback (Over.forget X) R)
    (arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)))
⊢ LE.le (α := Sieve Y) (generate (Presieve.functorPullback (Over.forget X) R))
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R))

Tactic:
rw [generate_le_iff]

Premises used: CategoryTheory.Sieve.generate_le_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
⊢ LE.le (α := Presieve Y) (Presieve.functorPullback (Over.forget X) R)
    (arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)))

Tactic:
fun Z g hg ↦ le_generate _ _ _ hg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Over.forget, CategoryTheory.Functor.map, CategoryTheory.Presieve.functorPullback, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
⊢ LE.le (α := Presieve Y) (Presieve.functorPullback (Over.forget X) R)
    (arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)))

Tactic:
exact fun Z g hg ↦ le_generate _ _ _ hg

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
h :
  ∀ ⦃W : Over.{v, u} Y⦄ (g : W ⟶ (Over.map f).obj Z),
    arrows (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S)) g ↔
      arrows
        (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S)
        g
⊢ Eq (α := Sieve ((Over.map f).obj Z))
    (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S))
    (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S)

Tactic:
ext W g
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
W : Over.{v, u} Y
g : W ⟶ (Over.map f).obj Z
h :
  arrows (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S)) g →
    arrows
      (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S) g
h₁ :
  arrows
      (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S)
      g →
    arrows (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S)) g
⊢ arrows (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S)) g ↔
    arrows
      (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S) g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
W : Over.{v, u} Y
T : Over.{v, u} X
a : T ⟶ Z
b : W ⟶ (Over.map f).obj T
ha : arrows (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S) a
⊢ arrows
    (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S)
    (b ≫ (Over.map f).map a)

Tactic:
S.downward_closed ha _

Premises used: CategoryTheory.Over, CategoryTheory.Sieve.downward_closed, CategoryTheory.CostructuredArrow, CategoryTheory.Presieve.functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
W : Over.{v, u} Y
T : Over.{v, u} X
a : T ⟶ Z
b : W ⟶ (Over.map f).obj T
ha : arrows (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S) a
⊢ arrows
    (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S)
    (b ≫ (Over.map f).map a)

Tactic:
exact S.downward_closed ha _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
W : Over.{v, u} Y
g : W ⟶ (Over.map f).obj Z
hg :
  arrows
    (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S) g
⊢ 𝟙 W.left ≫ ((Over.map f).obj (Over.mk (Over.Hom.left g ≫ Z.hom))).hom = W.hom

Tactic:
simpa using Over.w g

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over.{v, u} X
S : Sieve.{v, u} Z.left
W : Over.{v, u} Y
g : W ⟶ (Over.map f).obj Z
hg :
  arrows
    (((overEquiv ((Over.map f).obj Z)).symm : (a : Sieve ((Over.map f).obj Z).left) → Sieve ((Over.map f).obj Z)) S) g
⊢ arrows (functorPushforward (Over.map f) (((overEquiv Z).symm : (a : Sieve Z.left) → Sieve Z) S)) g

Tactic:
exact ⟨Over.mk (g.left ≫ Z.hom), Over.homMk g.left,
      Over.homMk (𝟙 _) (by simpa using Over.w g), hg, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
h :
  ∀ ⦃Z : C⦄ (g : Z ⟶ U.left),
    arrows ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.map f) S)) g ↔
      arrows ((overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S) g
⊢ Eq (α := Sieve.{v, u} U.left)
    ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.map f) S) : Sieve.{v, u} U.left)
    ((overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S :
      Sieve.{v, u} ((Over.map f).obj U).left)

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
⊢ 𝟙 Z ≫ (Over.mk (g ≫ U.hom ≫ f)).hom = ((Over.map f).obj (Over.mk (g ≫ U.hom))).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
h :
  Eq (α := ((Over.map f).obj (Over.mk (g ≫ U.hom))).left ⟶ ((Over.map f).obj U).left)
    (Over.Hom.left ((Over.map f).map (Over.homMk g ⋯))) (Over.Hom.left (u ≫ Over.homMk g ⋯))
⊢ Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
⊢ Eq (α := ((Over.map f).obj (Over.mk (g ≫ U.hom))).left ⟶ ((Over.map f).obj U).left)
    (Over.Hom.left ((Over.map f).map (Over.homMk g ⋯))) (Over.Hom.left (u ≫ Over.homMk g ⋯))

Tactic:
simp [u]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
⊢ Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)

Tactic:
have heq : (Over.map f).map (Over.homMk (U := Over.mk (g ≫ U.hom)) g rfl) =
      u ≫ Over.homMk (V := (Over.map f).obj U) g rfl := by
    ext
    simp [u]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
⊢ 𝟙 Z ≫ ((Over.map f).obj (Over.mk (g ≫ U.hom))).hom = (Over.mk (g ≫ U.hom ≫ f)).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
h : Over.Hom.left (u ≫ Over.homMk (𝟙 Z) ⋯) = Over.Hom.left (𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom))))
⊢ u ≫ Over.homMk (𝟙 Z) ⋯ = 𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
⊢ Over.Hom.left (u ≫ Over.homMk (𝟙 Z) ⋯) = Over.Hom.left (𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom))))

Tactic:
simp [u]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
h : Over.Hom.left (Over.homMk (𝟙 Z) ⋯ ≫ u) = Over.Hom.left (𝟙 (Over.mk (g ≫ U.hom ≫ f)))
⊢ Over.homMk (𝟙 Z) ⋯ ≫ u = 𝟙 (Over.mk (g ≫ U.hom ≫ f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
⊢ Over.Hom.left (Over.homMk (𝟙 Z) ⋯ ≫ u) = Over.Hom.left (𝟙 (Over.mk (g ≫ U.hom ≫ f)))

Tactic:
simp [u]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
⊢ IsIso u

Tactic:
have : IsIso u :=
    ⟨Over.homMk (𝟙 Z) (by simp), by ext; simp [u], by ext; simp [u]⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
this : IsIso u
h :
  (functorPullback (Over.map f) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g ⋯) ↔
    S.arrows (Y := Over.mk (g ≫ ((Over.map f).obj U).hom)) (Over.homMk g ⋯)
⊢ arrows ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.map f) S)) g ↔
    arrows ((overEquiv ((Over.map f).obj U) : (a : Sieve ((Over.map f).obj U)) → Sieve ((Over.map f).obj U).left) S) g

Tactic:
rw [Sieve.overEquiv_iff, Sieve.overEquiv_iff]

Premises used: CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over.{v, u} X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq :
  Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g ⋯))
    (u ≫ Over.homMk g ⋯)
this : IsIso u
⊢ (functorPullback (Over.map f) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g ⋯) ↔
    S.arrows (Y := Over.mk (g ≫ ((Over.map f).obj U).hom)) (Over.homMk g ⋯)

Tactic:
simp [Presieve.functorPullback, heq]

Premises used: CategoryTheory.Presieve.functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
⊢ Eq (α := Sieve.{v, u} U.left)
    ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S) : Sieve.{v, u} U.left)
    (functorPullback F
        ((overEquiv (Functor.obj (Over.post F) U) :
            (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
          S) :
      Sieve.{v, u} U.left)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
refine_1 :
  LE.le (α := Sieve.{v, u} U.left)
    ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S) : Sieve.{v, u} U.left)
    (functorPullback F
        ((overEquiv (Functor.obj (Over.post F) U) :
            (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
          S) :
      Sieve.{v, u} U.left)
refine_2 :
  LE.le (α := Sieve.{v, u} U.left)
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S))
⊢ Eq (α := Sieve.{v, u} U.left)
    ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S) : Sieve.{v, u} U.left)
    (functorPullback F
        ((overEquiv (Functor.obj (Over.post F) U) :
            (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
          S) :
      Sieve.{v, u} U.left)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
refine_1 :
  functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)
⊢ LE.le (α := Sieve.{v, u} U.left)
    (functorPushforward (Over.forget X) (functorPullback (Over.post F) S) :
      Sieve.{v, u} (Functor.obj (Over.forget X) U))
    (functorPullback F (functorPushforward (Over.forget (F.obj X)) S))

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback, ← Sieve.functorPullback_comp]

Premises used: CategoryTheory.Sieve.functorPullback_comp, CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
refine_1 :
  functorPullback (Over.post F) S ≤
    functorPullback (Over.post F)
      (functorPullback (Over.forget (F.obj X)) (functorPushforward (Over.forget (F.obj X)) S))
⊢ functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)

Tactic:
simp_rw [← CategoryTheory.Over.post_forget_eq_forget_comp, Sieve.functorPullback_comp]

Premises used: CategoryTheory.Sieve.functorPullback_comp, CategoryTheory.Over.post_forget_eq_forget_comp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
⊢ functorPullback (Over.post F) S ≤
    functorPullback (Over.post F)
      (functorPullback (Over.forget (F.obj X)) (functorPushforward (Over.forget (F.obj X)) S))

Tactic:
Sieve.functorPullback_monotone _ _ (Sieve.le_functorPushforward_pullback _ _)

Premises used: CategoryTheory.Sieve.functorPullback_monotone, CategoryTheory.Sieve.le_functorPushforward_pullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
⊢ functorPullback (Over.post F) S ≤
    functorPullback (Over.post F)
      (functorPullback (Over.forget (F.obj X)) (functorPushforward (Over.forget (F.obj X)) S))

Tactic:
exact Sieve.functorPullback_monotone _ _ (Sieve.le_functorPushforward_pullback _ _)

Premises used: CategoryTheory.Sieve.functorPullback_monotone, CategoryTheory.Sieve.le_functorPushforward_pullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
Z : C
g : Z ⟶ U.left
hg :
  arrows
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    g
refine_2 : (functorPullback (Over.post F) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g ⋯)
⊢ arrows ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S)) g

Tactic:
rw [Sieve.overEquiv_iff]

Premises used: CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
Z : C
g : Z ⟶ U.left
hg :
  arrows
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    g
refine_2 : S.arrows (Y := Over.mk (F.map (g ≫ U.hom))) (Over.homMk (F.map g) ⋯)
⊢ (functorPullback (Over.post F) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g ⋯)

Tactic:
dsimp [Presieve.functorPullback]

Premises used: CategoryTheory.Presieve.functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
Z : C
g : Z ⟶ U.left
hg :
  arrows
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    g
⊢ S.arrows (Y := Over.mk (F.map g ≫ (Functor.obj (Over.post F) U).hom)) (Over.homMk (F.map g) ⋯)

Tactic:
(Sieve.overEquiv_iff _ _).mp hg

Premises used: Iff.mp, CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
Z : C
g : Z ⟶ U.left
hg :
  arrows
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    g
h : F.map (g ≫ U.hom) = F.map g ≫ (Functor.obj (Over.post F) U).hom
⊢ S.arrows (Y := Over.mk (F.map (g ≫ U.hom))) (Over.homMk (F.map g) ⋯)

Tactic:
convert! (Sieve.overEquiv_iff _ _).mp hg

Premises used: Iff.mp, CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
X : C
U : Over.{v, u} X
S : Sieve (Functor.obj (Over.post F) U)
Z : C
g : Z ⟶ U.left
hg :
  arrows
    (functorPullback F
      ((overEquiv (Functor.obj (Over.post F) U) : (a : Sieve ((Over.post F).obj U)) → Sieve ((Over.post F).obj U).left)
        S))
    g
⊢ F.map (g ≫ U.hom) = F.map g ≫ (Functor.obj (Over.post F) U).hom

Tactic:
simp