awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w_1 : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ (T : Presieve.{v_1, u_1} B₂),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} B₂))
        {S : Presieve.{v_1, u_1} B₂ |
          ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → X a ⟶ B₂),
            S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}
        T ∧
      T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
have refine : (Presieve.ofArrows X₂ π₂).FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
Tactic: refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      {S : Presieve.{v_1, u_1} X |
        ∃ (X_1 : C) (f : X_1 ⟶ X), (S = Presieve.ofArrows (fun (x : Unit) ↦ X_1) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
      S →
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
          T ∧
        T.FactorsThruAlong S f
have this : ∀ (Z : C) (π : Z ⟶ X) (hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π) (h_epi : EffectiveEpi π),
  ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f
Tactic: ⟨Z, π, hπ, h_epi⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f
have this : ∃ (W : C) (h : W ⟶ Y) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f
Tactic: have := Preregular.exists_fac f π
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
this : ∃ (W : C) (h : W ⟶ Y) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f
have obtain : ∀ (W : C) (h : W ⟶ Y),
  EffectiveEpi h →
    ∀ (i : W ⟶ Z) (this : i ≫ π = h ≫ f),
      ∃ (T : Presieve.{v_1, u_1} Y),
        Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
            {S : Presieve.{v_1, u_1} Y |
              ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
            T ∧
          T.FactorsThruAlong S f
Tactic: obtain ⟨W, h, _, i, this⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f
have refine_1 : Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
  {S : Presieve.{v_1, u_1} Y |
    ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
  (Presieve.singleton h)
Tactic: refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
refine_1 :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
    (Presieve.singleton h)
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f
have refine_2 : (Presieve.singleton h).FactorsThruAlong S f
Tactic: refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton h = Presieve.ofArrows (fun (x : Unit) ↦ W) fun (x : Unit) ↦ h
have rw : Presieve.singleton h = Presieve.singleton h
Tactic: rw [Presieve.ofArrows_pUnit h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton h = Presieve.ofArrows (fun (x : Unit) ↦ W) fun (x : Unit) ↦ h
have this₁ : Presieve.singleton h = Presieve.singleton h
Tactic: {rw [Presieve.ofArrows_pUnit h]}
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W_1 : C
h : W_1 ⟶ Y
w : EffectiveEpi h
i : W_1 ⟶ Z
this : i ≫ π = h ≫ f
W : C
g : W ⟶ Y
hg : Presieve.singleton h g
⊢ ∃ (W_2 : C) (i : W ⟶ W_2) (e : W_2 ⟶ X), S e ∧ i ≫ e = g ≫ f
have refine_2 : ∃ (W : C) (i : W_1 ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = h ≫ f
Tactic: cases hg
Cleared hypotheses: W, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S e ∧ i ≫ e = h ≫ f
have refine_2 : S π
Tactic: refine ⟨Z, i, π, ⟨?_, this⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ S π
have refine_2 : Presieve.ofArrows (fun (x : Unit) ↦ Z) (fun (x : Unit) ↦ π) π
Tactic: cases hπ
Cleared hypotheses: S, hπ
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.ofArrows (fun (x : Unit) ↦ Z) (fun (x : Unit) ↦ π) π
have refine_2 : Presieve.singleton π π
Tactic: rw [Presieve.ofArrows_pUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      {S : Presieve.{v_1, u_1} X |
        ∃ (α : Type) (x : Finite α) (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
          S = Presieve.ofArrows X_1 π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X_1) (Sigma.desc π)}
      S →
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
              S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
          T ∧
        T.FactorsThruAlong S f
have this : ∀ (α : Type) (hα : Finite α) (Z : α → C) (π : (a : α) → Z a ⟶ X) (hS : S = Presieve.ofArrows Z π)
  (h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)),
  ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
            S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
        T ∧
      T.FactorsThruAlong S f
Tactic: ⟨α, hα, Z, π, hS, h_iso⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
            S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
        T ∧
      T.FactorsThruAlong S f
have refine_1 : Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
  {S : Presieve.{v_1, u_1} Y |
    ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
      S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
  (Presieve.ofArrows Z' π')
Tactic: refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
refine_1 :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
        S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
    (Presieve.ofArrows Z' π')
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
            S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
        T ∧
      T.FactorsThruAlong S f
have refine_2 : (Presieve.ofArrows Z' π').FactorsThruAlong S f
Tactic: refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
        S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
    (Presieve.ofArrows Z' π')
have refine_1 : ∃ (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
  Presieve.ofArrows Z' π' = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
W : C
g : W ⟶ Y
hg : Presieve.ofArrows Z' π' g
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S e ∧ i ≫ e = g ≫ f
have refine_2 : ∀ ⦃Y_1 : C⦄ (a : α), ∃ (W : C) (i : Z' a ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = π' a ≫ f
Tactic: rcases hg with ⟨a⟩
Cleared hypotheses: W, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
⊢ pullback.snd f (π a) ≫ π a = π' a ≫ f
have rw : Eq (α := Z' a ⟶ X) (pullback.snd f (π a) ≫ π a) (pullback.snd f (π a) ≫ π a)
Tactic: rw [CategoryTheory.Limits.pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
⊢ ∃ (W : C) (i : Z' a ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = π' a ≫ f
have refine_2 : S (π a)
Tactic: refine ⟨Z a, pullback.snd _ _, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
⊢ S (π a)
have refine_2 : Presieve.ofArrows Z π (π a)
Tactic: rw [hS]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
have mp : Presieve.IsSheaf (coherentTopology C) P →
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
mp :
  Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
have mpr : (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
  Presieve.IsSheaf (coherentTopology C) P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
have hP₁ : ∀ {X : C} (R : Presieve.{v_1, u_1} X),
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
    Presieve.IsSheafFor P R
Tactic: simp only [coherentTopology, Presieve.isSheaf_coverage] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)
have mp : Membership.mem (γ := Set (Presieve.{v_1, u_1} B))
  (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) B) (Presieve.ofArrows X π)
Tactic: apply hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf (coherentTopology C) P
have mpr : ∀ {X : C} (R : Presieve.{v_1, u_1} X),
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
    Presieve.IsSheafFor P R
Tactic: simp only [coherentTopology, Presieve.isSheaf_coverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W : C
⊢ Presieve.IsSheaf.{v_1, v_1, u_1} (coherentTopology C) (Functor.obj yoneda W)
have rw : ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
  EffectiveEpiFamily X π → Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows X π)
Tactic: rw [isSheaf_coherent]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
⊢ Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
have have : ∀ (h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone),
  Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
Tactic: have h_colim := isColimitOfEffectiveEpiFamilyStruct Y π H.effectiveEpiFamily.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone
⊢ Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
have rw : ∀ (h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone),
  Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
Tactic: rw [← Sieve.generateFamily_eq] at h_colim
Cleared hypotheses: h_colim
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t
have hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
Tactic: have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t
have obtain : ∀ (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X))
  (t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
  (t_uniq :
    ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
      (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
            x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
          y →
        y = t),
  ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t
Tactic: obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
    (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext