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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose
          (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
              (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (Cone.postcompose
          (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
              (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
      (E.multifork G) ≅
    Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone c ≅ colim.mapCone (limit.cone F)

pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone (limit.cone F) ≅ limit.cone (F ⋙ colim)

Tactic:
·

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone c ≅ colim.mapCone (limit.cone F)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone (limit.cone F) ≅ limit.cone (F ⋙ colim)

Tactic:
·

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone (limit.cone F) ≅ limit.cone (F ⋙ colim)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd) =
    (G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd) =
    (G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd) =
    (G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd)

Tactic:
simpa using g.w₁₁ k

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ J X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y → Sieve.ofObjects Y X ∈ J X
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ J X

Tactic:
constructor
  · tauto
  · intro h W
    apply J.superset_covering _ (J.pullback_stable (hX.from W) h)
    rintro T a ⟨i, ⟨b⟩⟩
    exact ⟨i, ⟨b⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd) =
    (G.p₂ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ j✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₂ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd) =
    (G.p₂ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ j✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ j✝)).snd)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

pp: case hunique
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∀ (y₁ y₂ : ↑F.sections),
    (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂

Tactic:
·

Goal state after:
case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : ((overEquiv Y) (generate R)).arrows g
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : ((overEquiv Y) (generate R)).arrows g
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
hg : ((overEquiv Y).symm (generate R)).arrows g
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ generate (Presieve.functorPullback (Over.forget X) R) ≤ (overEquiv Y).symm (generate R)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
hg : ((overEquiv Y).symm (generate R)).arrows g
⊢ (generate (Presieve.functorPullback (Over.forget X) R)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ generate (Presieve.functorPullback (Over.forget X) R) ≤ (overEquiv Y).symm (generate R)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ generate (Presieve.functorPullback (Over.forget X) R) ≤ (overEquiv Y).symm (generate R)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hunique
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∀ (y₁ y₂ : ↑F.sections),
    (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂

Tactic:
·

Goal state after:
case hunique
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
⊢ ∀ (y₁ y₂ : ↑F.sections),
    (∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i) → (∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i) → y₁ = y₂
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g → ((overEquiv ((Over.map f).obj Z)).symm S).arrows g

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows g → (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g → ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows g → (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows g → (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f → (↑S).arrows f

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f → (↑S).arrows f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ (overEquiv U) (functorPullback (Over.post F) S) ≤ functorPullback F ((overEquiv ((Over.post F).obj U)) S)

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback F ((overEquiv ((Over.post F).obj U)) S) ≤ (overEquiv U) (functorPullback (Over.post F) S)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ (overEquiv U) (functorPullback (Over.post F) S) ≤ functorPullback F ((overEquiv ((Over.post F).obj U)) S)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback F ((overEquiv ((Over.post F).obj U)) S) ≤ (overEquiv U) (functorPullback (Over.post F) S)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback F ((overEquiv ((Over.post F).obj U)) S) ≤ (overEquiv U) (functorPullback (Over.post F) S)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (E.map (Over.forget X)).sieve₀ ∈ J ((Over.forget X).obj Y)

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (E.map (Over.forget X)).sieve₀ ∈ J ((Over.forget X).obj Y)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (E.map (Over.post F)).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (E.map (Over.post F)).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)