awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
refine_1 : EffectiveEpiFamily X₂ π₂
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine_2 : ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
Tactic: refine ⟨X₂, π₂, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)
have h₁ : ∀ (b : α),
  CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
      (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π' ≫ g) =
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
      (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ EffectiveEpiFamily X₂ π₂
have this : Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
  (Sigma.desc π₂)
Tactic: have : (Sigma.desc π' ≫ g) = Sigma.desc π₂ := by ext; simp [π₂, π']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
this :
  Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)
⊢ EffectiveEpiFamily X₂ π₂
have refine_1 : EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.desc π' ≫ g)
Tactic: rw [← effectiveEpi_desc_iff_effectiveEpiFamily, ← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
have refine_2 : ∀ (b : α),
  CategoryStruct.comp (Y := X₁ (id b))
      ((fun (b : α) ↦ (pullback.snd g' (Sigma.ι X₁ b) : Limits.pullback g' (Sigma.ι X₁ b) ⟶ X₁ b)) b) (π₁ (id b)) =
    π₂ b ≫ f
Tactic: refine ⟨id, fun b ↦ pullback.snd _ _, fun b ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
⊢ CategoryStruct.comp (Y := X₁ (id b))
      ((fun (b : α) ↦ (pullback.snd g' (Sigma.ι X₁ b) : Limits.pullback g' (Sigma.ι X₁ b) ⟶ X₁ b)) b) (π₁ (id b)) =
    π₂ b ≫ f
have refine_2 : Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
  (pullback.fst g' (Sigma.ι X₁ b) ≫ g' ≫ Sigma.desc π₁)
Tactic: simp only [X₂, π₂, id_eq, Category.assoc, ← hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
⊢ Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
    (pullback.fst g' (Sigma.ι X₁ b) ≫ g' ≫ Sigma.desc π₁)
have refine_2 : Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
  (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ Sigma.ι X₁ b) (Sigma.desc π₁))
Tactic: rw [← Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
⊢ Eq (α := GrothendieckTopology.{v_1, u_1} C) (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C))
    (coherentTopology C)
have h : ∀ (B : C) (S : Sieve.{v_1, u_1} B),
  S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
Tactic: ext B S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
have h : ∀ (h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B),
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h :
  ∀ (h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B),
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
have h₁ : ∀ (h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B),
  S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T
⊢ generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
have h : Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
  (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
have hT₁ : Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) Y) T ∨
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) Y) T
Tactic: simp only [Coverage.sup_covering, Set.mem_union] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
have h : Coverage.Saturate (coherentCoverage C) Y T
Tactic: apply Coverage.Saturate.transitive Y T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_2 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (coherentCoverage C) Y T
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
Tactic: apply Coverage.Saturate.transitive Y T
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
have h : Coverage.Saturate (coherentCoverage C) Y T
Tactic: apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T S_1 : Sieve.{v_1, u_1} Y
h_1 : Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T
h_2 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S_1)
a_ih : T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
a_ih_1 :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1
h : Coverage.Saturate (coherentCoverage C) Y T
⊢ S_1 ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S_1)
Tactic: apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
have h₁ : ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
  (hT :
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T),
  generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
Tactic: induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hT :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T),
    generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
have h₂ : ∀ (X : C), ⊤ ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
Tactic: induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hT :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y) T),
    generate T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
h₂ : ∀ (X : C), ⊤ ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
have h₃ : ∀ (Y : C) (T S : Sieve.{v_1, u_1} Y),
  Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y T →
    (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
        T.arrows f → Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1 (Sieve.pullback f S)) →
      T ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y →
        (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
            T.arrows f → Sieve.pullback f S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y_1) →
          S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) Y
Tactic: induction h with
    | of Y T hT =>
      apply Coverage.Saturate.of
      simp only [Coverage.sup_covering, Set.mem_union] at hT
      exact Or.elim hT
        (fun ⟨α, x, X, π, ⟨h, _⟩⟩ ↦ ⟨α, x, X, π, ⟨h, inferInstance⟩⟩)
        (fun ⟨Z, f, ⟨h, _⟩⟩ ↦ ⟨Unit, inferInstance, fun _ ↦ Z, fun _ ↦ f, ⟨h, inferInstance⟩⟩)
    | top => apply Coverage.Saturate.top
    | transitive Y T => apply Coverage.Saturate.transitive Y T <;> [assumption; assumption]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
T : Presieve.{v_1, u_1} Y
hT :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
⊢ generate T ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h : ∀ (I : Type),
  Finite I →
    ∀ (X : I → C) (f : (a : I) → X a ⟶ Y) (hT : EffectiveEpiFamily X f),
      generate (Presieve.ofArrows X f) ∈
        (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
Tactic: obtain ⟨I, _, X, f, rfl, hT⟩ := hT
Cleared hypotheses: T, hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ generate (Presieve.ofArrows X f) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h : Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) Y
  (generate
    (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
Tactic: apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
h :
  Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) Y
    (generate
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
⊢ generate (Presieve.ofArrows X f) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) Y
have h₁ : ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
  arrows
      (generate
        (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
      f_1 →
    Coverage.Saturate (extensiveCoverage C ⊔ regularCoverage C) Y_1
      (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))
Tactic: apply Coverage.Saturate.transitive Y (generate (Presieve.ofArrows
        (fun (_ : Unit) ↦ (∐ fun (i : I) => X i)) (fun (_ : Unit) ↦ Sigma.desc f)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ Coverage.Saturate.{v_1, u_1} (extensiveCoverage C ⊔ regularCoverage C) Y
    (generate
      (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f))
have h : Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
  (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C ⊔ regularCoverage C)) Y)
  (Presieve.ofArrows (fun (x : Unit) ↦ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i) fun (x : Unit) ↦ Sigma.desc f)
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Comparison (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
Y_1 : C
I : Type
w : Finite I
X : I → C
f : (a : I) → X a ⟶ Y_1
hT : EffectiveEpiFamily X f
R Y : C
i : Unit
ψ : R ⟶ sigmaObj.{0, v_1, u_1} fun (i : I) ↦ X i
⊢ Sieve.pullback (ψ ≫ Sigma.desc f) (generate (Presieve.ofArrows X f)) ∈
    (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R
have h : Sieve.pullback ψ (Sieve.pullback (Sigma.desc f) (generate (Presieve.ofArrows X f))) ∈
  (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) R
Tactic: rw [Sieve.pullback_comp]