mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ F.obj U
⊢ x ∈ H.obj U

Tactic:
exact h₁ _ h

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ G = ⊤ → IsIso G.ι

Tactic:
rintro rfl

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
⊢ IsIso ⊤.ι
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
        (λ_ (M.obj Y)).symm.hom =
    (λ_ (M.obj X)).symm.hom ≫ (Monoidal.tensorObj (unit (R ⋙ forget₂ CommRingCat RingCat)) M).map f

Tactic:
ext m

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom
        (M.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
            (λ_ (M.obj Y)).symm.hom))
      m =
    (ModuleCat.Hom.hom
        ((λ_ (M.obj X)).symm.hom ≫ (Monoidal.tensorObj (unit (R ⋙ forget₂ CommRingCat RingCat)) M).map f))
      m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
        (ρ_ (M.obj Y)).symm.hom =
    (ρ_ (M.obj X)).symm.hom ≫ (Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f

Tactic:
ext m

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom
        (M.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
            (ρ_ (M.obj Y)).symm.hom))
      m =
    (ModuleCat.Hom.hom
        ((ρ_ (M.obj X)).symm.hom ≫ (Monoidal.tensorObj M (unit (R ⋙ forget₂ CommRingCat RingCat))).map f))
      m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ (x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝) = x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝

Tactic:
by ext1; apply tensorHom_comp_tensorHom

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Sieve.generate (pullbackArrows g R) ≤ Sieve.pullback g S

Tactic:
Sieve.pullbackArrows_comm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Sieve.pullback g (Sieve.generate R) ≤ Sieve.pullback g S
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)

Tactic:
refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_
  · rfl
  · exact _root_.isGLB_sInf _

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ f = g → singleton f g

Tactic:
rintro rfl

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
⊢ x.Compatible

Tactic:
intro Y Z W g₁ g₂ f₁ f₂ hf₁ hf₂ heq

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
x : FamilyOfElements P R
hx : (x.map f).Compatible
Y Z W : C
g₁ : W ⟶ Y
g₂ : W ⟶ Z
f₁ : Y ⟶ X
f₂ : Z ⟶ X
hf₁ : R f₁
hf₂ : R f₂
heq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ hf₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
Y : C
i : I
b : W ⟶ Z i
fac : b ≫ f i = a ≫ e.hom
⊢ b ≫ f i ≫ e.inv = a

Tactic:
simp [reassoc_of% fac]

Goal state after:
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
x : { x // x.Compatible }
⊢ (fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩)
      ((fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ }) x) =
    x

Tactic:
by
    ext
    dsimp
    rw! [Equiv.apply_symm_apply]
    simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
F : Cᵒᵖ ⥤ Type w
x : FamilyOfElements F S.arrows
hx : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔
    ∃! a, (↑(shrinkFunctorHomEquiv (shrinkFunctorHomEquiv.symm ⟨x, hx⟩))).IsAmalgamation (shrinkYonedaEquiv a)

Tactic:
simp [Equiv.existsUnique_congr_right]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ IsSheafFor P (ofArrows X π) ↔ Function.Bijective (Arrows.toCompatible P π)

Tactic:
rw [isSheafFor_arrows_iff]
  refine ⟨fun h ↦ ⟨fun x₁ x₂ hx ↦
      (h _ (Arrows.toCompatible P π x₁).property).unique (fun _ ↦ rfl)
        (congr_fun (congr_arg Subtype.val hx.symm)),
      fun ⟨y, hy⟩ ↦ ?_⟩, fun h x hx ↦ ?_⟩
  · obtain ⟨x, hx, _⟩ := h y hy
    exact ⟨x, by ext; apply hx⟩
  · obtain ⟨y, hy⟩ := h.2 ⟨x, hx⟩
    rw [Subtype.ext_iff] at hy
    dsimp at hy
    subst hy
    exact ⟨y, fun _ ↦ rfl, fun y' hy' ↦ h.1 (by ext; apply hy')⟩

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
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom

Tactic:
have := Over.w (f i₂)

Goal state after:
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
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)).hom
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: case refine_2
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 :
  (ConcreteCategory.hom (F.map j.op)) ↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s) ∈ G.obj (op W)
⊢ (ConcreteCategory.hom (F.map i ≫ F.map j.op)) ↑s ∈ G.obj (op W)

Tactic:
comp_apply

Goal state after:
case refine_2
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 :
  (ConcreteCategory.hom (F.map j.op)) ↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s) ∈ G.obj (op W)
⊢ (ConcreteCategory.hom (F.map j.op)) ((ConcreteCategory.hom (F.map i)) ↑s) ∈ G.obj (op W)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom

Tactic:
conv_lhs => rw [← I.fac]

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Subfunctor.range (I.e ≫ I.m).hom ≤ Subfunctor.range I.m.hom
Module: Mathlib.CategoryTheory.Sites.CompatibleSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} 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
P : Cᵒᵖ ⥤ D
⊢ (whiskerRight (J.toPlus P) F ≫ (J.plusCompIso F P).hom) ≫ J.plusMap (J.toPlus (P ⋙ F)) =
    J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))

Tactic:
whiskerRight_toPlus_comp_plusCompIso_hom

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} 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
P : Cᵒᵖ ⥤ D
⊢ J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) = J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F))
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫ (E.π.app k).app (op (W.shape.snd i).Y) ≫ (W.index (F.obj k).obj).snd i

Tactic:
← (E.π.app k).naturality

Goal state after:
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
i : W.shape.R
⊢ S.ι (W.shape.fst i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₁.op ≫ (E.π.app k).app (op i.r.Z) =
    S.ι (W.shape.snd i) ≫ (((Functor.const K).obj E.pt).obj k).map i.r.g₂.op ≫ (E.π.app k).app (op i.r.Z)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_1
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ {T : TopCat} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

Tactic:
intro T

Goal state after:
case mpr.refine_1
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
⊢ (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)

Tactic:
conv_lhs => rw [← Category.comp_id (α.app j)]

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_2
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    c.inl ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      f

Tactic:
intro T

Goal state after:
case mpr.refine_2
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    c.inl ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      f
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_3
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ ∀ {T : TopCat} (f : X ⟶ T) (g : Y ⟶ T),
    c.inr ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      g

Tactic:
intro T

Goal state after:
case mpr.refine_3
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
T : TopCat
⊢ ∀ (f : X ⟶ T) (g : Y ⟶ T),
    c.inr ≫
        ofHom
          {
            toFun := fun x ↦
              if h : x ∈ range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inl) ⋯).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective ⇑(ConcreteCategory.hom c.inr) ⋯).symm ⟨x, ⋯⟩),
            continuous_toFun := ⋯ } =
      g
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ Y ≅ pullback (c.inj i) (c.inj j)

Tactic:
refine hY.uniqueUpToIso ?_
    exact IsInitial.ofCoproductDisjointOfIsColimit hij hc

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this

Tactic:
refine Cocone.ext (Iso.refl c'.pt) ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ (Iso.refl c'.pt).hom =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j
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
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
⊢ x = y → equalizerSieve x y = ⊤

Tactic:
rintro rfl

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
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x : ToType (F.obj X)
⊢ equalizerSieve x x = ⊤
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₁) F ≫ whiskerRight ((sheafToPresheaf J A).map (G₁.map f)) F)

Tactic:
(W _).precomp_iff _ _ (h P₁)

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.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₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝¹ : IsLocallyInjective J f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallyInjective J f₂

Tactic:
subst fac
  exact isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective J f₁ f₂

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

Goal state before:
pp: case refine_2.hd₁
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₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor 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 α
Hc : IsColimit c
⊢ ∀ {T : C} (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      f

Tactic:
intro T

Goal state after:
case refine_2.hd₁
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₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor 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 α
Hc : IsColimit c
T : C
⊢ ∀ (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      f