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

Goal state before:
pp: case fac_left
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 } := ⋯
eY : { p // (ConcreteCategory.hom f) p.1 = Sum.inr p.2 } ≃ { x // (ConcreteCategory.hom f) x = Sum.inr PUnit.unit } := ⋯
⊢ ∀ (s : BinaryCofan (Types.PullbackObj f (↾Sum.inl)) (Types.PullbackObj f (↾Sum.inr))),
    ((↾fun p ↦ (↑p).1) ≫
        ↾fun x ↦
          if h : (ConcreteCategory.hom f) x = Sum.inl PUnit.unit then (ConcreteCategory.hom s.inl) (eX.symm ⟨x, h⟩)
          else (ConcreteCategory.hom s.inr) (eY.symm ⟨x, ⋯⟩)) =
      s.inl

Tactic:
intro s
      ext ⟨⟨x, ⟨⟩⟩, _⟩
      dsimp
      split_ifs with h <;> tauto

Goal state after:
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.{v, v, 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
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j ↦ pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
cf : (Cocone.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' :=
  {
    hom :=
      pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv,
    w := ⋯ }
this✝ :
  cf.hom ≫
      (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫
        pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt =
    𝟙 ((Cocone.precompose β.hom).obj c').pt
this : IsIso cf
⊢ whiskerRight α' Gr ≫ c.ι = c''.ι ≫ (const J).map (pullback.snd (Gr.map f) (adj.unit.app c.pt))

Tactic:
ext j
    dsimp [c'']
    simp only [pullback.lift_snd]

Goal state after:
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 α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
⊢ α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))

Tactic:
rw [hα'']

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 α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
⊢ α.app j = β.inv.app j ≫ adj.counit.app (F'.1 j) ≫ α.app j
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)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫
      (limit.π (F ⋙ J.diagramFunctor D X) k).app j ≫
        (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫
          (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom

Tactic:
simp_rw [← Category.assoc, ← NatTrans.comp_app]

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)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x ↦ Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    ((limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F)) ≫
              limit.π (F ⋙ J.diagramFunctor D X) k).app
          j ≫
        (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k) ≫
      (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
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'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
        G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app (G.obj X₁)) ≫
          (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
            L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
← G'.map_comp_assoc,

Goal state after:
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'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app (G.obj X₁)) ≫
        (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
          L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
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'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
      G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app (G.obj X₁)) ≫
        (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
          L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)

Tactic:
← G'.map_comp_assoc,

Goal state after:
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'
X₁ : C₁
eq : G.map (adj.unit.app X₁) ≫ adj.counit.app (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map
        ((L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) ≫
          (CatCommSq.iso F L₂ L₁ F').inv.app (G.obj X₁)) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj (G.obj X₁)) ≫
        L₂.map (adj.counit.app (G.obj X₁)) ≫ (𝟭 D₂).map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) =
    (NatTrans.id (𝟭 D₁ ⋙ G')).app (L₁.obj X₁)
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.IsLocallyInjective ((presheafToSheaf J A).map φ) ↔ IsLocallyInjective J φ

Tactic:
by
  rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]

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

Goal state before:
pp: case refine_2.hd₁
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
⊢ ∀ {T : C} (f : F' 0 ⟶ T) (g : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
        Hc.desc
          (Cofan.mk T fun i ↦
            Fin.cases f (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ g) i) =
      f

Tactic:
intro T f₁ f₂
      simp only [Discrete.functor_obj, pair_obj_left, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inl, IsColimit.fac, Cofan.mk_pt, Cofan.mk_ι_app,
        Fin.cases_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y 1)
E✝ X✝ : C
f : X ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
φ : X ⟶ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.X₂
hφ :
  (Ext.homEquiv₀.symm φ).comp (Ext.mk₀ { X₁ := kernel g, X₂ := E✝, X₃ := X✝, f := kernel.ι g, g := g, zero := ⋯ }.g) ⋯ =
    Ext.mk₀ f
⊢ Ext.homEquiv₀.symm (φ ≫ g) = Ext.homEquiv₀.symm f

Tactic:
simpa using hφ

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
inst✝ : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
⊢ projectiveDimension M ≤ ⊥ ↔ projectiveDimension N ≤ ⊥

Tactic:
simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr

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

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.left Bicone.left
⊢ Decidable (left_id = g)

Tactic:
cases g

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.right Bicone.right
⊢ Decidable (right_id = g)

Tactic:
cases g

Goal state after:
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.left (Bicone.diagram j✝)
⊢ Decidable (left j✝ = g)

Tactic:
cases g

Goal state after:
case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.right (Bicone.diagram j✝)
⊢ Decidable (right j✝ = g)

Tactic:
cases g

Goal state after:
case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram j✝) (Bicone.diagram k✝)
⊢ Decidable (diagram f✝ = g)

Tactic:
cases g

Goal state after:
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

Tactic:
cases g

Goal state after:
case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom J Bicone.left (Bicone.diagram k✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

Tactic:
cases g

Goal state after:
case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom J Bicone.right (Bicone.diagram k✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.left ⟶ Y✝
⊢ (BiconeHom.left_id ≫ g) ≫ h = BiconeHom.left_id ≫ g ≫ h

Tactic:
cases g

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.left ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h = BiconeHom.left_id ≫ BiconeHom.left_id ≫ h

case left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ h = BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.right ⟶ Y✝
⊢ (BiconeHom.right_id ≫ g) ≫ h = BiconeHom.right_id ≫ g ≫ h

Tactic:
cases g

Goal state after:
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.right ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h = BiconeHom.right_id ≫ BiconeHom.right_id ≫ h

case right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ h = BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.left j✝ ≫ g) ≫ h = BiconeHom.left j✝ ≫ g ≫ h

Tactic:
cases g

Goal state after:
case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.left j✝ ≫ BiconeHom.diagram f✝ ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.right j✝ ≫ g) ≫ h = BiconeHom.right j✝ ≫ g ≫ h

Tactic:
cases g

Goal state after:
case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.right j✝ ≫ BiconeHom.diagram f✝ ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Y✝
⊢ (BiconeHom.diagram f✝ ≫ g) ≫ h = BiconeHom.diagram f✝ ≫ g ≫ h

Tactic:
cases g

Goal state after:
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝ ≫ h
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
g : E.Hom F
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.s₀ = g.s₀
hh : ∀ (i : E.I₀), { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i = g.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
s₀✝¹ : E.I₀ → F.I₀
h₀✝¹ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝¹ i)
w₀✝¹ : ∀ (i : E.I₀), h₀✝¹ i ≫ F.f (s₀✝¹ i) = E.f i
s₀✝ : E.I₀ → F.I₀
h₀✝ : (i : E.I₀) → E.X i ⟶ F.X (s₀✝ i)
w₀✝ : ∀ (i : E.I₀), h₀✝ i ≫ F.f (s₀✝ i) = E.f i
hs : { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.s₀ = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.s₀
hh : ∀ (i : E.I₀), { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ }.h₀ i = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }.h₀ i ≫ eqToHom ⋯
⊢ { s₀ := s₀✝¹, h₀ := h₀✝¹, w₀ := w₀✝¹ } = { s₀ := s₀✝, h₀ := h₀✝, w₀ := w₀✝ }
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (Sieve.functorPushforward F S).arrows

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

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (Sieve.functorPushforward F (Sieve.ofArrows Y f)).arrows
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ ((iWV ≫ G.map iVZ) ≫ iZY) ≫ iYX = iWV ≫ G.map iVX

Tactic:
simp [e]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
this : ∀ (X : Dᵒᵖ), IsIso ((sheafHom i.hom).app X)
⊢ IsIso (sheafHom i.hom)

Tactic:
by apply NatIso.isIso_of_isIso_app

Goal state after: