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

Goal state before:
pp: 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
x✝ : F.multicospanShape.R
⊢ (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).map (WalkingMulticospan.Hom.fst x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (𝟭 (WalkingMulticospan F.multicospanShape)).map (WalkingMulticospan.Hom.fst x✝)

Tactic:
by

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

Goal state before:
pp: 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
x✝ : F.multicospanShape.R
⊢ (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).map (WalkingMulticospan.Hom.snd x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (𝟭 (WalkingMulticospan F.multicospanShape)).map (WalkingMulticospan.Hom.snd x✝)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
⊢ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W

Tactic:
by

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

Goal state before:
pp: 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
c : WalkingMulticospan E.multicospanShape
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app c) ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj c) =
    𝟙 ((Hom.mapMulticospan f.hom).obj c)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f

Tactic:
by

Goal state after:
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
F : J ⥤ K ⥤ Type v
this : IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫ lim.map (whiskerRight (currying.unitIso.app F).inv colim))
⊢ IsIso (colimitLimitToLimitColimitCone F).hom

Tactic:
by

Goal state after:
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
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimitCone F).hom

Tactic:
by

Goal state after:
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
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimitCone F)

Tactic:
by

Goal state after:
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
⊢ PreservesFiniteLimits colim

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsLimit (E.multifork G) ≃ IsLimit (F.multifork G)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
by

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

Goal state before:
pp: 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 : G.I₀),
    (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i ≫
        (E.inter F).f ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i) =
      G.f i

Tactic:
by

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

Goal state before:
pp: 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✝
⊢ f.h₁ k ≫ E.p₁ (f.s₁ k, g.s₁ k).1 ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 =
    g.h₁ k ≫ F.p₁ (f.s₁ k, g.s₁ k).2 ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
by

Goal state after:
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
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : PreservesFiniteLimits (forget C)
inst✝³ : PreservesColimitsOfShape K (forget C)
inst✝² : HasFiniteLimits C
inst✝¹ : HasColimitsOfShape K C
inst✝ : (forget C).ReflectsIsomorphisms
⊢ PreservesFiniteLimits colim

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit F.flip) b =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
hR : functorPullback (Over.forget X) R = S
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Presieve Y
h :
  { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      a✝ ≤
    { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      b✝
⊢ a✝ ≤ b✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
⊢ Presieve.functorPushforward (Over.forget X) S.arrows = Presieve.map (Over.forget X) S.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
⊢ functorPullback (Over.forget X) (functorPushforward (Over.forget X) S) = S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
⊢ functorPushforward (Over.forget X) (functorPullback (Over.forget X) S) = S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Sieve Y
h : functorPushforward (Over.forget X) a✝ ≤ functorPushforward (Over.forget X) b✝
⊢ a✝ ≤ b✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y},
    { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ (b ≫ Over.Hom.left a) ≫ Over.Hom.left f = b ≫ Over.Hom.left (a ≫ f)

Tactic:
by

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

Goal state before:
pp: 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) =
    G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: 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
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.obj
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
⊢ f = g

Tactic:
by

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

Goal state before:
pp: 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
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ g = 𝟙 Z ≫ Over.Hom.left c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Z : C
f : Z ⟶ X
i : I
φ : Z ⟶ Y i
⊢ x.familyOfElements X f ⋯ = (ConcreteCategory.hom (F.map φ.op)) (x i)

Tactic:
by

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

Goal state before:
pp: 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) =
    G.p₂ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ j✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
⊢ (overEquiv Y₁) (pullback f S) = pullback (Over.Hom.left f) ((overEquiv Y₂) S)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
Z : Over X
f : Z ⟶ Y
⊢ ((overEquiv Y).symm S).arrows f ↔ S.arrows (Over.Hom.left f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
Z : C
f : Z ⟶ Y.left
⊢ ((overEquiv Y) S).arrows f ↔ S.arrows (Over.homMk f ⋯)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
I : Type u_1
Z : I → Over X
g : (i : I) → Z i ⟶ Y
⊢ (overEquiv Y) (ofArrows Z g) = ofArrows (fun i ↦ (Z i).left) fun i ↦ Over.Hom.left (g i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : PreOneHypercover S
inst✝ : E.HasPullbacks
mem₀ : E.sieve₀ ∈ J S
mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ E.sieve₁ p₁ p₂ ∈ J W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X : C
⊢ (x.familyOfElements X).Compatible

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: 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
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X = (ConcreteCategory.hom (F.map f.op)) (x i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ b ≫ (E.Y k).hom = (Over.mk (f✝ ≫ W.hom)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ c.ι i₁ ≫ F.obj.map p₁.op = c.ι i₂ ≫ F.obj.map p₂.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₁ = Over.homMk b ⋯ ≫ E.p₁ k

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
i₀ : E.I₀
⊢ multiforkLift c ≫ F.obj.map (E.f i₀).op = c.ι i₀

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₂ = Over.homMk b ⋯ ≫ E.p₂ k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: 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
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
⊢ ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ (overEquiv W) (E.sieve₁ p₁ p₂) = (E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: 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
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
i : I
⊢ (ConcreteCategory.hom (F.map (𝟙 (Y i)).op)) (x i) = x i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
W : Over X
u : Over.mk (g ≫ Y.hom) ⟶ W
v : W ⟶ Y
hv : R v
huv : u ≫ v = Over.homMk g ⋯
⊢ Over.Hom.left v = 𝟙 W.left ≫ (Over.forget X).map v

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
⊢ ∀ (E_1 : Multifork (E.multicospanIndex F.obj)) (m : E_1.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = E_1.ι i) → m = multiforkLift E_1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S✝ S : C
⊢ (PreOneHypercover.trivial S).sieve₀ ∈ J S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S✝ S : C
x✝⁴ x✝³ : (PreOneHypercover.trivial S).I₀
x✝² : C
x✝¹ : x✝² ⟶ (PreOneHypercover.trivial S).X x✝⁴
x✝ : x✝² ⟶ (PreOneHypercover.trivial S).X x✝³
h : x✝¹ ≫ (PreOneHypercover.trivial S).f x✝⁴ = x✝ ≫ (PreOneHypercover.trivial S).f x✝³
⊢ (PreOneHypercover.trivial S).sieve₁ x✝¹ x✝ ∈ J x✝²

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
Z : Over X
g : Z ⟶ Y
W : C
p : Z.left ⟶ W
q : W ⟶ Y.left
hq : R q
hpq : p ≫ q = Over.Hom.left g
⊢ p ≫ (Over.mk (q ≫ Y.hom)).hom = Z.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover 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)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) ≫ E.f i₁.1 = (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2)) ≫ E.f i₂.1

Tactic:
by

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

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

Tactic:
by

Goal state after: