awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
⊢ IsSheafFor F R
have this : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)
Tactic: have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hF : PreservesFiniteProducts F
X : C
R : Presieve.{v_1, u_1} X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
this : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor F R
have this₁ : R.Extensive
Tactic: have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F
have mp : IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
mp : IsSheaf (extensiveTopology C) F → PreservesFiniteProducts F
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F
have mpr : PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : IsSheaf (extensiveTopology C) F
⊢ PreservesFiniteProducts F
have h₁ : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
Tactic: rw [IsSheaf] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
⊢ PreservesFiniteProducts F
have mp : ∀ (n : ℕ) {K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ} {c : Cone K} (hc : IsLimit c),
  Nonempty (IsLimit (F.mapCone c))
Tactic: refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
have mp : IsLimit (F.mapCone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)
have mp : (X : Dᵒᵖ) → IsLimit (F := (K ⋙ F) ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) (F.mapCone c))
Tactic: apply coyonedaJointlyReflectsLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
⊢ IsLimit (F := (K ⋙ F) ⋙ Functor.obj coyoneda (op E)) (Functor.mapCone (Functor.obj coyoneda (op E)) (F.mapCone c))
have h₁ : Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
Tactic: specialize h E
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
n : ℕ
K : Functor.{0, v_1, 0, u_1} (Discrete (Fin n)) Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
h : Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
⊢ IsLimit (F := (K ⋙ F) ⋙ Functor.obj coyoneda (op E)) (Functor.mapCone (Functor.obj coyoneda (op E)) (F.mapCone c))
have h₁ : PreservesFiniteProducts (F ⋙ Functor.obj coyoneda (op E))
Tactic: rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
inst_3 : FinitaryExtensive.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
h : PreservesFiniteProducts F
E : D
⊢ Presieve.IsSheaf (extensiveTopology C) (F ⋙ Functor.obj coyoneda (op E))
have mpr : PreservesFiniteProducts (F ⋙ Functor.obj coyoneda (op E))
Tactic: rw [Presieve.isSheaf_iff_preservesFiniteProducts]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp : S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X →
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
mp :
  S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X →
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
⊢ S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mpr : (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
  S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) S
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
have mp : ∀ (α : Type) (w : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X) (h : S = Presieve.ofArrows Y π)
  (h' : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)),
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
Tactic: obtain ⟨α, _, Y, π, h, h'⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
have mp : Nonempty (IsColimit (Cofan.mk X π))
Tactic: refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
mp : Nonempty (IsColimit (Cofan.mk X π))
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
have mp₁ : ∀ (a : α), (Sieve.generate S).arrows (π a)
Tactic: refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))
have this : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc (Cofan.mk X π).inj)
Tactic: have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
S : Presieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (X := sigmaObj.{0, v_1, u_1} Y) (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)
have mp : (Sieve.generate (Presieve.ofArrows Y π)).arrows (π a)
Tactic: obtain ⟨rfl, _⟩ := h
Cleared hypotheses: S, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S : Sieve.{v_1, u_1} X_1
X : C
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
have mp : IsColimit.{0, v_1, 0, u_1} (J := Discrete Unit) (F := Discrete.functor fun (x : Unit) ↦ X)
  (Cofan.mk X fun (x : Unit) ↦ 𝟙 X)
Tactic: refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S : Sieve.{v_1, u_1} X_1
X : C
⊢ IsIso.{v_1, u_1} (X := sigmaObj.{0, v_1, u_1} fun (b : Unit) ↦ X) (Y :=
    Cocone.pt.{0, v_1, 0, u_1} (J := Discrete Unit) (F := Discrete.functor fun (x : Unit) ↦ X)
      (Cofan.mk X fun (x : Unit) ↦ 𝟙 X))
    (Sigma.desc (Cofan.inj (Cofan.mk X fun (x : Unit) ↦ 𝟙 X)))
have this : IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : Unit) ↦ X)
  (Iso.hom (coproductUniqueIso fun (x : Unit) ↦ X) : (sigmaObj.{0, v_1, u_1} fun (x : Unit) ↦ X) ⟶ X)
Tactic: have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S : Sieve.{v_1, u_1} X_1
X : C
⊢ IsColimit.{0, v_1, 0, u_1} (J := Discrete Unit) (F := Discrete.functor fun (x : Unit) ↦ X)
    (Cofan.mk X fun (x : Unit) ↦ 𝟙 X)
have this : IsIso.{v_1, u_1} (X := sigmaObj.{0, v_1, u_1} fun (b : Unit) ↦ X) (Y :=
  Cocone.pt.{0, v_1, 0, u_1} (J := Discrete Unit) (F := Discrete.functor fun (x : Unit) ↦ X)
    (Cofan.mk X fun (x : Unit) ↦ 𝟙 X))
  (Sigma.desc (Cofan.inj (Cofan.mk X fun (x : Unit) ↦ 𝟙 X)))
Tactic: have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h : Coverage.Saturate (extensiveCoverage C) X R
h_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Coverage.Saturate (extensiveCoverage C) Y (Sieve.pullback f S)
a :
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
        Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp : ∀ (α : Type) (w : Finite α) (Y₁ : α → C) (π : (a : α) → Y₁ a ⟶ X) (h : Nonempty (IsColimit (Cofan.mk X π)))
  (h' : ∀ (a : α), R.arrows (π a)),
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
Tactic: obtain ⟨α, w, Y₁, π, h, h'⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X_1 : C
S_1 : Sieve.{v_1, u_1} X_1
X : C
R S : Sieve.{v_1, u_1} X
h_1 : Coverage.Saturate (extensiveCoverage C) X R
h_2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Coverage.Saturate (extensiveCoverage C) Y (Sieve.pullback f S)
b :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
        Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), R.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp : ∀ (β : (a : α) → Type),
  (∀ (a : α), Finite (β a)) →
    ∀ (Y_n : (a : α) → β a → C) (π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a)
      (H :
        ∀ (a : α),
          Nonempty (IsColimit (Cofan.mk (Y₁ a) (π_n a))) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)),
      ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
        Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
Tactic: choose β _ Y_n π_n H using fun a => b (h' a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp : ∀ (X : C) (S : Presieve.{v_1, u_1} X)
  (hS :
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) S),
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
Tactic: induction h with
    | of X S hS =>
      obtain ⟨α, _, Y, π, h, h'⟩ := hS
      refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
      · have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩
      · obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩
    | top X =>
      refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
      have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
      exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)
    | transitive X R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, h, h'⟩ := a
      choose β _ Y_n π_n H using fun a => b (h' a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
mp :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X)
    (hS :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) S),
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp₁ : ∀ (X : C),
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
Tactic: induction h with
    | of X S hS =>
      obtain ⟨α, _, Y, π, h, h'⟩ := hS
      refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
      · have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩
      · obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩
    | top X =>
      refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
      have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
      exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)
    | transitive X R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, h, h'⟩ := a
      choose β _ Y_n π_n H using fun a => b (h' a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
mp :
  ∀ (X : C) (S : Presieve.{v_1, u_1} X)
    (hS :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) S),
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)
mp₁ :
  ∀ (X : C),
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
    Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
have mp₂ : ∀ (X : C) (R S : Sieve.{v_1, u_1} X),
  Coverage.Saturate (extensiveCoverage C) X R →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Coverage.Saturate (extensiveCoverage C) Y (Sieve.pullback f S)) →
      ∀
        (a :
          ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
            Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), R.arrows (π a))
        (b :
          ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            R.arrows f →
              ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
                Nonempty (IsColimit (Cofan.mk Y π)) ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)),
        ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
          Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
Tactic: induction h with
    | of X S hS =>
      obtain ⟨α, _, Y, π, h, h'⟩ := hS
      refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
      · have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩
      · obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩
    | top X =>
      refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
      have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
      exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)
    | transitive X R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, h, h'⟩ := a
      choose β _ Y_n π_n H using fun a => b (h' a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
        fun c => (H c.fst).2 c.snd⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
have mpr : Presieve.ofArrows Y π ≤ S.arrows
Tactic: apply (extensiveCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
mpr : Presieve.ofArrows Y π ≤ S.arrows
⊢ S ∈ (extensiveTopology C : (a : C) → Set (Sieve a)) X
have mpr₁ : Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
  (Precoverage.coverings (Coverage.toPrecoverage (extensiveCoverage C)) X) (Presieve.ofArrows Y π)
Tactic: apply (extensiveCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)