awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve.{u_2, u_3} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
have mpr : ∀ (X : C) (S : Presieve.{u_2, u_3} X) (hS : S ∈ J.coverings X) ⦃Y : C⦄ (f : Y ⟶ X),
  Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
Tactic: induction hS with
    | of X S hS =>
      exact fun _ _ => H S hS
    | top =>
      simp [Presieve.isSheafFor_top P]
    | pullback X S hS _ f ih =>
      intro Y f
      rw [← S.pullback_comp]
      exact ih (f ≫ _)
    | transitive X R S hS h H1 H2 =>
      intro Y f
      simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
      choose H1 H1' using H1
      choose H2 H2' using H2
      refine ⟨?_, fun x hx => ?_⟩
      · intro x t₁ t₂ h₁ h₂
        refine (H1 f).ext (fun Z g hg => ?_)
        refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
        simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← op_comp, h₁, h₂]
        simpa only [Sieve.pullback_apply, Category.assoc] using hgg
      let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
      have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
        rw [hx]
        rw [reassoc_of% h]
      choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
        H2' hg (𝟙 _) (y g) (hy g)
      let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
      have hq : q.Compatible := by
        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
        apply (H2 h₁ g₁).ext
        intro ZZ gg hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
        · dsimp [y]; congr 1; simp only [Category.assoc, h]
        · simpa [reassoc_of% h] using hgg
        · simpa using hgg
      obtain ⟨t, ht⟩ := H1' f q hq
      refine ⟨t, fun Z g hg => ?_⟩
      refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
      rw [← comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
      on_goal 2 => simpa using hgg
      refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
      rw [← comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
      on_goal 2 => simpa using hggg
      refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
      rw [← comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
      apply hx
      simp
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_3
inst : Category.{u_2, u_3} C
J : Precoverage.{u_2, u_3} C
P : Functor.{u_2, u_1, u_3, u_1 + 1} Cᵒᵖ (Type u_1)
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve.{u_2, u_3} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
mpr :
  ∀ (X : C) (S : Presieve.{u_2, u_3} X) (hS : S ∈ J.coverings X) ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
have mpr₁ : ∀ (X : C) ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows
Tactic: induction hS with
    | of X S hS =>
      exact fun _ _ => H S hS
    | top =>
      simp [Presieve.isSheafFor_top P]
    | pullback X S hS _ f ih =>
      intro Y f
      rw [← S.pullback_comp]
      exact ih (f ≫ _)
    | transitive X R S hS h H1 H2 =>
      intro Y f
      simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
      choose H1 H1' using H1
      choose H2 H2' using H2
      refine ⟨?_, fun x hx => ?_⟩
      · intro x t₁ t₂ h₁ h₂
        refine (H1 f).ext (fun Z g hg => ?_)
        refine (H2 hg (𝟙 _)).ext (fun ZZ gg hgg => ?_)
        simp only [Sieve.pullback_id, Sieve.pullback_apply] at hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← op_comp, h₁, h₂]
        simpa only [Sieve.pullback_apply, Category.assoc] using hgg
      let y : ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
        ((S.pullback (g ≫ f)).pullback (𝟙 _)).arrows.FamilyOfElements P :=
        fun Z g ZZ gg hgg => x (gg ≫ g) (by simpa using hgg)
      have hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible := by
        intro Z g Y₁ Y₂ ZZ g₁ g₂ f₁ f₂ h₁ h₂ h
        rw [hx]
        rw [reassoc_of% h]
      choose z hz using fun ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : R.pullback f g) =>
        H2' hg (𝟙 _) (y g) (hy g)
      let q : (R.pullback f).arrows.FamilyOfElements P := fun Z g hg => z hg
      have hq : q.Compatible := by
        intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
        apply (H2 h₁ g₁).ext
        intro ZZ gg hgg
        simp only [← comp_apply]
        rw [← P.map_comp, ← P.map_comp, ← op_comp, ← op_comp, hz, hz]
        · dsimp [y]; congr 1; simp only [Category.assoc, h]
        · simpa [reassoc_of% h] using hgg
        · simpa using hgg
      obtain ⟨t, ht⟩ := H1' f q hq
      refine ⟨t, fun Z g hg => ?_⟩
      refine (H1 (g ≫ f)).ext (fun ZZ gg hgg => ?_)
      rw [← comp_apply _ (P.map gg.op), ← P.map_comp, ← op_comp, ht]
      on_goal 2 => simpa using hgg
      refine (H2 hgg (𝟙 _)).ext (fun ZZZ ggg hggg => ?_)
      rw [← comp_apply _ (P.map ggg.op), ← P.map_comp, ← op_comp, hz]
      on_goal 2 => simpa using hggg
      refine (H2 hgg ggg).ext (fun ZZZZ gggg _ => ?_)
      rw [← comp_apply _ (P.map gggg.op), ← P.map_comp, ← op_comp]
      apply hx
      simp
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_1 : ∀ (hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X), ∃ R ∈ J.coverings X, R ≤ S.arrows
Tactic: refine ⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
refine_1 : ∀ (hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X), ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X ↔ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_2 : (∃ R ∈ J.coverings X, R ≤ S.arrows) →
  ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows),
    S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
Tactic: refine ⟨fun hS ↦ ?_, fun ⟨R, hR, hle⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S : Sieve.{u_1, u_2} X_1
X : C
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
⊢ ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
have right : R ≤ (Sieve.generate R).arrows
Tactic: use R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
h : ∃ R ∈ J.coverings X, R ≤ S.arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
have refine_1 : ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows),
  ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
Tactic: obtain ⟨R, hR, hle⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
have this : R.HasPullbacks f
Tactic: have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
have refine_1 : Presieve.pullbackArrows f R ≤ (Sieve.pullback f S).arrows
Tactic: refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Presieve.pullbackArrows f R ≤ (Sieve.pullback f S).arrows
have refine_1 : Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S
Tactic: rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S : Sieve.{u_1, u_2} X
hS : J.Saturate X S
Y : C
f : Y ⟶ X
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
this : R.HasPullbacks f
⊢ Sieve.pullback f (Sieve.generate R) ≤ Sieve.pullback f S
have refine_1 : Sieve.generate R ≤ S
Tactic: apply Sieve.pullback_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have refine_1 : ∀ (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X) (hle : R ≤ S.arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
Tactic: obtain ⟨R, hR, hle⟩ := hleS
Cleared hypotheses: hleS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve.{u_1, u_2} X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have hR₁ : ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [mem_iff_exists_zeroHypercover] at hR
Cleared hypotheses: hR, hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve.{u_1, u_2} X
hR : ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have refine_1 : ∀ (E : J.ZeroHypercover X) (hle : Presieve.ofArrows E.X E.f ≤ S.arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
Tactic: obtain ⟨E, rfl⟩ := hR
Cleared hypotheses: R, hR, hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
have obtain : ∀ (R' : Presieve.{u_1, u_2} (E.X i))
  (hR' : Membership.mem (γ := Set (Presieve.{u_1, u_2} (E.X i))) (J.coverings (E.X i)) R')
  (hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows),
  ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
Tactic: obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve.{u_1, u_2} (E.X i)
hR' : Membership.mem (γ := Set (Presieve.{u_1, u_2} (E.X i))) (J.coverings (E.X i)) R'
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
have hR'₁ : ∃ (𝒰 : J.ZeroHypercover (E.X i)), R' = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [mem_iff_exists_zeroHypercover] at hR'
Cleared hypotheses: hR', hle'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve.{u_1, u_2} (E.X i)
hR' : ∃ (𝒰 : J.ZeroHypercover (E.X i)), R' = Presieve.ofArrows 𝒰.X 𝒰.f
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
have obtain : ∀ (F : J.ZeroHypercover (E.X i)) (hle' : Presieve.ofArrows F.X F.f ≤ (Sieve.pullback (E.f i) T).arrows),
  ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
Tactic: obtain ⟨F, rfl⟩ := hR'
Cleared hypotheses: R', hR', hle'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
F : J.ZeroHypercover (E.X i)
hle' : Presieve.ofArrows F.X F.f ≤ (Sieve.pullback (E.f i) T).arrows
w : J.ZeroHypercover (E.X i)
⊢ ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
have h : F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
Tactic: use F
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (hypothesis)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have hleT₁ : ∀ (i : E.I₀), ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
Tactic: replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
Cleared hypotheses: hleT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
hleT : ∀ (i : E.I₀), ∃ (F : J.ZeroHypercover (E.X i)), F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have refine_1 : ∀ (F : (i : E.I₀) → J.ZeroHypercover (E.X i))
  (hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows), ∃ R ∈ J.coverings X, R ≤ T.arrows
Tactic: choose F hle' using hleT
Cleared hypotheses: hleT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
have refine_1 : (E.bind F).presieve₀ ≤ T.arrows
Tactic: refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X_1 : C
S_1 : Sieve.{u_1, u_2} X_1
X : C
S T : Sieve.{u_1, u_2} X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
F : (i : E.I₀) → J.ZeroHypercover (E.X i)
hle' : ∀ (i : E.I₀), (F i).presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
⊢ (E.bind F).presieve₀ ≤ T.arrows
have refine_1 : ∀ (i : (E.bind F).I₀), T.arrows ((E.bind F).f i)
Tactic: rw [Presieve.ofArrows_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_1 : ∀ (X : C) (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X), ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
Tactic: induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_2
inst : Category.{u_1, u_2} C
J : Precoverage.{u_1, u_2} C
inst_1 : J.IsStableUnderComposition
inst_2 : J.IsStableUnderBaseChange
inst_3 : J.HasPullbacks
inst_4 : J.HasIsos
X : C
S : Sieve.{u_1, u_2} X
hS : S ∈ (J.toGrothendieck : (a : C) → Set (Sieve a)) X
refine_1 :
  ∀ (X : C) (R : Presieve.{u_1, u_2} X) (hR : R ∈ J.coverings X), ∃ R_1 ∈ J.coverings X, R_1 ≤ (Sieve.generate R).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows
have refine_1₁ : ∀ (X : C), ∃ R ∈ J.coverings X, R ≤ Sieve.arrows ⊤
Tactic: induction hS with
    | of X R hR =>
      use R, hR
      exact Sieve.le_generate R
    | top X =>
      exact ⟨Presieve.singleton (𝟙 X), mem_coverings_of_isIso (𝟙 X), by simp⟩
    | pullback X S hS Y f h =>
      obtain ⟨R, hR, hle⟩ := h
      have : R.HasPullbacks f := J.hasPullbacks_of_mem f hR
      refine ⟨R.pullbackArrows f, pullbackArrows_mem f hR, ?_⟩
      rw [← Sieve.generate_le_iff, Sieve.pullbackArrows_comm]
      apply Sieve.pullback_monotone
      rwa [Sieve.generate_le_iff]
    | transitive X S T hS hT hleS hleT =>
      obtain ⟨R, hR, hle⟩ := hleS
      rw [mem_iff_exists_zeroHypercover] at hR
      obtain ⟨E, rfl⟩ := hR
      replace hleT (i : E.I₀) : ∃ (F : J.ZeroHypercover (E.X i)),
          F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows := by
        obtain ⟨R', hR', hle'⟩ := hleT (hle _ _ ⟨i⟩)
        rw [mem_iff_exists_zeroHypercover] at hR'
        obtain ⟨F, rfl⟩ := hR'
        use F
      choose F hle' using hleT
      refine ⟨(E.bind F).presieve₀, (E.bind F).mem₀, ?_⟩
      rw [Presieve.ofArrows_le_iff]
      intro i
      exact hle' _ _ _ ⟨i.snd⟩
Cleared hypotheses: hS