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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsSheaf K G

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsSheaf K G
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsIso φ
X : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (φ.app X)))

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsIso φ
X : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (φ.app X)))
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ J.W (whiskerRight f F)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : HasWeakSheafify J A
inst✝ : J.PreservesSheafification F
⊢ ∀ (X : Cᵒᵖ ⥤ A), IsIso ((toPresheafToSheafCompComposeAndSheafify J F).app X)

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : HasWeakSheafify J A
inst✝ : J.PreservesSheafification F
⊢ ∀ (X : Cᵒᵖ ⥤ A), IsIso ((toPresheafToSheafCompComposeAndSheafify J F).app X)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
a✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ IsIso (G₁.map (adj₁.unit.app P))

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
a✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ IsIso (G₁.map (adj₁.unit.app P))
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (f ≫ adj₁.unit.app P₂) F)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight (adj₁.unit.app P₁ ≫ (G₁ ⋙ sheafToPresheaf J A).map f) F)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight ((sheafToPresheaf J A).map (G₁.map f)) F)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight ((sheafToPresheaf J A).map (G₁.map f)) F)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp.refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
Y : C
f : Y ⟶ unop X
hf : (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f
⊢ (ConcreteCategory.hom (F₂.map f.op)) ((ConcreteCategory.hom (φ.app (op (unop X)))) x) =
    (ConcreteCategory.hom (F₂.map f.op)) ((ConcreteCategory.hom (φ.app (op (unop X)))) y)

Tactic:
]

Goal state after:
case mp.refine_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
a✝ : IsLocallyInjective J φ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y) ∈ J (unop X)
S : Sieve (unop X) := equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)
T : ⦃Y : C⦄ → ⦃f : Y ⟶ unop X⦄ → S.arrows f → Sieve Y :=
  fun Y f x_1 ↦ equalizerSieve ((ConcreteCategory.hom (F₁.map f.op)) x) ((ConcreteCategory.hom (F₁.map f.op)) y)
Y : C
f : Y ⟶ unop X
hf : (equalizerSieve ((ConcreteCategory.hom (φ.app X)) x) ((ConcreteCategory.hom (φ.app X)) y)).arrows f
⊢ (ConcreteCategory.hom (F₂.map f.op)) ((ConcreteCategory.hom (φ.app (op (unop X)))) x) =
    (ConcreteCategory.hom (F₂.map f.op)) ((ConcreteCategory.hom (φ.app (op (unop X)))) y)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight (adj₁.unit.app P) F ≫ (sheafToPresheaf J B).map ((sheafCompose J F).map (G₁.map f)))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight (adj₁.unit.app P) F ≫ (sheafToPresheaf J B).map ((sheafCompose J F).map (G₁.map f)))
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = whiskerRight (adj₁.unit.app P) F

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = whiskerRight (adj₁.unit.app P) F
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst✝ : IsLocallyInjective J ψ
a✝ : IsLocallyInjective J φ
⊢ IsLocallyInjective J (φ ≫ ψ)

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
φψ : F₁ ⟶ F₃
fac : φ ≫ ψ = φψ
inst✝ : IsLocallyInjective J ψ
a✝ : IsLocallyInjective J φ
⊢ IsLocallyInjective J (φ ≫ ψ)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α = adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ (∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Cᵒᵖ ⥤ A), IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app X)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
⊢ (∀ (P : Cᵒᵖ ⥤ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))) ↔
    ∀ (X : Cᵒᵖ ⥤ A), IsIso ((sheafComposeNatTrans J F adj₁ adj₂).app X)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
⊢ J.W ((sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P)) ↔
    J.W ((sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P))

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ equalizerSieve x y ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
⊢ J.PreservesSheafification F

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
⊢ J.PreservesSheafification F
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝³ : HasWeakSheafify J A
inst✝² : HasWeakSheafify J B
inst✝¹ : J.HasSheafCompose F
inst✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ toSheafify J (P ⋙ F) = toSheafify J (P ⋙ F)

Tactic:
]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective J (J.toPlus P ≫ J.toPlus (J.plusObj P))

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
⊢ IsLocallyInjective J (J.toPlus P ≫ J.toPlus (J.plusObj P))
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} E
F : D ⥤ E
inst✝¹³ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁸ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
this :
  (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    { hom := (J.sheafifyCompIso F P).inv }
⊢ (sheafToPresheaf J E).map { hom := (J.sheafifyCompIso F P).inv } = (J.sheafifyCompIso F P).inv

Tactic:
]

Goal state after:
C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} E
F : D ⥤ E
inst✝¹³ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝¹¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹⁰ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁸ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
this :
  (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    { hom := (J.sheafifyCompIso F P).inv }
⊢ (sheafToPresheaf J E).map { hom := (J.sheafifyCompIso F P).inv } = (J.sheafifyCompIso F P).inv