awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
X : C
y : ToType (FC := TypeCat.Fun) ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))
⊢ ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
    ToType (FC := TypeCat.Fun)
      ((Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)).obj (P :=
            Presheaf.IsSheaf (coherentTopology C)).obj
        (op X'))),
    Eq (α := (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (InducedCategory.Hom.hom (c.π.app (op 0))) (op X')) :
            (a : (((Functor.const ℕᵒᵖ).obj c.pt).obj (op 0)).obj.obj (op X')) → (F.obj (op 0)).obj.obj (op X'))
          x :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
            (a : (F.obj (op 0)).obj.obj (op X)) → (F.obj (op 0)).obj.obj (op X'))
          y :
        (F.obj (op 0)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
have hh : EffectiveEpi (X := (preimageDiagram hF X y).obj (op 0)) (Y := limit (preimageDiagram hF X y))
  (limit.π (preimageDiagram hF X y) (op 0))
Tactic: have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) :=
    h _ fun n ↦ by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
inst_3 : HasLimitsOfShape.{0, 0, v, u} ℕᵒᵖ C
h :
  ∀ (G : Functor.{0, v, 0, u} ℕᵒᵖ C),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (op 0)) (Y := limit G) (limit.π G (op 0))
inst_4 : HasSheafify (coherentTopology C) (Type v)
inst_5 : Balanced (Sheaf (coherentTopology C) (Type v))
inst_6 : GrothendieckTopology.WEqualsLocallyBijective (coherentTopology C) (Type v) (FA := TypeCat.Fun)
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Epi (X := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))
have simp_rw : ∀ (hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE sorry).op)),
  Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F₁ :=
    Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (op 0)) (c.π.app (op 0))
Tactic: simp_rw [← Sheaf.isLocallySurjective_iff_epi'] at hF ⊢
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
⊢ F.IsCoverDense (coherentTopology D)
have refine : ∀ (B : D),
  Sieve.generate
      (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
    (coherentTopology D : (a : D) → Set (Sieve a)) B
Tactic: refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ Sieve.generate
      (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
        (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B)) ∈
    (coherentTopology D : (a : D) → Set (Sieve a)) B
have hS : Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
  (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
  (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
have hS : Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
  Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
Tactic: refine ⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B,
    fun _ => F.effectiveEpiOver B, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
hS :
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
⊢ Membership.mem (γ := Set (Presieve.{v_2, u_2} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage D)) B)
    (Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B))
have hS₁ : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := B) (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦
  F.effectiveEpiOver B
Tactic: refine ⟨Unit, inferInstance, fun _ => F.effectiveEpiOverObj B,
    fun _ => F.effectiveEpiOver B, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦ F.effectiveEpiOver B
have hS : ∀ (x : D) (x_1 : x ⟶ B),
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
Tactic: funext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 =
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
have hS : Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
  Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B x : D
x_1 : x ⟶ B
⊢ Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)))
      (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1 ↔
    Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1
have hS : Presieve.ofArrows (fun (x : Unit) ↦ F.effectiveEpiOverObj B) (fun (x : Unit) ↦ F.effectiveEpiOver B) x_1 →
  Presieve.singleton (Y := F.obj (EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some sorry)))
    (F.effectiveEpiOver B : F.effectiveEpiOverObj B ⟶ B) x_1
Tactic: refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
B : D
⊢ EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := B) (fun (x : Unit) ↦ F.effectiveEpiOverObj B) fun (x : Unit) ↦
    F.effectiveEpiOver B
have hS : EffectiveEpi (Y := F.effectiveEpiOverObj B) (F.effectiveEpiOver B)
Tactic: rw [← effectiveEpi_iff_effectiveEpiFamily]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
have refine_1 : (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
  ∀ (α : Type),
    Finite α →
      ∀ (Y : α → C) (π : (a : α) → Y a ⟶ X) (H₁ : EffectiveEpiFamily Y π) (H₂ : ∀ (a : α), S.arrows (π a)),
        S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
Tactic: refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
refine_1 :
  (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    ∀ (α : Type),
      Finite α →
        ∀ (Y : α → C) (π : (a : α) → Y a ⟶ X) (H₁ : EffectiveEpiFamily Y π) (H₂ : ∀ (a : α), S.arrows (π a)),
          S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
⊢ (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) ↔
    S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
have refine_2 : ∀ (hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X),
  ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic: refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
have refine_1 : ∃ (α : Type) (_ : Finite α) (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X),
  EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Tactic: apply (mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
h : ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X),
    EffectiveEpiFamily Y π ∧ ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
have refine_1 : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (i : α) ↦ F.obj (Y i)) fun (i : α) ↦ F.map (π i)
Tactic: refine ⟨α, inferInstance, fun i => F.obj (Y i),
      fun i => F.map (π i), ⟨?_,
      fun a => Sieve.image_mem_functorPushforward F S (H₂ a)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have refine_2 : ∀ (α : Type),
  Finite α →
    ∀ (Y : α → D) (π : (a : α) → Y a ⟶ F.obj X) (H₁ : EffectiveEpiFamily Y π)
      (H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)),
      ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
        EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic: obtain ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ := (mem_sieves_iff_hasEffectiveEpiFamily _).mp hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have refine_2 : ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic: refine ⟨α, inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
⊢ ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
Tactic: have : EffectiveEpiFamily _ (fun a ↦ g₀ a ≫ π a) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
⊢ ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have refine_2 : EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)
Tactic: refine ⟨Z, fun a ↦ F.preimage (g₀ a ≫ π a), ?_, fun a ↦ (?_ : S.arrows (F.preimage _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
refine_2 : EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)
⊢ ∃ (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
have refine_2₁ : ∀ (a : α), S.arrows (F.preimage (g₀ a ≫ π a))
Tactic: refine ⟨Z, fun a ↦ F.preimage (g₀ a ≫ π a), ?_, fun a ↦ (?_ : S.arrows (F.preimage _))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ F.preimage (g₀ a ≫ π a)
have refine_2 : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦
  F.map (F.preimage (g₀ a ≫ π a))
Tactic: refine F.finite_effectiveEpiFamily_of_map _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.SheafComparison (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : F.PreservesFiniteEffectiveEpiFamilies
inst_3 : F.ReflectsFiniteEffectiveEpiFamilies
inst_4 : F.Full
inst_5 : F.Faithful
inst_6 : F.EffectivelyEnough
inst_7 : Precoherent.{v_2, u_2} D
X : C
S : Sieve.{v_1, u_1} X
hS : S ∈ (F.inducedTopology (coherentTopology D) : (a : C) → Set (Sieve a)) X
α : Type
w : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun (a : α) ↦ EffectivePresentation.p.{v_1, u_1, v_2, u_2} (F := F) (Nonempty.some ⋯)
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun (a : α) ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily.{v_2, u_2, 0} (C := D) (B := F.obj X) (fun (a : α) ↦ F.obj (Z a)) fun (a : α) ↦ g₀ a ≫ π a
a : α
⊢ S.arrows (F.preimage (g₀ a ≫ π a))
have refine_2 : ∀ (W : C) (g₁ : W ⟶ X) (g₂ : Y a ⟶ F.obj W) (h₁ : S.arrows g₁) (h₂ : π a = g₂ ≫ F.map g₁),
  S.arrows (F.preimage (g₀ a ≫ π a))
Tactic: obtain ⟨W, g₁, g₂, h₁, h₂⟩ := H₂ a