awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯
⊢ ∃ (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
have h₁ : S.arrows (c ≫ f)
Tactic: refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯
⊢ c ≫ f = d ≫ a
have h₁ : Over.Hom.left (c ≫ f) = Over.Hom.left (d ≫ a)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 (c ≫ f)
have h₁ : S.arrows (d ≫ a)
Tactic: rw [show c ≫ f = d ≫ a by ext; exact w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) S) f ↔ S.arrows (Y := Over.mk (f ≫ Y.hom)) (Over.homMk f ⋯)
have 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 sorry : Over.mk (f ≫ Y.hom) ⟶ Y)
Tactic: obtain ⟨S, rfl⟩ := (overEquiv Y).symm.surjective S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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₂
⊢ (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₂)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have h : (E.sieve₁ p₁ p₂).arrows (Y := Over.mk (f ≫ W.hom)) (Over.homMk f sorry) ↔
  ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f
Tactic: rw [overEquiv_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
have 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 sorry)
Tactic: refine ⟨fun ⟨k, b, hb₁, hb₂⟩ ↦ ⟨k, b.left, congr($(hb₁).left), congr($(hb₂).left)⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
have 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
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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)
have 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)
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
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
⊢ arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g
have hg₁ : (generate R).arrows (Y := Over.mk (g ≫ Y.hom)) (Over.homMk g sorry)
Tactic: rw [overEquiv_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯)
⊢ arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g
have 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 sorry),
  arrows (generate (Presieve.functorPushforward (Over.forget X) R)) g
Tactic: obtain ⟨W, u, v, hv, huv⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve Y
⊢ 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)
have 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)))
Tactic: rw [generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
have 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
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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)
have refine_2 : LE.le (α := Sieve Y) (generate (Presieve.functorPullback (Over.forget X) R))
  (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R))
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
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
⊢ arrows (generate (Presieve.functorPullback (Over.forget X) R)) g
have hg₁ : (generate R).arrows (Over.Hom.left g)
Tactic: rw [overEquiv_symm_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
⊢ arrows (generate (Presieve.functorPullback (Over.forget X) R)) g
have 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
Tactic: obtain ⟨W, p, q, hq, hpq⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ arrows (generate (Presieve.functorPullback (Over.forget X) R)) g
have refine_1 : CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p sorry) (Over.homMk q sorry) = g
Tactic: refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p ⋯) (Over.homMk q ⋯) = g
have refine_1 : Over.Hom.left (CategoryStruct.comp (Y := Over.mk (q ≫ Y.hom)) (Over.homMk p sorry) (Over.homMk q sorry)) = Over.Hom.left g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
⊢ LE.le (α := Sieve Y) (generate (Presieve.functorPullback (Over.forget X) R))
    (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R))
have refine_2 : LE.le (α := Presieve Y) (Presieve.functorPullback (Over.forget X) R)
  (arrows (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) (generate R)))
Tactic: rw [generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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)
have 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
Tactic: ext W g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
⊢ 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)
have 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
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯)
have 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 sorry))) (Over.Hom.left (u ≫ Over.homMk g sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
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) ⋯
⊢ 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
have heq : Eq (α := (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ (Over.map f).obj U) ((Over.map f).map (Over.homMk g sorry))
  (u ≫ Over.homMk g sorry)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯)
⊢ u ≫ Over.homMk (𝟙 Z) ⋯ = 𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom)))
have h : Over.Hom.left (u ≫ Over.homMk (𝟙 Z) sorry) = Over.Hom.left (𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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.homMk (𝟙 Z) ⋯ ≫ u = 𝟙 (Over.mk (g ≫ U.hom ≫ f))
have h : Over.Hom.left (Over.homMk (𝟙 Z) sorry ≫ u) = Over.Hom.left (𝟙 (Over.mk (g ≫ U.hom ≫ f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
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 ⋯)
⊢ 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
have this : IsIso u
Tactic: have : IsIso u :=
    ⟨Over.homMk (𝟙 Z) (by simp), by ext; simp [u], by ext; simp [u]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have h : (functorPullback (Over.map f) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g sorry) ↔
  S.arrows (Y := Over.mk (g ≫ ((Over.map f).obj U).hom)) (Over.homMk g sorry)
Tactic: rw [Sieve.overEquiv_iff, Sieve.overEquiv_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
have 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)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
⊢ 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)
have 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))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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)
⊢ 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))
have refine_1 : functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)
Tactic: rw [Sieve.functorPushforward_le_iff_le_functorPullback, ← Sieve.functorPullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)
have refine_1 : functorPullback (Over.post F) S ≤
  functorPullback (Over.post F) (functorPullback (Over.forget (F.obj X)) (functorPushforward (Over.forget (F.obj X)) S))
Tactic: simp_rw [← CategoryTheory.Over.post_forget_eq_forget_comp, Sieve.functorPullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ arrows ((overEquiv U : (a : Sieve U) → Sieve U.left) (functorPullback (Over.post F) S)) g
have refine_2 : (functorPullback (Over.post F) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g sorry)
Tactic: rw [Sieve.overEquiv_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ (functorPullback (Over.post F) S).arrows (Y := Over.mk (g ≫ U.hom)) (Over.homMk g ⋯)
have refine_2 : S.arrows (Y := Over.mk (F.map (g ≫ U.hom))) (Over.homMk (F.map g) sorry)
Tactic: dsimp [Presieve.functorPullback]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ≫ U.hom))) (Over.homMk (F.map g) ⋯)
have h : F.map (g ≫ U.hom) = F.map g ≫ (Functor.obj (Over.post F) U).hom
Tactic: convert! (Sieve.overEquiv_iff _ _).mp hg