mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
CD : D → Type (max u v)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
P : Cᵒᵖ ⥤ D
inst✝² : HasWeakSheafify J D
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : J.PreservesSheafification (forget D)
⊢ IsLocallyInjective J
    ((J.toSheafify (P ⋙ forget D) ≫ (plusPlusIsoSheafify J (Type (max u v)) (P ⋙ forget D)).hom) ≫
      (sheafifyComposeIso J (forget D) P).hom)

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₃
CD : D → Type (max u v)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
P : Cᵒᵖ ⥤ D
inst✝² : HasWeakSheafify J D
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : J.PreservesSheafification (forget D)
⊢ IsLocallyInjective J
    ((J.toSheafify (P ⋙ forget D) ≫ (plusPlusIsoSheafify J (Type (max u v)) (P ⋙ forget D)).hom) ≫
      (sheafifyComposeIso J (forget D) P).hom)
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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presheaf.IsSheaf J (F₁.obj ⋙ forget D)

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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝ : J.HasSheafCompose (forget D)
⊢ Presheaf.IsSheaf J (F₁.obj ⋙ forget D)
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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ IsLocallyInjective φ

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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ IsLocallyInjective φ
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
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
⊢ IsIso (J.sheafifyCompIso F P).inv

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
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
⊢ IsIso (J.sheafifyCompIso F P).inv
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
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
⊢ IsIso (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E))

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
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
⊢ IsIso (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ (ConcreteCategory.hom (G.map j.op)) ((ConcreteCategory.hom (f.app (op V))) t) =
    (ConcreteCategory.hom (G.map j.op)) ((ConcreteCategory.hom (f.app (op V))) t)

Tactic:
]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
⊢ IsIso f

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
⊢ IsIso f
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ ∀ (X : Cᵒᵖ), IsIso (((sheafToPresheaf J (Type w)).map f).app X)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
⊢ ∀ (X : Cᵒᵖ), IsIso (((sheafToPresheaf J (Type w)).map f).app X)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
X : Cᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (((sheafToPresheaf J (Type w)).map f).app X))

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app X))
X : Cᵒᵖ
⊢ Function.Bijective ⇑(ConcreteCategory.hom (((sheafToPresheaf J (Type w)).map f).app X))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ J U

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
U : C
t : CA (F.obj (op U))
⊢ ⊤ ∈ J U
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (f.app U)))

Tactic:
]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ IsIso (↾⇑(ConcreteCategory.hom (f.app U)))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_4.refine_1.right
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.right }

Tactic:
· simpa using! pullback.condition

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J f₁
inst✝ : IsLocallySurjective J f₂
U✝ : C
s : ToType (F₃.obj (op U✝))
V W : C
i : V ⟶ W
j : W ⟶ U✝
H : (imageSieve f₂ s).arrows j
t' : ToType (F₁.obj (op V))
ht' : (ConcreteCategory.hom (f₁.app (op V))) t' = (ConcreteCategory.hom (F₂.map i.op)) (Exists.choose H)
⊢ (ConcreteCategory.hom (F₃.map i.op)) ((ConcreteCategory.hom (F₃.map j.op)) s) =
    (ConcreteCategory.hom (F₃.map i.op)) ((ConcreteCategory.hom (F₃.map j.op)) s)

Tactic:
]

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

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

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
a✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op Y))) (t g ?mp.Hf) = (ConcreteCategory.hom (G.obj.map g.op)) s

pp: case mp.Hf
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (Presheaf.imageSieve f.hom s).arrows g

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op Y))) (t g ?mp.Hf) = (ConcreteCategory.hom (G.obj.map g.op)) s

case mp.Hf
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (Presheaf.imageSieve f.hom s).arrows g
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J (f₁ ≫ f₂)
inst✝ : IsLocallySurjective J f₁
X : Cᵒᵖ
x₁ x₂ : ToType (F₂.obj X)
h : (ConcreteCategory.hom (f₂.app X)) x₁ = (ConcreteCategory.hom (f₂.app X)) x₂
S : Sieve (unop X) := imageSieve f₁ x₁ ⊓ imageSieve f₁ x₂
hS : S ∈ J (unop X)
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦ equalizerSieve (localPreimage f₁ x₁ f ⋯) (localPreimage f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ (ConcreteCategory.hom (F₃.map f.op)) ((ConcreteCategory.hom (f₂.app X)) x₂) =
    (ConcreteCategory.hom (F₃.map f.op)) ((ConcreteCategory.hom (f₂.app (op (unop X)))) x₂)

Tactic:
]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
a✝ : IsIso f
⊢ IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
constructor <;> infer_instance

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

Goal state before:
pp: case mp
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsLocallyInjective ((sheafCompose J (forget A)).map f) ∧ IsLocallySurjective ((sheafCompose J (forget A)).map f)

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsLocallyInjective ((sheafCompose J (forget A)).map f) ∧ IsLocallySurjective ((sheafCompose J (forget A)).map f)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsLocallyInjective ((sheafCompose J (forget A)).map f) ∧ IsLocallySurjective ((sheafCompose J (forget A)).map f)

Tactic:
constructor <;> infer_instance

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
a✝ : IsIso f
⊢ IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
constructor <;> infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
constructor <;> infer_instance

Goal state after: