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
S : Sieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
h : S.arrows g
⊢ g = 𝟙 Z ≫ Over.Hom.left (Over.homMk g ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
h : S.arrows g
⊢ ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left), S.arrows (Over.Hom.left g_1) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
exact ⟨Over.mk ((g ≫ Y.hom)), Over.homMk g, 𝟙 _, h, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
h : ∀ ⦃Z : C⦄ (g : Z ⟶ Y.left), arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g ↔ arrows ⊤ g
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) ⊤

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

Tactic:
simp only [top_apply, iff_true]

Premises used: CategoryTheory.Sieve.top_apply, iff_true
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
h : ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left), ⊤ g_1 ∧ g = h ≫ Over.Hom.left g_1
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g

Tactic:
dsimp [overEquiv, Presieve.functorPushforward]

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
⊢ ⊤ (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
⊢ g = g ≫ Over.Hom.left (𝟙 Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
⊢ ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left), ⊤ g_1 ∧ g = h ≫ Over.Hom.left g_1

Tactic:
exact ⟨Y, 𝟙 Y, g, by simp, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Eq (α := Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ⊤) :
      Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤ : Sieve.{v, u} Y.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊥) ⊥

Tactic:
simp [overEquiv]

Premises used: CategoryTheory.Sieve.overEquiv
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
rw :
  Eq (α := Sieve Y)
    ((Equiv.symm
          { toFun := fun (S : Sieve Y) ↦ functorPushforward (Over.forget X) S,
            invFun := fun (S' : Sieve.{v, u} Y.left) ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
            right_inv := ⋯ } :
        (a : Sieve Y.left) → Sieve Y)
      ⊥)
    ⊥
rw₁ : Eq (α := Sieve Y) (functorPullback (Over.forget X) ⊥) ⊥
rw₂ rw₃ : Eq (α := Sieve Y) ⊥ ⊥
⊢ Eq (α := Sieve Y) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ⊥) ⊥

Tactic:
rw [overEquiv, Equiv.coe_fn_symm_mk, functorPullback_bot]

Premises used: Equiv.coe_fn_symm_mk, CategoryTheory.Sieve.functorPullback_bot, CategoryTheory.Sieve.overEquiv
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
⊢ LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
      ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left) ↔
    R₁ ≤ R₂

Tactic:
⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩

Premises used: CategoryTheory.Over.forget, CategoryTheory.Sieve.functorPushforward_monotone, Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
refine :
  ∀
    (h :
      LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
        ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left)),
    R₁ ≤ R₂
⊢ LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
      ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left) ↔
    R₁ ≤ R₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
h :
  LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left)
⊢ LE.le (α := Sieve Y)
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁) : Sieve Y)
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂) : Sieve Y)

Tactic:
replace h : (overEquiv Y).symm (R₁.overEquiv Y) ≤ (overEquiv Y).symm (R₂.overEquiv Y) :=
    Sieve.functorPullback_monotone _ _ h
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
h :
  LE.le (α := Sieve Y)
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁) : Sieve Y)
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂) : Sieve Y)
⊢ R₁ ≤ R₂

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
h :
  ∀ ⦃Z : C⦄ (g : Z ⟶ Y₁.left),
    arrows ((overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S)) g ↔
      (pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)).arrows g
⊢ (overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S) =
    pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) ↔
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
      S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
⊢ arrows ((overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S)) g ↔
    (pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)).arrows g

Tactic:
dsimp [overEquiv, Presieve.functorPushforward]

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) →
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
      S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
h₁ :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
      S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1
⊢ (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) ↔
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
      S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over.{v, u} X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ (b ≫ Over.Hom.left a) ≫ Over.Hom.left f = b ≫ Over.Hom.left (a ≫ f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over.{v, u} X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ ∃ (Z_1 : Over.{v, u} X) (g : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
    S.arrows g ∧ (b ≫ Over.Hom.left a) ≫ Over.Hom.left f = h ≫ Over.Hom.left g

Tactic:
exact ⟨W, a ≫ f, b, h, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
dsimp : g ≫ Y₁.hom = b ≫ W.hom
⊢ g ≫ Y₁.hom = T.hom

Tactic:
dsimp [T]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
rw : g ≫ Y₁.hom = b ≫ Over.Hom.left a ≫ Y₂.hom
rw₁ : g ≫ Y₁.hom = g ≫ Over.Hom.left f ≫ Y₂.hom
rw₂ rw₃ : g ≫ Y₁.hom = g ≫ Y₁.hom
⊢ g ≫ Y₁.hom = b ≫ W.hom

Tactic:
rw [← Over.w a, ← reassoc_of% w, Over.w f]

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ g = 𝟙 Z ≫ Over.Hom.left c

Tactic:
simp [T, c]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
h₁ : S.arrows (c ≫ f)
⊢ ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
h₁ : Over.Hom.left (c ≫ f) = Over.Hom.left (d ≫ a)
⊢ c ≫ f = d ≫ a

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ Over.Hom.left (c ≫ f) = Over.Hom.left (d ≫ a)

Tactic:
w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ Over.Hom.left (c ≫ f) = Over.Hom.left (d ≫ a)

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
h₁ : S.arrows (d ≫ a)
⊢ S.arrows (c ≫ f)

Tactic:
rw [show c ≫ f = d ≫ a by ext; exact w]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)

Tactic:
S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)

Tactic:
exact S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve.{v, u} Y₂.left
⊢ ((overEquiv Y₁).symm : (a : Sieve Y₁.left) → Sieve Y₁) (pullback (Over.Hom.left f) S) =
    pullback f (((overEquiv Y₂).symm : (a : Sieve Y₂.left) → Sieve Y₂) S)

Tactic:
functorPullback_pullback _ _ _

Premises used: CategoryTheory.Sieve.functorPullback_pullback, CategoryTheory.Sieve.functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : Over.{v, u} X
f : Z ⟶ Y
⊢ arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S) f ↔ S.arrows (Over.Hom.left f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : C
f : Z ⟶ Y.left
obtain :
  ∀ (S : Sieve.{v, u} Y.left),
    arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S)) f ↔
      arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S : Sieve Y) (Y := Over.mk (f ≫ Y.hom))
        (Over.homMk f ⋯ : Over.mk (f ≫ Y.hom) ⟶ Y)
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) S) f ↔ S.arrows (Y := Over.mk (f ≫ Y.hom)) (Over.homMk f ⋯)

Tactic:
obtain ⟨S, rfl⟩ := (overEquiv Y).symm.surjective S

Premises used: CategoryTheory.Sieve.overEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
f : Z ⟶ Y.left
S : Sieve.{v, u} Y.left
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S)) f ↔
    arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) S : Sieve Y) (Y := Over.mk (f ≫ Y.hom))
      (Over.homMk f ⋯ : Over.mk (f ≫ Y.hom) ⟶ Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
I : Type u_1
Z : I → Over.{v, u} X
g : (i : I) → Z i ⟶ Y
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (ofArrows Z g) : Sieve.{v, u} Y.left)
    (ofArrows (fun (i : I) ↦ (Z i).left) fun (i : I) ↦ Over.Hom.left (g i) : Sieve.{v, u} Y.left)

Tactic:
simp [Sieve.overEquiv, functorPushforward_ofArrows]

Premises used: CategoryTheory.Sieve.overEquiv, CategoryTheory.Sieve.functorPushforward_ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h :
  ∀ ⦃Y_1 : C⦄ (f : Y_1 ⟶ W.left),
    arrows ((overEquiv W : (a : Sieve W) → Sieve W.left) (E.sieve₁ p₁ p₂)) f ↔
      ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f
⊢ (overEquiv W : (a : Sieve W) → Sieve W.left) (E.sieve₁ p₁ p₂) =
    (E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y_1 : C
f : Y_1 ⟶ W.left
h :
  (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f ⋯) ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f
⊢ arrows ((overEquiv W : (a : Sieve W) → Sieve W.left) (E.sieve₁ p₁ p₂)) f ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f

Tactic:
rw [overEquiv_iff]

Premises used: CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y_1 : C
f : Y_1 ⟶ W.left
⊢ (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f ⋯) ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f

Tactic:
⟨fun ⟨k, b, hb₁, hb₂⟩ ↦ ⟨k, b.left, congr($(hb₁).left), congr($(hb₂).left)⟩, ?_⟩

Premises used: congrArg, CategoryTheory.Over.Hom.left, CategoryTheory.PreOneHypercover.map, CategoryTheory.Over.forget, id, _private.0.CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁.match_1, CategoryTheory.Sieve.arrows, And.intro, Iff.intro, Exists.intro, CategoryTheory.PreOneHypercover.sieve₁
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y_1 : C
f : Y_1 ⟶ W.left
h :
  ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f →
    (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f ⋯)
⊢ (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f ⋯) ↔
    ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f

Tactic:
refine ⟨fun ⟨k, b, hb₁, hb₂⟩ ↦ ⟨k, b.left, congr($(hb₁).left), congr($(hb₂).left)⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y_1 : C
f : Y_1 ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y_1 ⟶ (E.map (Over.forget X)).Y k
hb₁ : f ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ b ≫ (E.Y k).hom = (Over.mk (f ≫ W.hom)).hom

Tactic:
simpa using (hb₁ =≫ (E.X i₁).hom).symm

Premises used: CategoryTheory.eq_whisker, CategoryTheory.PreOneHypercover.toPreZeroHypercover, CategoryTheory.PreZeroHypercover.X, Eq.symm, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over.{v, u} X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y_1 : C
f : Y_1 ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y_1 ⟶ (E.map (Over.forget X)).Y k
hb₁ : f ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f ⋯)

Tactic:
exact ⟨k, Over.homMk b (by simpa using (hb₁ =≫ (E.X i₁).hom).symm), by cat_disch, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R) : Sieve.{v, u} Y.left)
    (generate (Presieve.functorPushforward (Over.forget X) R) : Sieve.{v, u} Y.left)

Tactic:
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 Y
refine_1 :
  ∀ (Z : C) (g : Z ⟶ Y.left) (hg : arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R)) g),
    arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g
refine_2 :
  LE.le (α := Sieve.{v, u} Y.left) (generate (Presieve.functorPushforward (Over.forget X) R) : Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R) : Sieve.{v, u} Y.left)
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R) : Sieve.{v, u} Y.left)
    (generate (Presieve.functorPushforward (Over.forget X) R) : Sieve.{v, u} Y.left)

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 Y
Z : C
g : Z ⟶ Y.left
hg : arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R)) g
⊢ (generate R).arrows (Y := Over.mk (g ≫ Y.hom)) (Over.homMk g ⋯)

Tactic:
rw [overEquiv_iff] at hg

Premises used: CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : (generate R).arrows (Y := Over.mk (g ≫ Y.hom)) (Over.homMk g ⋯)
refine_1 :
  ∀ (W : Over.{v, u} X) (u : Over.mk (g ≫ Y.hom) ⟶ W) (v : W ⟶ Y) (hv : R v) (huv : u ≫ v = Over.homMk g ⋯),
    arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g
⊢ arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g

Tactic:
obtain ⟨W, u, v, hv, huv⟩ := hg
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
W : Over.{v, u} X
u : Over.mk (g ≫ Y.hom) ⟶ W
v : W ⟶ Y
hv : R v
huv : u ≫ v = Over.homMk g ⋯
⊢ Over.Hom.left v = 𝟙 W.left ≫ Functor.map (Over.forget X) v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
W : Over.{v, u} X
u : Over.mk (g ≫ Y.hom) ⟶ W
v : W ⟶ Y
hv : R v
huv : u ≫ v = Over.homMk g ⋯
⊢ arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g

Tactic:
exact ⟨W.left, u.left, v.left, ⟨W, v, 𝟙 _, hv, by simp⟩, congr($(huv).left)⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
refine_2 :
  LE.le (α := Presieve.{v, u} Y.left)
    (Presieve.functorPushforward (Over.forget X) R : Presieve.{v, u} (Functor.obj (Over.forget X) Y))
    (arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R)))
⊢ LE.le (α := Sieve.{v, u} Y.left) (generate (Presieve.functorPushforward (Over.forget X) R) : Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R) : Sieve.{v, u} Y.left)

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 Y
Z : C
W : Over.{v, u} X
u : W ⟶ Y
v : Z ⟶ Functor.obj (Over.forget X) W
hu : R u
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R)) (v ≫ Functor.map (Over.forget X) u)

Tactic:
(overEquiv_iff _ _).mpr ⟨W, Over.homMk v, u, hu, rfl⟩

Premises used: Iff.mpr, CategoryTheory.Over.homMk, And.intro, Exists.intro, rfl, CategoryTheory.Sieve.overEquiv_iff
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
Z : C
W : Over.{v, u} X
u : W ⟶ Y
v : Z ⟶ Functor.obj (Over.forget X) W
hu : R u
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) (generate R)) (v ≫ Functor.map (Over.forget X) u)

Tactic:
exact (overEquiv_iff _ _).mpr ⟨W, Over.homMk v, u, hu, rfl⟩
-- 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
⊢ 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:
le_antisymm (fun Z g hg ↦ ?_) ?_

Premises used: le_antisymm