mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))

pp: case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)

Tactic:
·

Goal state after:
case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)

Tactic:
·

Goal state after:
case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
·

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) a

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) a
Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
·

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Precoherent C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
⊢ IsIso (Sigma.desc (Cofan.mk X fun x ↦ 𝟙 X).inj)

Tactic:
have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S : Sieve X✝
X : C
this : IsIso (coproductUniqueIso fun x ↦ X).hom
⊢ IsIso (Sigma.desc (Cofan.mk X fun x ↦ 𝟙 X).inj)
Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
·

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F

Tactic:
·

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mpr.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

pp: case mpr.hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).coverings X

Tactic:
·

Goal state after:
case mpr.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mpr.hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).coverings X

Tactic:
·

Goal state after:
case mpr.hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (extensiveCoverage C).coverings X
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ Presieve.singleton (F.effectiveEpiOver B) =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ Presieve.singleton (F.effectiveEpiOver B) =
    Presieve.ofArrows (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
x✝ : ∃ α, ∃ (_ : Finite α), ∃ Y π, 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)) X

pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
x✝ : ∃ α, ∃ (_ : Finite α), ∃ Y π, 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)) X
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (coherentTopology D)) X
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj 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 ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
⊢ EffectiveEpiFamily Z fun a ↦ F.preimage (g₀ a ≫ π a)

pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj 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 ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
a : α
⊢ S.arrows (F.preimage (g₀ a ≫ π a))

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj 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 ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
⊢ EffectiveEpiFamily Z fun a ↦ F.preimage (g₀ a ≫ π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj 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 ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
a : α
⊢ S.arrows (F.preimage (g₀ a ≫ π a))

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj 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 ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
a : α
⊢ S.arrows (F.preimage (g₀ a ≫ π a))
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective (regularTopology C) f →
    ∀ (X : C) (y : ToType (G.obj (op X))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y

pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
⊢ (∀ (X : C) (y : ToType (G.obj (op X))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ),
          ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y) →
    Presheaf.IsLocallySurjective (regularTopology C) f

Tactic:
·

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective (regularTopology C) f →
    ∀ (X : C) (y : ToType (G.obj (op X))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: case mp
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ IsLocallySurjective φ → Epi φ

pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ Epi φ → IsLocallySurjective φ

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
⊢ IsLocallySurjective φ → Epi φ