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
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
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)
have h : 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: constructor
-- 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
Z : C
v : Z ⟶ B
h :
  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)
⊢ 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)
have h₁ : 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) →
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
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
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
h :
  Eq (α := (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) :
          (Y : C) × (Y ⟶ B)))
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u))
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry
have h₁ : Sigma.fst (β := fun (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) :
            (Y : C) × (Y ⟶ B)))
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) =
    Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ∧
  HEq.{v₁ + 1} (α :=
    Sigma.fst (β := fun (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) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
      B)
    (Sigma.snd (β := fun (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) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) :
      Sigma.fst (β := fun (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) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
        B)
    (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)
Tactic: rw [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 : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
⊢ (s.bind t).uncurry =
    ⋃ (i : (Y : C) × (Y ⟶ X)),
      ⋃ (h : i ∈ s.uncurry),
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
          (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry
have h : ∀ (Z : C) (v : Z ⟶ X),
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (⋃ (i : (Y : C) × (Y ⟶ X)),
        ⋃ (h : i ∈ s.uncurry),
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
              fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
            (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry)
      (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 : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (⋃ (i : (Y : C) × (Y ⟶ X)),
        ⋃ (h : i ∈ s.uncurry),
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
              fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
            (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
  ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
    ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) sorry).uncurry,
      Eq (α := (Y : C) × (Y ⟶ X))
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
Tactic: simp only [Set.mem_iUnion, Set.mem_image]
-- 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
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry →
  ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
    ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) sorry).uncurry,
      Eq (α := (Y : C) × (Y ⟶ X))
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
        (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 : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry →
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h₁ : (∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
    ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) sorry).uncurry,
      Eq (α := (Y : C) × (Y ⟶ X))
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) →
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry
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
⊢ (ofArrows Y f).uncurry = Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i)
have h : ∀ (Z : C) (v : Z ⟶ X),
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i))
      (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 : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i))
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
have h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔ ∃ (y : ι), Y y = Z ∧ f y ≍ v
Tactic: simp only [Set.mem_range, Sigma.mk.injEq]
-- 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
v : Z ⟶ X
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔ ∃ (y : ι), Y y = Z ∧ f y ≍ v
have h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry → ∃ (y : ι), Y y = Z ∧ f y ≍ v
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
v : Z ⟶ X
h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry → ∃ (y : ι), Y y = Z ∧ f y ≍ v
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔ ∃ (y : ι), Y y = Z ∧ f y ≍ v
have h₁ : (∃ (y : ι), Y y = Z ∧ f y ≍ v) → Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry
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
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) v ∈ (ofArrows Y f).uncurry
have h₁ : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i) ∈ (ofArrows Y f).uncurry
Tactic: rw [← eq_of_heq h]
-- 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
⊢ ofArrows X f =
    ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx ⋯))
      fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx ⋯)
have refine : ∀ (Z : C) (g : Z ⟶ S) (hg : ofArrows X f g),
  ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx sorry))
    (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx sorry)) g
Tactic: refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ .mk _
-- 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 Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
𝒮 : Set (Sieve.{v₁, u₁} X)
x x_1 : C
f : x ⟶ X
hf : ∃ S ∈ 𝒮, S.arrows f
x_2 : x_1 ⟶ x
⊢ ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)
have obtain : ∀ (S : Sieve.{v₁, u₁} X) (hS : S ∈ 𝒮) (hf : S.arrows f), ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)
Tactic: obtain ⟨S, hS, hf⟩ := hf
Cleared hypotheses: hf
-- 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
s : Presieve.{v₁, u₁} X
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s
have refine_1 : ∀ (Z : D) (u : Z ⟶ F.obj X), (generate (Presieve.map F s)).arrows u → Presieve.functorPushforward F s u
Tactic: refine funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩
-- 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
s : Presieve.{v₁, u₁} X
refine_1 : ∀ (Z : D) (u : Z ⟶ F.obj X), (generate (Presieve.map F s)).arrows u → Presieve.functorPushforward F s u
⊢ (generate (Presieve.map F s)).arrows = Presieve.functorPushforward F s
have refine_2 : ∀ (Z : D) (u : Z ⟶ F.obj X), Presieve.functorPushforward F s u → (generate (Presieve.map F s)).arrows u
Tactic: refine funext fun Z ↦ funext fun u ↦ propext ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
R : Presieve.{v₁, u₁} X
f : Y ⟶ X
inst_1 : IsSplitEpi f
hf : R f
⊢ generate R = ⊤
have rw : (generate R).arrows (𝟙 X)
Tactic: rw [← id_mem_iff_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f
have refine : ∀ (H : S.arrows (i ≫ f)), S.arrows f
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst_1 : IsIso i
S : Sieve.{v₁, u₁} Z
H : S.arrows (i ≫ f)
⊢ S.arrows f
have h : f = inv i ≫ i ≫ f
Tactic: convert! S.downward_closed H (inv i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g ↔ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
have mp : (ofArrows Y f).arrows g → ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
mp : (ofArrows Y f).arrows g → ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
⊢ (ofArrows Y f).arrows g ↔ ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
have mpr : (∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i) → (ofArrows Y f).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ ∃ (i : I) (h : W ⟶ Y i), g = h ≫ f i
have obtain : ∀ ⦃Y_1 : C⦄ (i : I) (h : W ⟶ Y i), ∃ (i_1 : I) (h_1 : W ⟶ Y i_1), h ≫ f i = h_1 ≫ f i_1
Tactic: obtain ⟨_, h, _, ⟨i⟩, rfl⟩ := hg
Cleared hypotheses: g, hg
-- 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) =
    generate 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) ≤
  generate 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) ≤
    generate 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) =
    generate R
have refine_2 : generate 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
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) ≤
    generate R
have refine_1 : (Presieve.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) ≤
  (generate R).arrows
Tactic: rw [Sieve.generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Sieve.{v₁, u₁} S
⊢ (ofArrows (fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).left)
      fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).hom) =
    R
have rw : generate R.arrows = R
Tactic: rw [ofArrows_category', generate_sieve]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
S : C
R : Sieve.{v₁, u₁} S
rw : generate R.arrows = R
⊢ (ofArrows (fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).left)
      fun (f : R.arrows.category) ↦ f.obj (P := fun (f : Over.{v₁, u₁} S) ↦ R.arrows f.hom).hom) =
    R
have rw₁ : R = R
Tactic: rw [ofArrows_category', generate_sieve]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : (ofArrows Y f).arrows g
⊢ arrows (ofObjects Y X) g
have hg₁ : ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
Tactic: rw [mem_ofArrows_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
hg : ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
⊢ arrows (ofObjects Y X) g
have obtain : ∀ (i : I) (a : W ⟶ Y i), arrows (ofObjects Y X) (a ≫ f i)
Tactic: obtain ⟨i, a, rfl⟩ := hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsTerminal.{v₁, u₁} X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
⊢ ofArrows Y f = ofObjects Y X
have refine : ∀ (W : C) (g : W ⟶ X), arrows (ofObjects Y X) g → (ofArrows Y f).arrows g
Tactic: refine le_antisymm (ofArrows_le_ofObjects Y f) (fun W g => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsTerminal.{v₁, u₁} X
I : Type u_1
Y : I → C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ arrows (ofObjects Y X) g → (ofArrows Y f).arrows g
have rw : (∃ (i : I), Nonempty.{v₁ + 1} (W ⟶ Y i)) → ∃ (i : I) (a : W ⟶ Y i), g = a ≫ f i
Tactic: rw [mem_ofArrows_iff, mem_ofObjects_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
I' : Type u_2
X' : I' → C
Y : C
h : Set.range X ⊆ Set.range X'
Z : C
f : Z ⟶ Y
i : I
g : Z ⟶ X i
⊢ arrows (ofObjects X' Y) f
have obtain : ∀ (i' : I') (h : X' i' = X i), arrows (ofObjects X' Y) f
Tactic: obtain ⟨i', h⟩ := h ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ pullback e.hom (ofArrows Z f) = ofArrows Z fun (i : I) ↦ f i ≫ e.inv
have rw : ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) f_1
Tactic: rw [Sieve.ext_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a
have mp : (pullback e.hom (ofArrows Z f)).arrows a → arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
mp : (pullback e.hom (ofArrows Z f)).arrows a → arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a
⊢ (pullback e.hom (ofArrows Z f)).arrows a ↔ arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a
have mpr : arrows (ofArrows Z fun (i : I) ↦ f i ≫ e.inv) a → (pullback e.hom (ofArrows Z f)).arrows a
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
⊢ S.arrows f ↔ pullback f S = ⊤
have rw : S.arrows f ↔ (pullback f S).arrows (𝟙 Y)
Tactic: rw [← id_mem_iff_eq_top, pullback_apply, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
rw : S.arrows f ↔ (pullback f S).arrows (𝟙 Y)
⊢ S.arrows f ↔ pullback f S = ⊤
have rw₁ : S.arrows f ↔ S.arrows (𝟙 Y ≫ f)
Tactic: rw [← id_mem_iff_eq_top, pullback_apply, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Sieve.{v₁, u₁} X
f : Y ⟶ X
rw : S.arrows f ↔ (pullback f S).arrows (𝟙 Y)
rw₁ : S.arrows f ↔ S.arrows (𝟙 Y ≫ f)
⊢ S.arrows f ↔ pullback f S = ⊤
have rw₂ : S.arrows f ↔ S.arrows f
Tactic: rw [← id_mem_iff_eq_top, pullback_apply, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
⊢ Eq (α := Sieve.{v₁, u₁} X) (ofObjects Y X) ⊤
have h : ∀ ⦃Z : C⦄ (h : Z ⟶ X), arrows (ofObjects Y X) h ↔ arrows ⊤ h
Tactic: ext Z h