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

Goal state before:
pp: case e'_3
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
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ (ConcreteCategory.hom (Multiequalizer.ι (T.index P) (Cover.Arrow.map i h2))) ((Meq.equiv P T).symm y) =
    ↑y { Y := i.Y, f := i.f, hf := ⋯ }

Tactic:
erw [Meq.equiv_symm_eq_apply]

Goal state after:
case e'_3
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
i : (unop (op S)).shape.L
e : ↑(x.refine h1) i = ↑(y.refine h2) i
e_1✝ : CD (((unop (op S)).index P).left i) = ToType (P.obj (op i.Y))
⊢ ↑y (Cover.Arrow.map i h2) = ↑y { Y := i.Y, f := i.f, hf := ⋯ }
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) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
⊢ ∀ ⦃f₁ : Y₁ ⟶ Y⦄ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : (B H).arrows f₁) (h₂ : (B H).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) (y H f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y H f₂ h₂)

Tactic:
f₁

Goal state after:
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) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
⊢ ∀ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : (B H).arrows f₁) (h₂ : (B H).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) (y H f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y H f₂ h₂)
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
⊢ ∀ (E_1 : Multifork (W.index E.pt)) (i : W.shape.L),
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W E_1) ≫
        (W.multifork E.pt).ι i =
      E_1.ι i

Tactic:
intro 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),
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S) ≫
        (W.multifork E.pt).ι i =
      S.ι i
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
⊢ ∀ (E_1 : Multifork (W.index E.pt)) (m : E_1.pt ⟶ (W.multifork E.pt).pt),
    (∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = E_1.ι i) →
      m = (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W E_1)

Tactic:
intro 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)
⊢ ∀ (m : S.pt ⟶ (W.multifork E.pt).pt),
    (∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i) →
      m = (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W S)
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ IsOpenEmbedding (⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom f)) ↔ IsOpenEmbedding ⇑(ConcreteCategory.hom g)

Tactic:
exact isOpenEmbedding_iff_isIso_comp f g

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
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
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ = η

Tactic:
rw [← Category.assoc, ← plusMap_toPlus]

Goal state after:
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
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.sheafify P ⟶ Q
h : J.toSheafify P ≫ γ = η
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ = η
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (s : PullbackCone f g) →
    { l //
      l ≫ (pullbackCone f g).fst = s.fst ∧
        l ≫ (pullbackCone f g).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (pullbackCone f g).pt},
            m ≫ (pullbackCone f g).fst = s.fst → m ≫ (pullbackCone f g).snd = s.snd → m = l }

Tactic:
intro S

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ { l //
    l ≫ (pullbackCone f g).fst = S.fst ∧
      l ≫ (pullbackCone f g).snd = S.snd ∧
        ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
          m ≫ (pullbackCone f g).fst = S.fst → m ≫ (pullbackCone f g).snd = S.snd → m = l }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
⊢ ∀ (s : Cone (Discrete.functor α)) (m : s.pt ⟶ (piFan α).pt),
    (∀ (j : Discrete ι), m ≫ (piFan α).π.app j = s.π.app j) →
      m = ofHom { toFun := fun s_1 i ↦ (ConcreteCategory.hom (s.π.app { as := i })) s_1, continuous_toFun := ⋯ }

Tactic:
intro S

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
α : ι → TopCat
S : Cone (Discrete.functor α)
⊢ ∀ (m : S.pt ⟶ (piFan α).pt),
    (∀ (j : Discrete ι), m ≫ (piFan α).π.app j = S.π.app j) →
      m = ofHom { toFun := fun s i ↦ (ConcreteCategory.hom (S.π.app { as := i })) s, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
⊢ ∀ (s : Cocone (Discrete.functor β)) (m : (sigmaCofan β).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = s.ι.app j) →
      m = ofHom { toFun := fun s_1 ↦ (ConcreteCategory.hom (s.ι.app { as := s_1.fst })) s_1.snd, continuous_toFun := ⋯ }

Tactic:
intro S

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
⊢ ∀ (m : (sigmaCofan β).pt ⟶ S.pt),
    (∀ (j : Discrete ι), (sigmaCofan β).ι.app j ≫ m = S.ι.app j) →
      m = ofHom { toFun := fun s ↦ (ConcreteCategory.hom (S.ι.app { as := s.fst })) s.snd, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
⊢ ∀ (s : Cone (pair X Y)) (m : s.pt ⟶ (X.prodBinaryFan Y).pt),
    (∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = s.π.app j) →
      m =
        ofHom
          {
            toFun := fun s_1 ↦
              ((ConcreteCategory.hom (BinaryFan.fst s)) s_1, (ConcreteCategory.hom (BinaryFan.snd s)) s_1),
            continuous_toFun := ⋯ }

Tactic:
intro S

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
⊢ ∀ (m : S.pt ⟶ (X.prodBinaryFan Y).pt),
    (∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j) →
      m =
        ofHom
          { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
            continuous_toFun := ⋯ }
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.fst f g))

Tactic:
by
  convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isEmbedding.comp
      (pullback_map_isEmbedding (i₁ := 𝟙 X) f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isEmbedding H
        (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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

Goal state before:
pp: case pos
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
x : ↑c.1
h : x ∈ range ⇑(ConcreteCategory.hom c.inl)
⊢ ContinuousAt
    (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, ⋯⟩))
    x

Tactic:
revert h x

Goal state after:
case pos
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
⊢ ∀ x ∈ range ⇑(ConcreteCategory.hom c.inl),
    ContinuousAt
      (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, ⋯⟩))
      x
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case neg
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
x : ↑c.1
h : x ∉ range ⇑(ConcreteCategory.hom c.inl)
⊢ ContinuousAt
    (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, ⋯⟩))
    x

Tactic:
revert h x

Goal state after:
case neg
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
⊢ ∀ x ∉ range ⇑(ConcreteCategory.hom c.inl),
    ContinuousAt
      (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, ⋯⟩))
      x
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
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k ↦ X ↑k
hc₂ : IsColimit c₂
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i ↦ c.inj (ι i))

Tactic:
let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
  refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
  exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: 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
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPullbacksOfInclusions C
X Y Z : C
f : Z ⟶ X ⨿ Y
this✝ : IsPullback (𝟙 Z) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom
this :
  IsPullback (pullback.fst (f ≫ (coprod.braiding X Y).hom) coprod.inl ≫ 𝟙 Z)
    (pullback.snd (f ≫ (coprod.braiding X Y).hom) coprod.inl) f (coprod.inl ≫ (coprod.braiding Y X).hom)
⊢ HasPullback f coprod.inr

Tactic:
simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc,
    BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this

Goal state after:
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
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPullbacksOfInclusions C
X Y Z : C
f : Z ⟶ X ⨿ Y
this✝ : IsPullback (𝟙 Z) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom
this :
  IsPullback (pullback.fst (f ≫ (coprod.braiding X Y).hom) coprod.inl)
    (pullback.snd (f ≫ (coprod.braiding X Y).hom) coprod.inl) f coprod.inr
⊢ HasPullback f coprod.inr
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.h₂
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
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
refine e₁.trans (Eq.symm ?_); exact h.fac _ _

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
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),
    αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f →
      αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f →
        IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
          IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr

Tactic:
intro X' Y' αX αY f hαX hαY

Goal state after:
case h₁
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
⊢ IsPullback (X'.binaryCofan Y').inl αX f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl ∧
    IsPullback (X'.binaryCofan Y').inr αY f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α),
    c.inj i ≫ (Iso.refl c.pt).hom ≫ (PullbackCone.mk (𝟙 Y) f ⋯).snd =
      PullbackCone.snd (limit.cone (cospan f (π i))) ≫ (Cofan.mk X π).inj i

Tactic:
simp [pullback.condition, c]

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

Goal state before:
pp: case refine_1
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 t
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 X)) (j : K),
    liftToPlusObjLimitObj F (unop X) s ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j =
      s.π.app j

Tactic:
intro S

Goal state after:
case refine_1
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 t
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 X)
⊢ ∀ (j : K),
    liftToPlusObjLimitObj F (unop X) S ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j =
      S.π.app j
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: case refine_2
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 t
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 X))
    (m : s.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt),
    (∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = s.π.app j) →
      m = liftToPlusObjLimitObj F (unop X) s

Tactic:
intro S

Goal state after:
case refine_2
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 t
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 X)
⊢ ∀ (m : S.pt ⟶ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).pt),
    (∀ (j : K), m ≫ ((J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj X).mapCone (limit.cone F)).π.app j = S.π.app j) →
      m = liftToPlusObjLimitObj F (unop X) S