awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
⊢ (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f ↔
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f
have h : (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f →
  ofArrows
    (fun (i : (i : ι) × j (g i) sorry) ↦
      W (g (i.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (i.snd (β := fun (i : ι) ↦ j (g i) sorry)))
    (fun (ij : (i : ι) × j (g i) sorry) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ j (g i) sorry)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry)))
    f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
j : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type u_2
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → j f H → C
k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y
Y : C
f : Y ⟶ X
h :
  (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f →
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f
⊢ (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f ↔
    ofArrows
      (fun (i : (i : ι) × j (g i) ⋯) ↦
        W (g (i.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (i.snd (β := fun (i : ι) ↦ j (g i) ⋯)))
      (fun (ij : (i : ι) × j (g i) ⋯) ↦
        k (g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ j (g i) ⋯)) ≫
          g (ij.fst (β := fun (i : ι) ↦ j (g i) ⋯)))
      f
have h₁ : ofArrows
    (fun (i : (i : ι) × j (g i) sorry) ↦
      W (g (i.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (i.snd (β := fun (i : ι) ↦ j (g i) sorry)))
    (fun (ij : (i : ι) × j (g i) sorry) ↦
      k (g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ j (g i) sorry)) ≫
        g (ij.fst (β := fun (i : ι) ↦ j (g i) sorry)))
    f →
  (ofArrows Z g).bind (fun (x : C) (f : x ⟶ X) (H : ofArrows Z g f) ↦ ofArrows (W f H) (k f H)) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
hg : ofArrows Y f g
⊢ ∃ (i : ι) (h : Y i = Z), g = eqToHom ⋯ ≫ f i
have obtain : ∀ ⦃Y_1 : C⦄ (i : ι), ∃ (i_1 : ι) (h : Y i_1 = Y i), f i = eqToHom sorry ≫ f i_1
Tactic: obtain ⟨i⟩ := hg
Cleared hypotheses: Z, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
ι : Type (max 0 u₁ v₁) := { x : (Z : C) × (Z ⟶ X) // R (x.snd (β := fun (Z : C) ↦ Z ⟶ X)) }
⊢ ∃ (ι : Type (max u₁ v₁)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X), R = ofArrows Y f
have h : R =
  ofArrows (fun (x : ι) ↦ (↑x : (Z : C) × (Z ⟶ X)).fst (β := fun (Z : C) ↦ Z ⟶ X)) fun (x : ι) ↦
    (↑x : (Z : C) × (Z ⟶ X)).snd (β := fun (Z : C) ↦ Z ⟶ X)
Tactic: use ι, fun x ↦ x.1.1, fun x ↦ x.1.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
⊢ (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) =
    R
have refine_1 : (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
    f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) ≤
  R
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Presieve.{v₁, u₁} S
refine_1 :
  (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) ≤
    R
⊢ (ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
      f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom) =
    R
have refine_2 : R ≤
  ofArrows (fun (f : R.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).left) fun (f : R.category) ↦
    f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R f.hom).hom
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
ha : Function.Surjective a
⊢ (ofArrows (Y ∘ a) fun (i : σ) ↦ f (a i)) = ofArrows Y f
have refine : ofArrows Y f ≤ ofArrows (Y ∘ a) fun (i : σ) ↦ f (a i)
Tactic: refine le_antisymm (ofArrows_comp_le f a) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
a : σ → ι
ha : Function.Surjective a
Y : C
i : ι
⊢ ofArrows (Y_1 ∘ a) (fun (i : σ) ↦ f (a i)) (f i)
have obtain : ∀ (j : σ), ofArrows (Y_1 ∘ a) fun (i : σ) ↦ f (a i) (Y := Y_1 (a j)) (f (a j))
Tactic: obtain ⟨j, rfl⟩ := ha i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = singleton (Y := Y default) (f default)
have refine : ofArrows Y f ≤ singleton (Y := Y default) (f default)
Tactic: refine le_antisymm ?_ fun Y _ ⟨⟩ ↦ ⟨default⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f ≤ singleton (Y := Y default) (f default)
have rw : ∀ (i : ι), singleton (Y := Y default) (f default) (f i)
Tactic: rw [ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
⊢ singleton (Y := Y default) (f default) (f i)
have obtain : singleton (Y := Y default) (f default) (Y := Y default) (f default)
Tactic: obtain rfl : i = default := Subsingleton.elim _ _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ (ofArrows (fun (x : PUnit.{u_1 + 1}) ↦ Y) fun (x : PUnit.{u_1 + 1}) ↦ f) = singleton f
have rw : singleton f = singleton f
Tactic: rw [ofArrows_of_unique]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst_1 : IsEmpty ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ofArrows Y f = ⊥
have rw : ∀ (i : ι), ⊥ (f i)
Tactic: rw [eq_bot_iff, ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
σ : ι → Type u_2
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
⊢ (bindOfArrows X f fun (i : ι) ↦ ofArrows (Y i) (g i)) =
    ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (p : (i : ι) × σ i) ↦
      g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i))
have refine : (bindOfArrows X f fun (i : ι) ↦ ofArrows (Y i) (g i)) ≤
  ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
    fun (p : (i : ι) × σ i) ↦
    g (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)) ≫ f (p.fst (β := fun (i : ι) ↦ σ i))
Tactic: refine le_antisymm ?_ (fun _ _ ⟨p⟩ ↦ ⟨p.1, _, ⟨p.2⟩⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z : C
f_1 : Y_1 ⟶ X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₂, u₁, u₂} C D
S : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h : functorPushforward F S f
⊢ FunctorPushforwardStructure F S f
have choose : (Z : C) → (f' : Z ⟶ X) → (g : Y ⟶ F.obj Z) → (h₁ : S f') → (h : f = g ≫ F.map f') → FunctorPushforwardStructure F S f
Tactic: choose Z f' g h₁ h using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
have h : ∀ (x : E),
  Eq (α := (x ⟶ (F ⋙ G).obj X) → Prop) (functorPushforward (F ⋙ G) R) (functorPushforward G (functorPushforward F R))
Tactic: funext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
x : E
⊢ Eq (α := (x ⟶ (F ⋙ G).obj X) → Prop) (functorPushforward (F ⋙ G) R) (functorPushforward G (functorPushforward F R))
have h : ∀ (f : x ⟶ (F ⋙ G).obj X), functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f
have h : functorPushforward (F ⋙ G) R f → functorPushforward G (functorPushforward F R) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
x : E
f : x ⟶ (F ⋙ G).obj X
h : functorPushforward (F ⋙ G) R f → functorPushforward G (functorPushforward F R) f
⊢ functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f
have h₁ : functorPushforward G (functorPushforward F R) f → functorPushforward (F ⋙ G) R f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
⊢ map F R f ↔ ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
have refine : (∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f) →
  ∀ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X) (hg : R g) (heq : F.map g = eqToHom h ≫ f), map F R f
Tactic: refine ⟨fun (.of (u := u) hu) ↦ ⟨_, rfl, u, hu, by simp⟩, fun ⟨Z, h, g, hg, heq⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h_1 : ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
Z : C
h : F.obj Z = Y
g : Z ⟶ X
hg : R g
heq : F.map g = eqToHom h ≫ f
⊢ map F R f
have subst : ∀ {f : F.obj Z ⟶ F.obj X},
  (∃ (Z_1 : C) (h : F.obj Z_1 = F.obj Z) (g : Z_1 ⟶ X), R g ∧ F.map g = eqToHom h ≫ f) →
    ∀ (heq : F.map g = eqToHom sorry ≫ f), map F R f
Tactic: subst h
Cleared hypotheses: Y, f, h_1, h, heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
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
R : Presieve.{v₁, u₁} X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
h : ∃ (Z_1 : C) (h : F.obj Z_1 = F.obj Z) (g : Z_1 ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = eqToHom ⋯ ≫ f
⊢ map F R f
have heq₁ : F.map g = f
Tactic: rw [eqToHom_refl, Category.id_comp] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ map F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
have refine : ∀ (Z : D) (g : Z ⟶ F.obj X) (hg : map F (ofArrows Y f) g),
  ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) g
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) fun _ _ ⟨i⟩ ↦ map_map ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : D
g : Z ⟶ F.obj X
hg : map F (ofArrows Y f) g
⊢ ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) g
have obtain : ∀ ⦃Y_1 : D⦄ {Y_2 : C} {u : Y_2 ⟶ X} (hu : ofArrows Y f u),
  ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) (F.map u)
Tactic: obtain ⟨hu⟩ := hg
Cleared hypotheses: Z, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : D
Y_2 : C
u : Y_2 ⟶ X
hu : ofArrows Y_1 f u
⊢ ofArrows (fun (i : ι) ↦ F.obj (Y_1 i)) (fun (i : ι) ↦ F.map (f i)) (F.map u)
have obtain : ∀ (i : ι) (hu : ofArrows Y_1 f (eqToHom sorry ≫ f i)),
  ofArrows (fun (i : ι) ↦ F.obj (Y_1 i)) (fun (i : ι) ↦ F.map (f i)) (F.map (eqToHom sorry ≫ f i))
Tactic: obtain ⟨i, rfl, rfl⟩ := Presieve.ofArrows_surj _ _ hu
Cleared hypotheses: Y_2, u, hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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 : X ⟶ Y
⊢ map F (singleton f) = singleton (F.map f)
have rw : map F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) = singleton (F.map f)
Tactic: rw [← ofArrows_pUnit.{_, _, 0}, map_ofArrows, ofArrows_pUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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 : X ⟶ Y
rw : map F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) = singleton (F.map f)
⊢ map F (singleton f) = singleton (F.map f)
have rw₁ : (ofArrows (fun (i : PUnit.{1}) ↦ F.obj X) fun (i : PUnit.{1}) ↦ F.map f) = singleton (F.map f)
Tactic: rw [← ofArrows_pUnit.{_, _, 0}, map_ofArrows, ofArrows_pUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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 : X ⟶ Y
rw : map F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) = singleton (F.map f)
rw₁ : (ofArrows (fun (i : PUnit.{1}) ↦ F.obj X) fun (i : PUnit.{1}) ↦ F.map f) = singleton (F.map f)
⊢ map F (singleton f) = singleton (F.map f)
have rw₂ : singleton (F.map f) = singleton (F.map f)
Tactic: rw [← ofArrows_pUnit.{_, _, 0}, map_ofArrows, ofArrows_pUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
⊢ (singleton u).uncurry = {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
have h : ∀ (Z : C) (v : Z ⟶ X),
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
Tactic: ext ⟨Z, v⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry →
  Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry →
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h₁ : Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) →
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
have h₁ : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) =
    Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ∧
  HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
Tactic: rw [Set.mem_singleton_iff, Sigma.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ∧
    HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
have h₁ : ∀ (u : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
  (h :
    HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (β :=
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
        X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
              (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
          X)),
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
Tactic: obtain ⟨rfl, h⟩ := h
Cleared hypotheses: Y, u, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
u : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X
h :
  HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (β :=
    Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
      X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
        X)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
have h₁ : Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
  (uncurry
      (singleton (Y := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))) :
    Set ((Y : C) × (Y ⟶ X)))
  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
Tactic: subst h
Cleared hypotheses: u, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
⊢ (pullbackArrows b s).uncurry =
    (fun (f : (Y : C) × (Y ⟶ X)) ↦
        Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
          (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)) ''
      s.uncurry
have h : ∀ (Z : C) (v : Z ⟶ B),
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ B)))
      ((fun (f : (Y : C) × (Y ⟶ X)) ↦
          Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
            (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)) ''
        s.uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v)
Tactic: ext ⟨Z, v⟩