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

Goal state before:
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 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 φ
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ S ∈ (F.inducedTopology (regularTopology 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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ S ∈ (F.inducedTopology (regularTopology D)) X
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
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 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
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : S ∈ (F.inducedTopology (regularTopology D)) X
⊢ ∃ Y π, EffectiveEpi π ∧ S.arrows π
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (F.preimage (g₀ ≫ π))

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ EffectiveEpi (F.preimage (g₀ ≫ π))
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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))

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.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
H₂ : (Sieve.functorPushforward F S).arrows π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
⊢ S.arrows (F.preimage (g₀ ≫ π))
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
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 π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : (ConcreteCategory.hom (P.map (pullback.fst π π).op)) b = (ConcreteCategory.hom (P.map (pullback.snd π π).op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = ⟨b, hb'⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.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 π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : (ConcreteCategory.hom (P.map (pullback.fst π π).op)) b = (ConcreteCategory.hom (P.map (pullback.snd π π).op)) b
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = ⟨b, hb'⟩
ha₂ :
  ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.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.SheafComparison

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝³ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
inst✝ : ReflectsFiniteLimits s
left✝ : PreservesFiniteProducts (F ⋙ s)
hF₂ : EqualizerCondition (F ⋙ s)
x✝² x✝¹ : C
π : x✝² ⟶ x✝¹
x✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ IsLimit (Fork.ofι (F.map π.op) ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢
  exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

Goal state after:
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✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

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✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ (∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))) →
    Presheaf.IsLocallySurjective (extensiveTopology 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✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
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✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ (∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) f

Tactic:
·

Goal state after:
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✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ (∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))) →
    Presheaf.IsLocallySurjective (extensiveTopology C) f
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
·

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
·

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ (Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z)

pp: case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ ⦃Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ⦄
    (i j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
·

Goal state after:
case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ (Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ),
    Nonempty (op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ ⦃Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ⦄
    (i j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a

Tactic:
·

Goal state after:
case h₂
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
⊢ ∀ ⦃Z : (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryᵒᵖ⦄
    (i j : op ((Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.categoryMk π ⋯) ⟶ Z),
    ∃ a, i = (ObjectProperty.homMk (Over.homMk c.fst ⋯)).op ≫ a ∧ j = (ObjectProperty.homMk (Over.homMk c.snd ⋯)).op ≫ a
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case e'_3
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y) =
    (ConcreteCategory.hom (G.map (π a).op)) y

Tactic:
·

Goal state after:
case e'_3
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this✝ : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
this : (ConcreteCategory.hom (f.app (op (Z a)))) (x a) = (ConcreteCategory.hom (G.map (π a).op)) y
⊢ (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y) =
    (ConcreteCategory.hom (G.map (π a).op)) y
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
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f → Presheaf.IsLocallySurjective (regularTopology C) f

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
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology 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
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f → Presheaf.IsLocallySurjective (regularTopology C) f
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
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
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f

Tactic:
·

Goal state after:
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
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f