awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} (S.bind Ti)
have h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
  (Sieve.generate S).arrows f → Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.transitive hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Y
have h : Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: rw [Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ (J : (a : C) → Set (Sieve a)) Y
have h : Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Z
Tactic: apply J.pullback_stable g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
J : GrothendieckTopology.{v, u} C
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS :
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {R : Presieve.{v, u} X | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) X} S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {R : Presieve.{v, u} Y | Sieve.generate R ∈ (J : (a : C) → Set (Sieve a)) Y} (Ti f H)
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ (J : (a : C) → Set (Sieve a)) Z
have apply : Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (S.bind Ti))
Tactic: apply J.superset_covering _ (hTi _ hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPretopology
have mp : K.toGrothendieck ≤ J → K ≤ J.toPretopology
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
mp : K.toGrothendieck ≤ J → K ≤ J.toPretopology
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toPretopology
have mpr : K ≤ J.toPretopology → K.toGrothendieck ≤ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
K : Pretopology.{v, u} C
J : GrothendieckTopology.{v, u} C
h : K ≤ J.toPretopology
X : C
S : Sieve.{v, u} X
R : Presieve.{v, u} X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have apply : Sieve.generate R ≤ S
Tactic: apply J.superset_covering _ (h _ hR)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y))
    {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f}
    (pullbackArrows f (Presieve.singleton g))
have refine_1 : IsIso (X := pullback g f) (pullback.snd g f)
Tactic: refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 : IsIso (X := pullback g f) (pullback.snd g f)
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y))
    {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f}
    (pullbackArrows f (Presieve.singleton g))
have refine_2 : pullbackArrows f (Presieve.singleton g) = Presieve.singleton (Y := pullback g f) (pullback.snd g f)
Tactic: refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso (X := pullback g f) (pullback.snd g f)
have refine_1 : pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) sorry = 𝟙 (pullback g f)
Tactic: refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ = 𝟙 (pullback g f)
have refine_1 : CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) sorry) (pullback.fst g f) =
  𝟙 (pullback g f) ≫ pullback.fst g f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
refine_1 :
  CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.fst g f) =
    𝟙 (pullback g f) ≫ pullback.fst g f
⊢ pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ = 𝟙 (pullback g f)
have refine_1₁ : CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) sorry) (pullback.snd g f) =
  𝟙 (pullback g f) ≫ pullback.snd g f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ CategoryStruct.comp (Y := pullback g f) (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) (pullback.fst g f) =
    𝟙 (pullback g f) ≫ pullback.fst g f
have refine_1 : pullback.fst g f ≫ g ≫ inv g = 𝟙 (pullback g f) ≫ pullback.fst g f
Tactic: rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)
have rcases : ∀ (Y : C) (f : Y ⟶ Z) (i : IsIso f) (hTi : Ti g sorry = Presieve.singleton f),
  Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)
Tactic: rcases hS g (singleton_self g) with ⟨Y, f, i, hTi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)
have refine_1 : IsIso (f ≫ g)
Tactic: refine ⟨_, f ≫ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
refine_1 : IsIso (f ≫ g)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X))
    {S : Presieve.{v, u} X | ∃ (Y : C) (f : Y ⟶ X) (_ : IsIso f), S = Presieve.singleton f}
    ((Presieve.singleton g).bind Ti)
have refine_2 : (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
Tactic: refine ⟨_, f ≫ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ (Presieve.singleton g).bind Ti = Presieve.singleton (f ≫ g)
have refine_2 : ∀ (x : C), Eq (α := (x ⟶ X) → Prop) ((Presieve.singleton g).bind Ti) (Presieve.singleton (f ≫ g))
Tactic: apply funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
⊢ Eq (α := (W ⟶ X) → Prop) ((Presieve.singleton g).bind Ti) (Presieve.singleton (f ≫ g))
have refine_2 : ∀ (K : W ⟶ X), (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K
Tactic: ext K
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
⊢ (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K
have refine_2 : (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_1 : C) (f : Y_1 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W : C
K : W ⟶ X
refine_2 : (Presieve.singleton g).bind Ti K → Presieve.singleton (f ≫ g) K
⊢ (Presieve.singleton g).bind Ti K ↔ Presieve.singleton (f ≫ g) K
have refine_2₁ : Presieve.singleton (f ≫ g) K → (Presieve.singleton g).bind Ti K
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Ti g ⋯ h
⊢ Presieve.singleton (f ≫ g) (h ≫ g)
have hh₁ : Presieve.singleton f h
Tactic: rw [hTi] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
W Y : C
h : W ⟶ Z
hh : Presieve.singleton f h
⊢ Presieve.singleton (f ≫ g) (h ≫ g)
have refine_2 : Presieve.singleton (f ≫ g) (f ≫ g)
Tactic: cases hh
Cleared hypotheses: W, h, hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ (Presieve.singleton g).bind Ti (f ≫ g)
have refine_2 : Ti g sorry f
Tactic: refine bind_comp g singleton.mk ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
X Z : C
g : Z ⟶ X
i_1 : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve.{v, u} Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f),
    Membership.mem (γ := Set (Presieve.{v, u} Y))
      {S : Presieve.{v, u} Y | ∃ (Y_2 : C) (f : Y_2 ⟶ Y) (_ : IsIso f), S = Presieve.singleton f} (Ti f H)
Y_1 : C
f : Y_1 ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Ti g ⋯ f
have refine_2 : Presieve.singleton f f
Tactic: rw [hTi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
h : IsIso f
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X)
    (Presieve.singleton f)
have simp : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Presieve.singleton f ∈ i.coverings X
Tactic: simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists,
        Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X Y : C
f : Y ⟶ X
S : Presieve.{v, u} X
hS : Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X) S
⊢ Membership.mem (γ := Set (Presieve.{v, u} Y)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) Y)
    (pullbackArrows f S)
have simp : ∀ (hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X) (i : Pretopology.{v, u} C) (i_1 : i ∈ T),
  pullbackArrows f S ∈ i.coverings Y
Tactic: simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (Pretopology.{v, u} C)
X : C
S : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve.{v, u} Y
hS : Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X) S
hTi :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f),
    Membership.mem (γ := Set (Presieve.{v, u} Y)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) Y)
      (Ti f H)
⊢ Membership.mem (γ := Set (Presieve.{v, u} X)) (sInf ((fun (J : Pretopology.{v, u} C) ↦ J.coverings) '' T) X)
    (S.bind Ti)
have simp : ∀ (hS : ∀ (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S ∈ i.coverings X)
  (hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f) (i : Pretopology.{v, u} C) (i_1 : i ∈ T), Ti f H ∈ i.coverings Y)
  (i : Pretopology.{v, u} C) (i_1 : i ∈ T), S.bind Ti ∈ i.coverings X
Tactic: simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS hTi ⊢
Cleared hypotheses: hS, hTi
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
T : Set (GrothendieckTopology.{v, u} C)
⊢ Eq (α := Pretopology.{v, u} C) (sInf T).toPretopology (sInf (GrothendieckTopology.toPretopology '' T))
have coverings : ∀ (X : C) (S : Presieve.{v, u} X),
  S ∈ (toPrecoverage (sInf T).toPretopology).coverings X ↔
    S ∈ (toPrecoverage (sInf (GrothendieckTopology.toPretopology '' T))).coverings X
Tactic: ext X S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
R : Presieve.{v, u} X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → R f → Presieve.{v, u} Y
hR : R ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : R f), Ti f H ∈ J.coverings Y
⊢ R.bind Ti ∈ J.coverings X
have obtain : ∀ (ι : Type (max u v)) (Z : ι → C) (g : (i : ι) → Z i ⟶ X)
  (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y) (hR : ofArrows Z g ∈ J.coverings X)
  (hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y), (ofArrows Z g).bind Ti ∈ J.coverings X
Tactic: obtain ⟨ι, Z, g, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R, Ti, hR, hTi
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
⊢ (ofArrows Z g).bind Ti ∈ J.coverings X
have choose : ∀ (κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v))
  (W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C)
  (p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y)
  (hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)),
  (ofArrows Z g).bind Ti ∈ J.coverings X
Tactic: choose κ W p hp using fun ⦃Y⦄ (f : Y ⟶ X) hf ↦ (Ti f hf).exists_eq_ofArrows
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Pretopology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
have a : (ofArrows Z g).bind Ti ≤
  ofArrows
    (fun (ij : (i : ι) × κ (g i) sorry) ↦
      W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ κ (g i) sorry)))
    fun (ij : (i : ι) × κ (g i) sorry) ↦
    p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) sorry))) sorry (ij.snd (β := fun (i : ι) ↦ κ (g i) sorry)) ≫
      g (ij.fst (β := fun (i : ι) ↦ κ (g i) sorry))
Tactic: apply le_antisymm