mathlib-initiative/mathlib-tactics huggingface dataset:
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 G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
j : J
this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (((const J).obj c.pt).obj j)) (c.ι.app j)
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔
    IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)

Tactic:
rw [← IsPullback.paste_vert_iff this _, Category.comp_id]

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
j : J
this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (((const J).obj c.pt).obj j)) (c.ι.app j)
⊢ c'.ι.app j ≫ f = α'.app j ≫ α.app j ≫ c.ι.app j
Module: Mathlib.CategoryTheory.Limits.MonoCoprod

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
a₁ : (pair A B).obj { as := WalkingPair.left }
⊢ ∀ ⦃a₂ : (fun X ↦ X) ((pair A B).obj { as := WalkingPair.left })⦄,
    (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₁ =
        (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₂ →
      a₁ = a₂

Tactic:
a₂

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
⊢ (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₁ =
      (ConcreteCategory.hom (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).inl) a₂ →
    a₁ = a₂
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
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))
j : J
⊢ Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j

Tactic:
rw [← cancel_mono (adj.counit.app <| F.obj j)]

Goal state after:
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))
j : J
⊢ Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case pos
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
e₁ : (↾fun p ↦ (↑p).1) ≫ m = s.inl
e₂ : (↾fun p ↦ (↑p).1) ≫ m = s.inr
x : Z
h✝ : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom m) x = (ConcreteCategory.hom s.inl) (eX.symm ⟨x, ⋯⟩)

Tactic:
rw [← e₁]

Goal state after:
case pos
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
Z : Type u
f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
this :
  ∀ (x : (fun X ↦ X) Z),
    (ConcreteCategory.hom f) x = Sum.inl PUnit.unit ∨ (ConcreteCategory.hom f) x = Sum.inr PUnit.unit
eX : { p // (ConcreteCategory.hom f) p.1 = Sum.inl p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inl PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } :=
  { toFun := fun p ↦ ⟨(↑p).1, ⋯⟩, invFun := fun x ↦ ⟨(x.1, PUnit.unit), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))
m : Z ⟶ s.pt
e₁ : (↾fun p ↦ (↑p).1) ≫ m = s.inl
e₂ : (↾fun p ↦ (↑p).1) ≫ m = s.inr
x : Z
h✝ : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit
⊢ (ConcreteCategory.hom m) x = (ConcreteCategory.hom ((↾fun p ↦ (↑p).1) ≫ m)) (eX.symm ⟨x, ⋯⟩)
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
    constructor
    · refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · exact ⟨val, rfl, fun y h => Sum.inl_injective h.symm⟩
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨TopCat.ofHom ⟨l, ?_⟩, TopCat.ext fun a => (hl a).symm,
        TopCat.isTerminalPUnit.hom_ext _ _,
        fun {l'} h₁ _ => TopCat.ext fun x =>
          hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
      apply (IsEmbedding.inl (X := X') (Y := Y')).isInducing.continuous_iff.mpr
      convert! s.fst.hom.2 using 1
      exact (funext hl).symm
    · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
      intro s
      have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · exact ⟨val, rfl, fun y h => Sum.inr_injective h.symm⟩
      delta ExistsUnique at this
      choose l hl hl' using this
      refine ⟨TopCat.ofHom ⟨l, ?_⟩, TopCat.ext fun a => (hl a).symm,
        TopCat.isTerminalPUnit.hom_ext _ _,
        fun {l'} h₁ _ =>
          TopCat.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩
      apply (IsEmbedding.inr (X := X') (Y := Y')).isInducing.continuous_iff.mpr
      convert! s.fst.hom.2 using 1
      exact (funext hl).symm

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u''
inst✝⁶ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁵ : FinitaryExtensive D
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasPullbacks C
inst✝² : PreservesLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : F.ReflectsIsomorphisms
⊢ FinitaryExtensive C

Tactic:
by
  have : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms
  have : ReflectsColimitsOfShape (Discrete WalkingPair) F :=
    reflectsColimitsOfShape_of_reflectsIsomorphisms
  exact finitaryExtensive_of_preserves_and_reflects F

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

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
⊢ f = g

Tactic:
let : Mono v :=
      mono_of_isPushout_of_mono_left (of_hasPushout (pullback.fst a b) (pullback.snd a b))

Goal state after:
J : Type v'
inst✝⁴ : Category.{u', v'} J
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✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
⊢ f = g
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
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit 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
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, 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' : IsColimit c'
j✝ : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
⊢ Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j

Tactic:
rw [← cancel_mono (adj.counit.app <| F.obj j)]

Goal state after:
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
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit 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
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, 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' : IsColimit c'
j✝ : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
⊢ Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: 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✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := ⋯
this✝ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
S : Cone F
hS : IsLimit S
⊢ IsLimit ((sheafToPresheaf J D).mapCone ((plusPlusSheaf J D).mapCone S))

Tactic:
have : ReflectsLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) (forget D) :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms

Goal state after:
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✝⁶ : (forget D).ReflectsIsomorphisms
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
K : Type w'
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimits (forget D)
inst✝ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
e : K ≌ AsSmall (FinCategory.AsType K) := (FinCategory.equivAsType K).symm.trans AsSmall.equiv
this✝¹ : HasLimitsOfShape (AsSmall (FinCategory.AsType K)) D
this✝ : FinCategory (AsSmall (FinCategory.AsType K))
F : AsSmall (FinCategory.AsType K) ⥤ Cᵒᵖ ⥤ D
S : Cone F
hS : IsLimit S
this : ReflectsLimitsOfShape (AsSmall (FinCategory.AsType K)) (forget D)
⊢ IsLimit ((sheafToPresheaf J D).mapCone ((plusPlusSheaf J D).mapCone S))
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₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
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'
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso := (CatCommSq.iso (G ⋙ F) L₁ L₁ (G' ⋙ F')).symm }
⊢ 𝟭 D₁ ⟶ G' ⋙ F'

Tactic:
exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F')
    (whiskerRight adj.unit L₁)

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

Goal state before:
pp: case mp.right
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
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := ⋯
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr αY f c.inr

Tactic:
rw [← Category.id_comp αY, ← Iso.hom_inv_id_assoc e f]

Goal state after:
case mp.right
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
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} 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
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
⊢ (sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) =
    (J.sheafifyCompIso F P).inv

Tactic:
suffices (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    ⟨(sheafifyCompIso J F P).inv⟩ by
    rw [this]
    rfl

Goal state after:
C : Type u
inst✝¹⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_3
E : Type u_4
inst✝¹⁵ : Category.{v_3, u_3} D
inst✝¹⁴ : Category.{v_4, u_4} 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
FD : D → D → Type u_5
CD : D → Type u_6
FE : E → E → Type u_7
CE : E → Type u_8
inst✝⁷ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁶ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
instCCD : ConcreteCategory D FD
instCCE : ConcreteCategory E FE
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁴ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)
inst✝³ : PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (forget D)
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (forget E)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : (forget E).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
⊢ (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P =
    { hom := (J.sheafifyCompIso F P).inv }
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

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
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ

Tactic:
← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,

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
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ IsLocallySurjective J ((sheafToPresheaf J A).map ((presheafToSheaf J A).map φ)) ↔ IsLocallySurjective J φ