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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (t.app (op Z)))
      ⟨(ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g.op)) (shrinkYonedaObjObjEquiv.symm f), ⋯⟩ =
    (ConcreteCategory.hom (t.app (op Z)))
      ((ConcreteCategory.hom ((shrinkFunctor.{w, v₁, u₁} S).toFunctor.map g.op)) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
e_1✝ : F.obj Z = F.obj (op (unop Z))
⊢ g.unop ≫ shrinkYonedaObjObjEquiv f = unop g ≫ shrinkYonedaObjObjEquiv f

Tactic:
rfl

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

Goal state before:
pp: case e'_3.e'_2.e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
Y : Cᵒᵖ
u : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hu : u ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ u = u

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ Multiequalizer.ι ((unop S).index P) ((Cover.Arrow.base I).map f.unop) =
    Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I ((J.pullback f✝).map f.unop)).base

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ ((unop W).index P).snd i ≫ η.app (op i.r.Z) =
    Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ P.map i.r.g₂.op ≫ η.app (op i.r.Z)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
Y : C
f : Y ⟶ X
hf : (↑S).arrows f
⊢ ↑x { Y := Y, f := f, hf := hf } = ↑x { Y := Y, f := f, hf := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
Y✝ : C
f✝ : Y✝ ⟶ Y
hf✝ : (↑(S.pullback f)).arrows f✝
⊢ ↑x { Y := Y✝, f := f✝, hf := hf✝ }.base =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ f, hf := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
i : S.shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) x = ↑(Meq.mk S x) i

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
⊢ J.toPlus P ≫ γ = J.toPlus P ≫ γ

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P = (J.isoToPlus P hP).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
⊢ range p ≤ range p

Tactic:
rfl

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

Goal state before:
pp: case e'_2.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑x ({ Y := Y✝, f := f✝, hf := hf✝ }.map h1.unop)

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
e : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f) ≃
  Subtype (Arrows.Compatible P fun i ↦ (Over.map p).map (f i)) :=
  { toFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, invFun := fun s ↦ ⟨fun i ↦ ↑s i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (⇑e ∘ Arrows.toCompatible ((Over.map p).op ⋙ P) f) ↔
    Function.Bijective (Arrows.toCompatible P fun i ↦ (Over.map p).map (f i))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ (fun x ↦ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (p.app U✝)) x)) ⁻¹' G.obj V✝ ⊆
    (fun x ↦ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (p.app U✝)) x)) ⁻¹' G.obj V✝

Tactic:
rfl

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

Goal state before:
pp: case e'_3.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑y { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑y ({ Y := Y✝, f := f✝, hf := hf✝ }.map h2.unop)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ s ∈ (sheafify J G).obj U

Tactic:
change _ ∈ J _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s ∈ J (unop U)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop (op S))).arrows f✝
e : ↑(x.refine h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(y.refine h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  CD (((unop (op S)).index P).left { Y := Y✝, f := f✝, hf := hf✝ }) =
    ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y))
⊢ ↑x ({ Y := Y✝, f := f✝, hf := hf✝ }.map h1) =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: case e'_3.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S✝ T : J.Cover X
x : Meq P S✝
y : Meq P T
S : J.Cover X
h1 : S ⟶ S✝
h2 : S ⟶ T
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop (op S))).arrows f✝
e : ↑(x.refine h1) { Y := Y✝, f := f✝, hf := hf✝ } = ↑(y.refine h2) { Y := Y✝, f := f✝, hf := hf✝ }
e_1✝ :
  CD (((unop (op S)).index P).left { Y := Y✝, f := f✝, hf := hf✝ }) =
    ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y))
⊢ ↑y ({ Y := Y✝, f := f✝, hf := hf✝ }.map h2) =
    ↑y { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
this✝ : (Sieve.bind U.arrows B).arrows (m ≫ l ≫ h ≫ f)
this : (ConcreteCategory.hom (P.map m.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) = y ⋯ (m ≫ l) ⋯
⊢ (ConcreteCategory.hom (P.map m.op)) ((ConcreteCategory.hom (P.map l.op)) (t (h ≫ f) ⋯)) = s (m ≫ l ≫ h ≫ f) this✝

Tactic:
grind

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (f.app (op W)))
      ⟨(ConcreteCategory.hom (F.map j.op)) ↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s), hj⟩ =
    (ConcreteCategory.hom (f.app (op W))) ⟨(ConcreteCategory.hom (F.map j.op)) ((ConcreteCategory.hom (F.map i)) ↑s), ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
⊢ Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))

Tactic:
intro x y h
  simp only [toPlus_eq_mk] at h
  rw [eq_mk_iff_exists] at h
  obtain ⟨W, h1, h2, hh⟩ := h
  apply hsep X W
  intro I
  apply_fun fun e => e I at hh
  exact hh

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

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
this :
  ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩) =
    ↑((ConcreteCategory.hom ((homOfLe h).app (op V))) ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)
⊢ ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app (op V)))
        ((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) ⟨x, hx⟩)) =
    ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ m ≫ (((Functor.const K).obj E.pt).obj k).map i.f.op ≫ (E.π.app k).app (op i.Y) =
    m ≫ (W.multifork E.pt).ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ ((sheafToPresheaf J D).mapCocone S).ι.app j = (S.ι.app j).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget TopCat).map f)) ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : ↑X ≃ₜ ↑Y
x✝ : ↑X
⊢ (homeoOfIso (isoOfHomeo f)) x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x✝ : ↑X
⊢ (ConcreteCategory.hom (isoOfHomeo (homeoOfIso f)).hom) x✝ = (ConcreteCategory.hom f.hom) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i✝ j✝ : J
f : i✝ ⟶ j✝
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i✝)) x) =
    (ConcreteCategory.hom (S.π.app i✝ ≫ F.map f)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : ↑S.1
i j : J
f : i ⟶ j
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (S.π.app i)) x) =
    (ConcreteCategory.hom (S.π.app i ≫ F.map f)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = S.π.app j
a : ↑S.pt
⊢ (ConcreteCategory.hom m) a =
    (ConcreteCategory.hom
        (ofHom
          { toFun := fun x ↦ ⟨fun x_1 ↦ (Hom.hom ((limitCone F).π.app x_1)) ((Hom.hom m) x), ⋯⟩,
            continuous_toFun := ⋯ }))
      a

Tactic:
rfl

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

Goal state before:
pp: case h
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ (ConcreteCategory.hom ((J.plusObj P).map i.f.op)) t = ↑(Meq.mk S t) i

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
j✝ : J
⊢ (coneOfConeForget (forget.mapCone c)).π.app j✝ =
    (isoOfHomeo
          (let __Equiv := Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt;
          { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom ≫
      c.π.app j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
c' : Cocone F := coconeOfCoconeForget (forget.mapCocone c)
hc' : IsColimit c' := isColimitCoconeOfForget (forget.mapCocone c) (isColimitOfPreserves forget hc)
e : c'.pt ≅ c.pt := hc'.coconePointUniqueUpToIso hc
he : ∀ (j : J), c'.ι.app j ≫ e.hom = c.ι.app j
⊢ ⨆ i, coinduced (⇑(homeoOfIso e)) (coinduced (⇑(ConcreteCategory.hom (c.ι.app i))) (F.obj i).str) =
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c'.ι.app j ≫ e.hom))) (F.obj j).str

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ IsColimit c

Tactic:
refine .ofIsoColimit (isColimitCoconeOfForget _ hc) (Cocone.ext ?_ ?_)

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ (coconeOfCoconeForget (forget.mapCocone c)).pt ≅ c.pt

case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ ∀ (j : J), (coconeOfCoconeForget (forget.mapCocone c)).ι.app j ≫ Iso.hom ?refine_1 = c.ι.app j
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
j✝ : J
⊢ (coconeOfCoconeForget (forget.mapCocone c)).ι.app j✝ ≫
      (isoOfHomeo
          (let __Equiv := Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt;
          { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom =
    c.ι.app j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case left
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
x✝ : ↑S.pt
⊢ (ConcreteCategory.hom
        (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ } ≫
          (X.prodBinaryFan Y).π.app { as := WalkingPair.left }))
      x✝ =
    (ConcreteCategory.hom (S.π.app { as := WalkingPair.left })) x✝

Tactic:
rfl

Goal state after: