awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Sieve.{v_1, u_1} X
h : K.Saturate X S
⊢ K.Saturate Y (Sieve.pullback f S)
have of : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X) (f : Y ⟶ X),
  K.Saturate Y (Sieve.pullback f (Sieve.generate S))
Tactic: induction h with
  | of X S hS =>
    obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]
  | top X => exact .top _
  | transitive X R S _ hS H1 _ =>
    refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Sieve.{v_1, u_1} X
h : K.Saturate X S
of :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X) (f : Y ⟶ X),
    K.Saturate Y (Sieve.pullback f (Sieve.generate S))
⊢ K.Saturate Y (Sieve.pullback f S)
have top : ∀ (X : C) (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f ⊤)
Tactic: induction h with
  | of X S hS =>
    obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]
  | top X => exact .top _
  | transitive X R S _ hS H1 _ =>
    refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Sieve.{v_1, u_1} X
h : K.Saturate X S
of :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X) (f : Y ⟶ X),
    K.Saturate Y (Sieve.pullback f (Sieve.generate S))
top : ∀ (X : C) (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f ⊤)
⊢ K.Saturate Y (Sieve.pullback f S)
have transitive : ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
  K.Saturate X R →
    ∀ (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S))
      (H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)),
      (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
          R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))) →
        ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f S)
Tactic: induction h with
  | of X S hS =>
    obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]
  | top X => exact .top _
  | transitive X R S _ hS H1 _ =>
    refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ K.Saturate X S ↔ K.Saturate X S
have mp : K.Saturate X S → K.Saturate X S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
mp : K.Saturate X S → K.Saturate X S
⊢ K.Saturate X S ↔ K.Saturate X S
have mpr : K.Saturate X S → K.Saturate X S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
⊢ K.Saturate X S
have mp : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
mp : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
⊢ K.Saturate X S
have mp₁ : ∀ (X : C), K.Saturate X ⊤
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
mp : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
mp₁ : ∀ (X : C), K.Saturate X ⊤
⊢ K.Saturate X S
have mp₂ : ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
  K.Saturate X R →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
      K.Saturate X R → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) → K.Saturate X S
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
⊢ K.Saturate X S
have mpr : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
mpr : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
⊢ K.Saturate X S
have mpr₁ : ∀ (X : C), K.Saturate X ⊤
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
mpr : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
mpr₁ : ∀ (X : C), K.Saturate X ⊤
⊢ K.Saturate X S
have mpr₂ : ∀ (X : C) (S : Sieve.{v_1, u_1} X),
  K.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), K.Saturate X S → K.Saturate Y (Sieve.pullback f S)
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : K.Saturate X S
mpr : ∀ (X : C), ∀ S ∈ K.coverings X, K.Saturate X (Sieve.generate S)
mpr₁ : ∀ (X : C), K.Saturate X ⊤
mpr₂ :
  ∀ (X : C) (S : Sieve.{v_1, u_1} X),
    K.Saturate X S → ∀ (Y : C) (f : Y ⟶ X), K.Saturate X S → K.Saturate Y (Sieve.pullback f S)
⊢ K.Saturate X S
have mpr₃ : ∀ (X : C) (S R : Sieve.{v_1, u_1} X),
  K.Saturate X S →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)) →
      K.Saturate X S → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f R)) → K.Saturate X R
Tactic: induction hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.45260
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.45260} D
K : Coverage.{v_1, u_1} C
⊢ K.toGrothendieck.sieves = fun (X : C) ↦ setOf (K.Saturate X)
have h : ∀ (x : C) (x_1 : Sieve.{v_1, u_1} x), x_1 ∈ K.toGrothendieck.sieves x ↔ x_1 ∈ setOf (K.Saturate x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage
have mp : K.toGrothendieck ≤ J → K ≤ J.toCoverage
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
mp : K.toGrothendieck ≤ J → K ≤ J.toCoverage
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage
have mpr : K ≤ J.toCoverage → K.toGrothendieck ≤ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have mpr : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
mpr : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have mpr₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
H : K ≤ J.toCoverage
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
mpr : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
mpr₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have mpr₂ : ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
  K.Saturate X R →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
      ∀ (H1 : R ∈ (J : (a : C) → Set (Sieve a)) X)
        (H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y),
        S ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
J : GrothendieckTopology.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X
have rw : Sieve.generate S.arrows ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X
Tactic: rw [← Sieve.generate_sieve S]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.47256
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.47256} D
J : GrothendieckTopology.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Sieve.generate S.arrows ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) X
have hS₁ : S.arrows ∈ J.toCoverage.coverings X
Tactic: apply Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
⊢ K.toGrothendieck = sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
have a : K.toGrothendieck ≤ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
a : K.toGrothendieck ≤ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
⊢ K.toGrothendieck = sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
have a₁ : sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} ≤ K.toGrothendieck
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
⊢ K.toGrothendieck ≤ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
have a : ∀ (b : GrothendieckTopology.{v_1, u_1} C),
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
      {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} b →
    K.toGrothendieck ≤ b
Tactic: apply le_sInf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have a : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
    | of X S hS => apply hJ; assumption
    | top => apply J.top_mem
    | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
a : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have a₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
    | of X S hS => apply hJ; assumption
    | top => apply J.top_mem
    | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
J : GrothendieckTopology.{v_1, u_1} C
hJ :
  Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C))
    {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} J
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (K.toGrothendieck : (a : C) → Set (Sieve a)) X
a : ∀ (X : C) (S : Presieve.{v_1, u_1} X) (hS : S ∈ K.coverings X), Sieve.generate S ∈ (J : (a : C) → Set (Sieve a)) X
a₁ : ∀ (X : C), ⊤ ∈ (J : (a : C) → Set (Sieve a)) X
⊢ S ∈ (J : (a : C) → Set (Sieve a)) X
have a₂ : ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
  K.Saturate X R →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)) →
      ∀ (H1 : R ∈ (J : (a : C) → Set (Sieve a)) X)
        (H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ (J : (a : C) → Set (Sieve a)) Y),
        S ∈ (J : (a : C) → Set (Sieve a)) X
Tactic: induction hS with
    | of X S hS => apply hJ; assumption
    | top => apply J.top_mem
    | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Coverage.{v_1, u_1} C
⊢ sInf {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage} ≤ K.toGrothendieck
have a : Membership.mem (γ := Set (GrothendieckTopology.{v_1, u_1} C)) {J : GrothendieckTopology.{v_1, u_1} C | K ≤ J.toCoverage}
  K.toGrothendieck
Tactic: apply sInf_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hx : S ∈ x.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
have inl : ∀ (T : Presieve.{v_1, u_1} Y) (hT : T ∈ x.coverings Y ∧ T.FactorsThruAlong S f),
  ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
Tactic: obtain ⟨T, hT⟩ := x.pullback f S hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
D : Type ?u.48971
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.48971} D
x y : Coverage.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
have inr : ∀ (T : Presieve.{v_1, u_1} Y) (hT : T ∈ y.coverings Y ∧ T.FactorsThruAlong S f),
  ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
Tactic: obtain ⟨T, hT⟩ := y.pullback f S hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck
have h : ∀ (T : C) (S : Sieve.{v_1, u_1} T),
  S ∈ (J.toCoverage.toGrothendieck : (a : C) → Set (Sieve a)) T ↔ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) T
Tactic: ext T S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
⊢ J.toCoverage.Saturate T S ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows
have h : ∀ (h : J.toCoverage.Saturate T S), ∃ R ∈ J.coverings T, R ≤ S.arrows
Tactic: refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
h : ∀ (h : J.toCoverage.Saturate T S), ∃ R ∈ J.coverings T, R ≤ S.arrows
⊢ J.toCoverage.Saturate T S ↔ ∃ R ∈ J.coverings T, R ≤ S.arrows
have h₁ : (∃ R ∈ J.coverings T, R ≤ S.arrows) →
  ∀ (R : Presieve.{v_1, u_1} T) (hR : R ∈ J.coverings T) (hle : R ≤ S.arrows), J.toCoverage.Saturate T S
Tactic: refine ⟨fun h ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ J.toCoverage.coverings X
w : Presieve.{v_1, u_1} X
⊢ ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows
have left : S ∈ J.coverings X
Tactic: use S, hS, Sieve.le_generate S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
S : Presieve.{v_1, u_1} X
hS : S ∈ J.toCoverage.coverings X
w : Presieve.{v_1, u_1} X
left : S ∈ J.coverings X
⊢ ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows
have right : S ≤ (Sieve.generate S).arrows
Tactic: use S, hS, Sieve.le_generate S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
X : C
⊢ ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
have w : Presieve.{v_1, u_1} X
Tactic: use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
X : C
w : Presieve.{v_1, u_1} X
⊢ ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
have left : Presieve.singleton (𝟙 X) ∈ J.coverings X
Tactic: use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S : Sieve.{v_1, u_1} T
X : C
w : Presieve.{v_1, u_1} X
left : Presieve.singleton (𝟙 X) ∈ J.coverings X
⊢ ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
have right : LE.le (α := Presieve.{v_1, u_1} X) (Presieve.singleton (𝟙 X)) (Sieve.arrows ⊤)
Tactic: use Presieve.singleton (𝟙 X), J.has_isos (𝟙 X), le_top
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hle : ∃ R_1 ∈ J.coverings X, R_1 ≤ R.arrows
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have h : ∀ (R' : Presieve.{v_1, u_1} X) (hR' : R' ∈ J.coverings X) (hle : R' ≤ R.arrows), ∃ R ∈ J.coverings X, R ≤ S.arrows
Tactic: obtain ⟨R', hR', hle⟩ := hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have h : ∀ (S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y)
  (hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y)
  (hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows),
  ∃ R ∈ J.coverings X, R ≤ S.arrows
Tactic: choose S' hS' hS'le using hfS
Cleared hypotheses: hfS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have h : (R'.bind fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' sorry) ∈ J.coverings X
Tactic: refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coverage (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
J : Pretopology.{v_1, u_1} C
T : C
S_1 : Sieve.{v_1, u_1} T
X : C
R S : Sieve.{v_1, u_1} X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
R' : Presieve.{v_1, u_1} X
hR' : R' ∈ J.coverings X
hle : R' ≤ R.arrows
S' : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → R.arrows f → Presieve.{v_1, u_1} Y
hS' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ∈ J.coverings Y
hS'le : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (a : R.arrows f), S' a ≤ (Sieve.pullback f S).arrows
h : (R'.bind fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' ⋯) ∈ J.coverings X
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have h₁ : ∀ (Z : C) (u : Z ⟶ X) (hu : R'.bind (fun (Y : C) (f : Y ⟶ X) (hf : R' f) ↦ S' sorry) u), S.arrows u
Tactic: refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩