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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
⊢ K.Saturate X T

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
f : S ⟶ T
hf : Presieve.singleton f ∈ J.coverings T
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ J.coverings T

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.IsStableUnderComposition
E : J.ZeroHypercover T
F : J.ZeroHypercover T
inst✝ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ (E.inter F.toPreZeroHypercover).presieve₀ ∈ J.coverings T

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover T
ι : Type w'
e : ι ≃ E.I₀
⊢ (E.reindex e).presieve₀ ∈ J.coverings T

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ (E.sum F.toPreZeroHypercover).presieve₀ ∈ J.coverings S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T✝ : C
E : J.ZeroHypercover S
T : C
f : T ⟶ S
hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J.coverings S
⊢ (E.add f).presieve₀ ∈ J.coverings S

Tactic:
by

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

Goal state before:
pp: case transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X✝ Y : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝ : K.Saturate X R
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : ∀ (f : Y ⟶ X), K.Saturate Y (Sieve.pullback f R)
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄, R.arrows f → ∀ (f_1 : Y ⟶ Y_1), K.Saturate Y (Sieve.pullback f_1 (Sieve.pullback f S))
f : Y ⟶ X
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
| transitive X R S _ hS H1 _ =>

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
S T : C
inst✝¹ : J.IsStableUnderComposition
inst✝ : J.HasIsos
X Y : C
f : X ⟶ Y
hf : Presieve.singleton f ∈ J.coverings Y
E : J.ZeroHypercover X
⊢ (PreZeroHypercover.pushforward f E.toPreZeroHypercover).presieve₀ ∈ J.coverings Y

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X Y : C
f : Y ⟶ X
S : Sieve X
h : K.Saturate X S
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F✝ : C ⥤ D
K : Precoverage D
F : C ⥤ D
E : J.ZeroHypercover S
h : J ≤ comap F K
⊢ (PreZeroHypercover.map F E.toPreZeroHypercover).presieve₀ ∈ K.coverings (F.obj S)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
inst✝ : Small.{w', w} E.I₀
⊢ (E.restrictIndex ⇑(equivShrink E.I₀).symm).presieve₀ ∈ J.coverings S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows Y f g
⊢ E.presieve₀ g

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S ↔ K.Saturate X S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows Y f g
⊢ ∃ j, ∃ (h : Z = E.X j), g = eqToHom h ≫ E.f j

Tactic:
by

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
⊢ K.toGrothendieck.sieves = fun X ↦ Set.ofPred (K.Saturate X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T✝ : C
E : J.ZeroHypercover S
inst✝² : E.Small
T : C
f : T ⟶ S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : ∀ (i : E.I₀), HasPullback f (E.f i)
i : E.restrictIndexOfSmall.I₀
⊢ HasPullback f (E.restrictIndexOfSmall.f i)

Tactic:
by

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T✝ : C
E : J.ZeroHypercover S
inst✝² : E.Small
T : C
f : T ⟶ S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : ∀ (i : E.I₀), HasPullback f (E.f i)
⊢ (pullback₁ f E).Small

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
X : C
R : Presieve X
⊢ R ∈ J.coverings X ↔ ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
by

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J X
⊢ S ∈ J.toCoverage.toGrothendieck X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J K : Precoverage C
h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X
⊢ J ≤ K

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ J : Precoverage C
inst✝ : J.Small
S : C
E : J.ZeroHypercover S
⊢ E.Small

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : Precoverage C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
J : Precoverage D
inst✝ : J.Small
X : C
E : (comap F J).ZeroHypercover X
⊢ E.Small

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ K.toGrothendieck = sInf {J | K ≤ J.toCoverage}

Tactic:
by

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ x.coverings X ∪ y.coverings X, ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ≤ E.presieve₀

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ E.Small

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ CommSq (F.f i) (e.inv.h₀ i) (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
by

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝³ : Category.{v_1, ?u.2} C
inst✝² : Category.{v_2, ?u.4} D
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ J.coverings X
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : Coverage C
⊢ J.toGrothendieck = J.toGrothendieck

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
W : C
i : Z ⟶ W
e : W ⟶ X
h1 : S e
h2 : i ≫ e = g ≫ f
⊢ 𝟙 Z ≫ g = g

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ IsSheaf K.toGrothendieck P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_1, u_2} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := { toPreZeroHypercover := E₀, mem₀ := hR }
⊢ E.restrictIndexOfSmall.presieve₀ ≤ E₀.presieve₀

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
K : Coverage C
P : Cᵒᵖ ⥤ D
⊢ IsSheaf K.toGrothendieck P ↔
    ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
⊢ x = y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
inst✝ : H.IsGenerating
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ lift hP hE le F ≫ P.map f.op = F.ι { Y := Y, f := f, hf := hf }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
⊢ ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), lift hP hE le F ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
⊢ m = lift hP hE le F

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
⊢ ⊤ (Cover.oneHypercover ⟨S, hS⟩)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
⊢ (Cover.oneHypercover ⟨S, hS⟩).sieve₀ ≤ S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : J.IsGeneratedByOneHypercovers
P : Cᵒᵖ ⥤ A
⊢ IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork P))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ D⦄ (f : X ⟶ Y),
    (𝟭 (C ⥤ D)).map f ≫ ((𝟭 (C ⥤ D)).obj Y).rightUnitor.inv ≫ Y.whiskerLeft adj.unit ≫ (Y.associator F G).inv =
      (((𝟭 (C ⥤ D)).obj X).rightUnitor.inv ≫ X.whiskerLeft adj.unit ≫ (X.associator F G).inv) ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ E⦄ (f : X ⟶ Y),
    ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f ≫
        (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom =
      ((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
⊢ ((whiskeringLeft E D C).obj G).map
        ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ }.app
          X) ≫
      { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
        (((whiskeringLeft E D C).obj G).obj X) =
    𝟙 (((whiskeringLeft E D C).obj G).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
⊢ { app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }.app
        (((whiskeringLeft D E C).obj F).obj X) ≫
      ((whiskeringLeft D E C).obj F).map
        ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
          X) =
    𝟙 (((whiskeringLeft D E C).obj F).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
F' : C ⥤ B
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
h✝ : (F' ⋙ G).IsLeftKanExtension (whiskerRight α G ≫ (L.associator F' G).hom)
F'' : C ⥤ B
α' : F ⟶ L ⋙ F''
h : F''.IsLeftKanExtension α'
⊢ (whiskerRight α G ≫ (L.associator F' G).hom) ≫
      L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom =
    whiskerRight α' G ≫ (L.associator F'' G).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : L.HasLeftKanExtension F
inst✝ : G.PreservesLeftKanExtension F L
⊢ (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
⊢ whiskerRight (L.leftKanExtensionUnit F) G ≫
      (L.associator (L.leftKanExtension F) G).hom ≫ L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).hom =
    L.leftKanExtensionUnit (F ⋙ G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
a : A
⊢ G.map ((L.leftKanExtensionUnit F).app a) ≫ (G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    (L.leftKanExtensionUnit (F ⋙ G)).app a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
⊢ L.leftKanExtensionUnit (F ⋙ G) ≫ L.whiskerLeft (G.leftKanExtensionCompIsoOfPreserves F L).inv =
    whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
a : A
⊢ (L.leftKanExtensionUnit (F ⋙ G)).app a ≫ (G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.leftKanExtensionUnit F).app a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseLeftKanExtension F L
inst✝ : L.HasPointwiseLeftKanExtension F
⊢ whiskerRight (L.pointwiseLeftKanExtensionUnit F) G ≫
      (L.associator (L.pointwiseLeftKanExtension F) G).hom ≫
        L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom =
    L.pointwiseLeftKanExtensionUnit (F ⋙ G)

Tactic:
by

Goal state after: