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
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
have refine_1 : Presieve.functorPushforward F R.arrows f →
  ∀ (Z : C) (g : Z ⟶ X) (h : F.obj Y ⟶ F.obj Z) (hg : R.arrows g) (hcomp : f = h ≫ F.map g),
    ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
Tactic: refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, 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
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
refine_1 :
  Presieve.functorPushforward F R.arrows f →
    ∀ (Z : C) (g : Z ⟶ X) (h : F.obj Y ⟶ F.obj Z) (hg : R.arrows g) (hcomp : f = h ≫ F.map g),
      ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
have refine_2 : (∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g) →
  ∀ (g : Y ⟶ X) (hcomp : F.map g = f) (hg : R.arrows g), Presieve.functorPushforward F R.arrows f
Tactic: refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, 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
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
⊢ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
have refine_1 : ∀ (h' : Y ⟶ Z) (hh' : F.map h' = h), ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
Tactic: obtain ⟨h', hh'⟩ := F.map_surjective 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
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
have h₁ : F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)
Tactic: use h' ≫ g
-- 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
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h_1 : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)
have h₁ : R.arrows (h' ≫ g)
Tactic: simp only [Functor.map_comp, hh', hcomp, true_and]
-- 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
inst_2 : F.Full
X Y : C
R : Sieve.{v₁, u₁} X
f : F.obj Y ⟶ F.obj X
h : ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f
have right : f = 𝟙 (F.obj Y) ≫ F.map g
Tactic: use Y, 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
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f
have rw : (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f
Tactic: rw [Sieve.mem_functorPushforward_iff_of_full]
-- 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
inst_2 : F.Full
inst_3 : F.Faithful
X Y : C
R : Sieve.{v₁, u₁} X
f : Y ⟶ X
⊢ (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f
have refine : (∃ (g : Y ⟶ X), F.map g = F.map f ∧ R.arrows g) →
  ∀ (g : Y ⟶ X) (hcomp : F.map g = F.map f) (hg : R.arrows g), R.arrows f
Tactic: refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, 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 Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
Z_1 : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : Z_1 ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
⊢ f = g
have w : ∀ (Y : Cᵒᵖ) (y : Z_1.obj Y), (hom (FC := TypeCat.Fun) (f.app Y)).toFun y = (hom (FC := TypeCat.Fun) (g.app Y)).toFun y
Tactic: ext Y y
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : R ⟶ Functor.obj yoneda X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ ∃ (t_1 : R.obj (Opposite.op Z)),
    Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
          t_1 :
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      (g ≫
          (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
              (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
                (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
            t :
        Z ⟶ X)
have refine : Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
  ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
        (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
          (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (R.map g.op) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) → (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z)))
          t :
        (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) :
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
  (g ≫
      (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
          (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
        t :
    Z ⟶ X)
Tactic: refine ⟨R.map g.op t, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
⊢ sieveOfSubfunctor S.functorInclusion = S
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (sieveOfSubfunctor S.functorInclusion).arrows f ↔ S.arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
⊢ (∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f) ↔
    S.arrows f
have h : (∃ (t : S.functor.obj (Opposite.op Y)),
    (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
          (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
        t =
      f) →
  S.arrows f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
h :
  (∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f) →
    S.arrows f
⊢ (∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f) ↔
    S.arrows f
have h₁ : S.arrows f →
  ∃ (t : S.functor.obj (Opposite.op Y)),
    (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
          (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
        t =
      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 Y Z : C
f : Y ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
⊢ x = x_1
have w : ∀ (Y : Cᵒᵖ) (y : Z_1.obj Y), (hom (FC := TypeCat.Fun) (x.app Y)).toFun y = (hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y
Tactic: ext Y y
-- 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_1 Z : C
f : Y_1 ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
Y : Cᵒᵖ
y : Z_1.obj Y
⊢ (hom (FC := TypeCat.Fun) (x.app Y)).toFun y = (hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y
have w : (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x.app Y)).toFun y)) : Opposite.unop Y ⟶ X) =
  (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y)) : Opposite.unop Y ⟶ X)
Tactic: refine ULift.ext _ _ (Subtype.ext_iff.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 : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
⊢ (∃ (t : R.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
              (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
          t =
        { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }) →
    ∀ (g : Z ⟶ Y),
      ∃ (t : R.obj (Opposite.op Z)),
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
                (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
            t =
          { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
have this : ∀ (t : R.obj (Opposite.op Y))
  (ht :
    (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
            (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
        t =
      { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) })
  (g : Z ⟶ Y),
  ∃ (t : R.obj (Opposite.op Z)),
    (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
        t =
      { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
Tactic: ⟨t, ht⟩
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
t : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))
ht :
  (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
      t =
    { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }
g : Z ⟶ Y
⊢ ∃ (t : R.obj (Opposite.op Z)),
    (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
        t =
      { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
have refine : (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
      (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
        (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
    ((hom (FC := TypeCat.Fun) (R.map g.op) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
          (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z)))
      t) =
  { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
Tactic: refine ⟨R.map g.op t, ?_⟩
-- 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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ = pullback g (ofArrows X f)
have refine_1 : ofArrows P p₁ ≤ pullback g (ofArrows X f)
Tactic: refine le_antisymm ?_ ?_
-- 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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
refine_1 : ofArrows P p₁ ≤ pullback g (ofArrows X f)
⊢ ofArrows P p₁ = pullback g (ofArrows X f)
have refine_2 : pullback g (ofArrows X f) ≤ ofArrows P p₁
Tactic: refine le_antisymm ?_ ?_
-- 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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ ≤ pullback g (ofArrows X f)
have refine_1 : Presieve.ofArrows P p₁ ≤ (pullback g (ofArrows X f)).arrows
Tactic: rw [Sieve.ofArrows, Sieve.generate_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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ (pullback g (ofArrows X f)).arrows (p₁ i)
have right : p₂ i ≫ f i = p₁ i ≫ g
Tactic: use X i, p₂ i, f i, ⟨i⟩
-- 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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
W : C
u : W ⟶ Y_1
Y : C
i : ι
v : W ⟶ X i
heq : v ≫ f i = u ≫ g
⊢ (ofArrows P p₁).arrows u
have right : sorry.lift u v sorry ≫ p₁ i = u
Tactic: use P i, (h i).lift u v heq.symm, p₁ i, ⟨i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve.{v₁, u₁} (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (v ≫ v')
have rw : (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))
Tactic: rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
have rcases : ∀ (U : Opens T) (g : U ⟶ X) (hg : S.arrows g) (hU : y ∈ U),
  ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
Tactic: rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), (Sieve.pullback f S).arrows f_1 ∧ y ∈ U
have refine : (Sieve.pullback f S).arrows (Y := U ⊓ Y) (homOfLE sorry)
Tactic: refine ⟨U ⊓ Y, homOfLE inf_le_right, ?_, hU, hy⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
have rcases : ∀ (U : Opens T) (f : U ⟶ X) (hf : S.arrows f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
Tactic: rcases hS x hx with ⟨U, f, hf, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Sieve X
hS : Membership.mem (γ := Set (Sieve X)) {S : Sieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S.arrows f ∧ x ∈ U} S
R : Sieve X
hR :
  ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve Y)) {S : Sieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), S.arrows f ∧ x ∈ U}
        (Sieve.pullback f R)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
have rcases : ∀ (V : Opens T) (g : V ⟶ U) (hg : (Sieve.pullback f R).arrows g) (hV : x ∈ V),
  ∃ (U : Opens T) (f : U ⟶ X), R.arrows f ∧ x ∈ U
Tactic: rcases hR hf _ hU with ⟨V, g, hg, hV⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U
have rcases : ∀ (U : Opens T) (g : U ⟶ X) (hg : S g) (hU : x ∈ U),
  ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U
Tactic: rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ ∃ (U : Opens T) (f_1 : U ⟶ Y), Presieve.pullbackArrows f S f_1 ∧ x ∈ U
have refine : x ∈ pullback g f
Tactic: refine ⟨_, _, Presieve.pullbackArrows.mk _ _ hg, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (hypothesis)
Goal:
T : Type u
inst : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ x ∈ pullback g f
have this : U ⊓ Y ≤ pullback g f
Tactic: have : U ⊓ Y ≤ pullback g f :=
      leOfHom (pullback.lift (homOfLE inf_le_left) (homOfLE inf_le_right) rfl)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
have rcases : ∀ (U : Opens T) (f : U ⟶ X) (hf : S f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
Tactic: rcases hS x hx with ⟨U, f, hf, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : Membership.mem (γ := Set (Presieve X)) {R : Presieve X | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U} S
hTi :
  ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve Y)) {R : Presieve Y | ∀ x ∈ Y, ∃ (U : Opens T) (f : U ⟶ Y), R f ∧ x ∈ U} (Ti f H)
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
⊢ ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
have rcases : ∀ (V : Opens T) (g : V ⟶ U) (hg : Ti f hf g) (hV : x ∈ V), ∃ (U : Opens T) (f : U ⟶ X), S.bind Ti f ∧ x ∈ U
Tactic: rcases hTi f hf x hU with ⟨V, g, hg, hV⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
⊢ Eq (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)
have a : LE.le (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
a : LE.le (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)
⊢ Eq (α := Pretopology (Opens T)) (GrothendieckTopology.toPretopology (grothendieckTopology T)) (pretopology T)
have a₁ : LE.le (α := Pretopology (Opens T)) (pretopology T) (GrothendieckTopology.toPretopology (grothendieckTopology T))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR :
  R ∈ Precoverage.coverings (Pretopology.toPrecoverage (GrothendieckTopology.toPretopology (grothendieckTopology T))) X
x : T
hx : x ∈ X
⊢ ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U
have a : ∀ (U : Opens T) (f : U ⟶ X) (hU : x ∈ U) (V : Opens T) (g₁ : U ⟶ V) (g₂ : V ⟶ X) (hg₂ : R g₂),
  g₁ ≫ g₂ = f → ∃ (U : Opens T) (f : U ⟶ X), R f ∧ x ∈ U
Tactic: rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ Precoverage.coverings (Pretopology.toPrecoverage (pretopology T)) X
x : T
hx : x ∈ X
⊢ ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U
have a : ∀ (U : Opens T) (f : U ⟶ X) (hf : R f) (hU : x ∈ U), ∃ (U : Opens T) (f : U ⟶ X), (Sieve.generate R).arrows f ∧ x ∈ U
Tactic: rcases hR x hx with ⟨U, f, hf, hU⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Spaces (goal)
Goal:
T : Type u
inst : TopologicalSpace T
⊢ Eq (α := GrothendieckTopology (Opens T)) (Pretopology.toGrothendieck (pretopology T)) (grothendieckTopology T)
have rw : Eq (α := GrothendieckTopology (Opens T))
  (Pretopology.toGrothendieck (GrothendieckTopology.toPretopology (grothendieckTopology T))) (grothendieckTopology T)
Tactic: rw [← toPretopology_grothendieckTopology]