mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y : CD (P.obj (op X))
h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ x = y

Tactic:
eq_mk_iff_exists

Goal state after:
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
x y : CD (P.obj (op X))
h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case hS
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
← Sieve.pullback_comp

Goal state after:
case hS
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows
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)
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
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := ⋯
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := ⋯
⊢ Meq.mk S (mk w) = s

Tactic:
ext I

Goal state after:
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)
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
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
B : J.Cover X := S.bind T
Z : B.Arrow → C
e1 : (I : B.Arrow) → I.Y ⟶ Z I
e2 : (I : B.Arrow) → Z I ⟶ X
he2 : ∀ (I : B.Arrow), (↑S).arrows (e2 I)
h✝ :
  ∀ (I : B.Arrow),
    (fun x x_1 h ↦ ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) x x_1 h).arrows) (Z I) (e2 I) ⋯ (e1 I)
a✝ : ∀ (I : B.Arrow), e1 I ≫ e2 I = I.f
w : Meq P B := meqOfSep P hsep X S s T t ht
I : S.Arrow
⊢ ↑(Meq.mk S (mk w)) I = ↑s I
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
dsimp [colimitLimitToLimitColimit]
  simp

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

Goal state before:
pp: case neg.hf
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
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (Subtype.map (fun a ↦ a) this)

Tactic:
rw [IsEmbedding.subtypeVal.isInducing.continuous_iff]

Goal state after:
case neg.hf
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
this : ∀ a ∉ range ⇑(ConcreteCategory.hom c.inl), a ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ Continuous (Subtype.val ∘ Subtype.map (fun a ↦ a) this)
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
⊢ ∃ c x, Mono c.inl

Tactic:
refine ⟨BinaryCofan.mk (↾(Sum.inl : A → A ⊕ B))
      (↾Sum.inr), ?_, ?_⟩
    · exact BinaryCofan.IsColimit.mk _
        (fun f₁ f₂ => ↾fun x => by
          rcases x with x | x
          exacts [f₁ x, f₂ x])
        (fun f₁ f₂ => by rfl)
        (fun f₁ f₂ => by rfl)
        (fun f₁ f₂ m h₁ h₂ => by
          ext x
          rcases x with x | x
          · exact ConcreteCategory.congr_hom h₁ x
          · exact ConcreteCategory.congr_hom h₂ x)
    · rw [mono_iff_injective]
      intro a₁ a₂ h
      simpa using h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoCoprod C
I : Type u_2
X : I → C
c : Cofan X
h : IsColimit c
i : I
inst✝ : HasCoproduct fun k ↦ X ↑k
⊢ Mono (c.inj i)

Tactic:
by
  let ι : Unit → I := fun _ ↦ i
  have hι : Function.Injective ι := fun _ _ _ ↦ rfl
  exact mono_of_injective X ι hι c (Cofan.mk (X i) (fun _ ↦ 𝟙 _)) h
    (Cofan.IsColimit.mk _ (fun s => s.inj ()))

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H : IsVanKampenColimit c₀
⊢ ∀ {X Y : C} (c : BinaryCofan X Y) (a : IsColimit c), IsVanKampenColimit c

Tactic:
BinaryCofan.isVanKampen_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbacksOfInclusions C
T : C
HT : IsTerminal T
c₀ : BinaryCofan T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (f : c'.pt ⟶ c₀.pt),
    αX ≫ c₀.inl = c'.inl ≫ f →
      αY ≫ c₀.inr = c'.inr ≫ f →
        (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c₀.inl ∧ IsPullback c'.inr αY f c₀.inr)
⊢ ∀ {X Y : C} (c : BinaryCofan X Y) (a : IsColimit c) {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inl
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr y

Tactic:
apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

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

Goal state before:
pp: case mp.refine_2
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
    iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
intro m e₁ e₂

Goal state after:
case mp.refine_2
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inl
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑X'
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr y

Tactic:
apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm

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

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j))
      ((ConcreteCategory.hom (colimitLimitToLimitColimit F))
        ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k''))
          (id
            (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
              (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) ⋯)))) =
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x

Tactic:
simp only [comp_obj, colim_obj, lim_obj, Bifunctor.map_id_comp, id_eq, ← comp_apply, assoc,
        ι_colimitLimitToLimitColimit_π, curry_obj_obj_obj, swap_obj]

Goal state after:
case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ (ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj k'') j ≫ colimit.ι ((curry.obj F).obj j) k''))
      (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
        (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j) ≫ F.map (𝟙 j ×ₘ gf (𝟙 j)) ≫ F.map (𝟙 j ×ₘ i (𝟙 j)))) (y j))
        ⋯) =
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ 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
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ colimit.ι (J.diagram (limit F) (unop (op X))) j ≫ (J.plusMap (limit.π F k)).app (op X) =
    colimit.ι (J.diagram (limit F) (unop (op X))) j ≫
      (HasColimit.isoOfNatIso
            ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
              (limit.isLimit (F ⋙ J.diagramFunctor D X)))).hom ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫
          (HasLimit.isoOfNatIso
                (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                    ⋯).symm).inv ≫
            limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k

Tactic:
dsimp [plusMap]

Goal state after:
case e_a
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ 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
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ colimit.ι (J.diagram (limit F) X) j ≫ colimMap (J.diagramNatTrans (limit.π F k) X) =
    colimit.ι (J.diagram (limit F) X) j ≫
      (HasColimit.isoOfNatIso
            ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
              (limit.isLimit (F ⋙ J.diagramFunctor D X)))).hom ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫
          (HasLimit.isoOfNatIso
                (NatIso.ofComponents (fun k ↦ colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                    ⋯).symm).inv ≫
            limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso := (CatCommSq.iso (F ⋙ G) L₂ L₂ (F' ⋙ G')).symm }
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso_inv_app,
    whiskerRight_app, Functor.rightUnitor_inv_app, comp_id, assoc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
⊢ IsVanKampenColimit c

Tactic:
BinaryCofan.isVanKampen_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
⊢ ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective fun g_1 ↦ g ≫ g_1

Tactic:
← Function.Bijective.of_comp_iff' (hf Z hZ)

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.isLocal f
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective ((fun g ↦ f ≫ g) ∘ fun g_1 ↦ g ≫ g_1)
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 : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
eq_mk_iff_exists

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.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✝ : IsLocallySurjective J f₁
⊢ IsLocallySurjective J f₃ ↔ IsLocallySurjective J f₂

Tactic:
by
  constructor
  · intro
    exact isLocallySurjective_of_isLocallySurjective_fac J fac
  · intro
    rw [← fac]
    infer_instance

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
P : Cᵒᵖ ⥤ Type (max u v)
U✝ : C
S : J.Cover U✝
x : Meq P S
Y : C
f : Y ⟶ U✝
hf : (↑S).arrows f
⊢ Plus.mk (Meq.mk ⊤ (↑x { Y := Y, f := f, hf := hf })) = Plus.mk (x.pullback f)

Tactic:
eq_mk_iff_exists

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
P : Cᵒᵖ ⥤ Type (max u v)
U✝ : C
S : J.Cover U✝
x : Meq P S
Y : C
f : Y ⟶ U✝
hf : (↑S).arrows f
⊢ ∃ W h1 h2, (Meq.mk ⊤ (↑x { Y := Y, f := f, hf := hf })).refine h1 = (x.pullback f).refine h2