mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
this : HasExt C := HasExt.standard C
⊢ Injective X ↔ HasInjectiveDimensionLT X 1

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ injective_iff_subsingleton_ext_one.2
    (HasInjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x.comp (Ext.mk₀ (h.i ≫ h.r)) ⋯ = 0

Tactic:
← Ext.mk₀_comp_mk₀,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext T X i
⊢ x.comp ((Ext.mk₀ h.i).comp (Ext.mk₀ h.r) ⋯) ⋯ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } = s.ι.app j

Tactic:
ext1 X
    exact (hc X).fac ((evaluation R X).mapCocone s) j

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)

Tactic:
by
  rw [← Functor.map_comp, prod_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)

Tactic:
by
  rw [← Functor.map_comp, prod_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.leftAdjointObjIsDefined = ⊤
X : C
⊢ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
simp only [← leftAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]

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

Goal state before:
pp: case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ Presieve.ofArrows P p₁ = Presieve.ofArrows (P ∘ a) fun i ↦ p₁ (a i)

pp: case convert_4
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (P ∘ a) fun i ↦ p₁ (a i)) ∈ J.coverings Y

Tactic:
· refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩
    exact .mk' (Sum.inr ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

Goal state after:
case convert_4
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (P ∘ a) fun i ↦ p₁ (a i)) ∈ J.coverings Y
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
J : Precoverage E
X : C
R : Presieve X
⊢ R ∈ (comap (F ⋙ G) J).coverings X ↔ R ∈ (comap F (comap G J)).coverings X

Tactic:
obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
F : C ⥤ D
G : D ⥤ E
J : Precoverage E
X : C
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ (comap (F ⋙ G) J).coverings X ↔ Presieve.ofArrows Y f ∈ (comap F (comap G J)).coverings X
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X Y : C
f : Y ⟶ X
x✝ : IsIso f
⊢ Presieve.singleton f ∈ sInf ((fun J ↦ J.coverings) '' T) X

Tactic:
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists,
        Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X Y : C
f : Y ⟶ X
x✝ : IsIso f
⊢ ∀ i ∈ T, Presieve.singleton f ∈ i.coverings X
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
W : C
h : W ⟶ Y
⊢ pullbackArrows f (singleton g) h → singleton (pullback.snd g f) h

Tactic:
rintro ⟨W, _, _, _⟩

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝¹ Z : C
f : Y✝¹ ⟶ X
g : Z ⟶ X
inst✝ : HasPullback g f
Y✝ Y : C
⊢ singleton (pullback.snd g f) (pullback.snd g f)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal

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
F : C ⥤ D
hF : (X : C) → IsTerminal (F.obj X)
⊢ IsTerminal F

Tactic:
by
  refine evaluationJointlyReflectsLimits _
    fun X ↦ IsLimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)
  exact Cone.ext (Iso.refl _)

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ hf₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
← pullback.lift_fst _ _ comm,

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map (pullback.lift g₁ g₂ comm ≫ pullback.fst f₁ f₂).op)) (x f₁ hf₁) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf

Tactic:
← q

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t =
    (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) f hf
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : ∃ t, x.IsAmalgamation t
⊢ x.Compatible

Tactic:
obtain ⟨t, ht⟩ := h
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm
  rw [← ht _ h₁, ← ht _ h₂, ← comp_apply, ← Functor.map_comp, ← op_comp, comm]
  simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf

Tactic:
← q

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) f hf
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
    x
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
← q

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
    x
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t =
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) i
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
x : unop (op X)
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    S.arrows f →
      (ConcreteCategory.hom (P.map f.op)) ((ConcreteCategory.hom y) x) =
        (ConcreteCategory.hom (P.map f.op))
          ((ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x)

Tactic:
intro Y' f hf

Goal state after:
case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
x : unop (op X)
Y' : C
f : Y' ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) ((ConcreteCategory.hom y) x) =
    (ConcreteCategory.hom (P.map f.op))
      ((ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
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
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map gi.op)) (x i) = (ConcreteCategory.hom (P.map gj.op)) (x j)

Tactic:
← pullback.lift_fst _ _ comm,

Goal state after:
case refine_2
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
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map (pullback.lift gi gj comm ≫ pullback.fst (π i) (π j)).op)) (x i) =
    (ConcreteCategory.hom (P.map gj.op)) (x j)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
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 : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left✝ : ((fun T k x ↦ Sieve.pullback k S) W l hl).arrows k
comm : k ≫ l = g ≫ f
⊢ R.arrows (k ≫ l)

Tactic:
simp [hl]

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)
i : W.shape.L
k : K
⊢ ((isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
        (E.π.app k).app (op X)) ≫
      (F.obj k).obj.map i.f.op =
    S.ι i ≫ (E.π.app k).app (op i.Y)

Tactic:
(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac
        (multiforkEvaluationCone F E X W S)

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
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)
i : W.shape.L
k : K
⊢ (multiforkEvaluationCone F E X W S).π.app k ≫ (F.obj k).obj.map i.f.op = S.ι i ≫ (E.π.app k).app (op i.Y)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
            (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯ ≫
          colimit.ι (J.diagram Q (unop X)) W) ≫
      (J.plusCompIso F Q).hom.app X =
    ((J.diagramCompIso F P (unop X)).hom.app W ≫
        Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯) ≫
      colimit.ι (J.diagram (Q ⋙ F) (unop X)) W

Tactic:
simp only [Functor.map_comp, Category.assoc, ι_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) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map
        (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P))
          (fun x ↦ Multiequalizer.ι ((unop W).index P) x ≫ η.app (op x.Y)) ⋯) ≫
      (J.diagramCompIso F Q (unop X)).hom.app W ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W =
    (J.diagramCompIso F P (unop X)).hom.app W ≫
      Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F)))
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ F.map (η.app (op x.Y))) ⋯ ≫
        colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩

Tactic:
apply Continuous.subtype_mk

Goal state after:
J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun x ↦ (↑x, Exists.choose ⋯)
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
rw [pullback_snd_range]

Goal state after:
X Y S : TopCat
f : X ⟶ S
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
H : Set.range ⇑(ConcreteCategory.hom g) ⊆ Set.range ⇑(ConcreteCategory.hom f)
x : ↑Y
⊢ x ∈ {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
j : J
⊢ Gr.map (c'.ι.app j ≫ f) = (Gr.map (α'.app j) ≫ c.ι.app j) ≫ adj.unit.app c.pt

Tactic:
← hc''

Goal state after:
case refine_1
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
j : J
⊢ Gr.map (α.app j ≫ Gl.map (c.ι.app j)) = (Gr.map (α'.app j) ≫ c.ι.app j) ≫ adj.unit.app c.pt
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.refine_3.none
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 : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ ({ app := fun X_1 ↦ Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY, naturality := ⋯ } ≫
          (PushoutCocone.mk h i ⋯).ι).app
      none =
    (w.cocone.ι ≫ (Functor.const WalkingSpan).map αZ).app none

Tactic:
simp [hh.w, hf.w_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
⊢ IsPullback (pullback.fst αY c.inr ≫ i') (pullback.snd αY c.inr) αZ (c.inr ≫ i)

Tactic:
exact hc₃

Goal state after: