mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
⊢ Presheaf.IsLocallySurjective J φ

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
⊢ Presheaf.IsLocallySurjective J φ
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.left_id ∈ {BiconeHom.left_id}

Tactic:
;

Goal state after:
case left_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.left_id ∈ {BiconeHom.left_id}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.left val✝ ∈ {BiconeHom.left val✝}

Tactic:
;

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.left val✝ ∈ {BiconeHom.left val✝}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.right_id ∈ {BiconeHom.right_id}

Tactic:
;

Goal state after:
case right_id
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ BiconeHom.right_id ∈ {BiconeHom.right_id}
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.right val✝ ∈ {BiconeHom.right val✝}

Tactic:
;

Goal state after:
case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
val✝ : J
⊢ BiconeHom.right val✝ ∈ {BiconeHom.right val✝}
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case self
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| x (u ≫ f) ⋯

Tactic:
;

Goal state after:
case self
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| x (u ≫ f) ⋯
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case self.f
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| u ≫ f

Tactic:
;

Goal state after:
case self.f
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
| u ≫ f
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : E.I₀
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : E.I₀
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : F.I₀
⊢ ({ s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 F).s₀ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : F.I₀
⊢ ({ s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 F).s₀ x✝
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F

Tactic:
;

Goal state after:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i✝ : E.I₀
i : ↑R.uncurry
⊢ (↑i).fst ≅ YR (↑i).snd ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i✝ : E.I₀
i : ↑R.uncurry
⊢ (↑i).fst ≅ YR (↑i).snd ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S := ⋯
F : PreZeroHypercover S := ⋯
i✝ : E.I₀
i : ↑R.uncurry
⊢ YR (↑i).snd ⋯ ≅ (↑i).fst

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S := ⋯
F : PreZeroHypercover S := ⋯
i✝ : E.I₀
i : ↑R.uncurry
⊢ YR (↑i).snd ⋯ ≅ (↑i).fst
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i✝ : E.I₀
i : ↑T.uncurry
⊢ YT (↑i).snd ⋯ ≅ (↑i).fst

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i✝ : E.I₀
i : ↑T.uncurry
⊢ YT (↑i).snd ⋯ ≅ (↑i).fst
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.f (Small.restrictFun E i))

Tactic:
;

Goal state after:
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.f (Small.restrictFun E i))
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ S ∈ K.coverings X

Tactic:
;

Goal state after:
case a.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ S ∈ K.coverings X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.hS
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
⊢ T ∈ K.coverings Y

Tactic:
;

Goal state after:
case mpr.hS
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
⊢ T ∈ K.coverings Y
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:
;

Goal state after:
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✝
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✝
x✝ : C
⊢ ((𝟭 (C ⥤ D)).map f✝ ≫ ((𝟭 (C ⥤ D)).obj Y✝).rightUnitor.inv ≫ Y✝.whiskerLeft adj.unit ≫ (Y✝.associator F G).inv).app
      x✝ =
    ((((𝟭 (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✝).app
      x✝

Tactic:
;

Goal state after:
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✝
x✝ : C
⊢ ((𝟭 (C ⥤ D)).map f✝ ≫ ((𝟭 (C ⥤ D)).obj Y✝).rightUnitor.inv ≫ Y✝.whiskerLeft adj.unit ≫ (Y✝.associator F G).inv).app
      x✝ =
    ((((𝟭 (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✝).app
      x✝
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:
;

Goal state after:
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✝
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✝
x✝ : C
⊢ (((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).app
      x✝ =
    (((X✝.associator G F).hom ≫ X✝.whiskerLeft adj.counit ≫ X✝.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f✝).app x✝

Tactic:
;

Goal state after:
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✝
x✝ : C
⊢ (((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).app
      x✝ =
    (((X✝.associator G F).hom ≫ X✝.whiskerLeft adj.counit ≫ X✝.rightUnitor.hom) ≫ (𝟭 (C ⥤ E)).map f✝).app x✝
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
x✝ : E
⊢ (((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)).app
      x✝ =
    (𝟙 (((whiskeringLeft E D C).obj G).obj X)).app x✝

Tactic:
;

Goal state after:
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
x✝ : E
⊢ (((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)).app
      x✝ =
    (𝟙 (((whiskeringLeft E D C).obj G).obj X)).app x✝
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
x✝ : D
⊢ ({ 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)).app
      x✝ =
    (𝟙 (((whiskeringLeft D E C).obj F).obj X)).app x✝

Tactic:
;

Goal state after:
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
x✝ : D
⊢ ({ 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)).app
      x✝ =
    (𝟙 (((whiskeringLeft D E C).obj F).obj X)).app x✝
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 α'
x : A
⊢ ((whiskerRight α G ≫ (L.associator F' G).hom) ≫
          L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom).app
      x =
    (whiskerRight α' G ≫ (L.associator F'' G).hom).app x

Tactic:
;

Goal state after:
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 α'
x : A
⊢ ((whiskerRight α G ≫ (L.associator F' G).hom) ≫
          L.whiskerLeft (isoWhiskerRight (F'.leftKanExtensionUnique α F'' α') G).hom).app
      x =
    (whiskerRight α' G ≫ (L.associator F'' G).hom).app x