mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift (of ⋙q Φ)

Tactic:
fapply Prefunctor.ext

Goal state after:
case h_obj
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X

case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))
Module: Mathlib.CategoryTheory.Products.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.1 ∧ IsIso f.2

Tactic:
constructor
  · rintro ⟨g, hfg, hgf⟩
    rcases Prod.hom_ext_iff.1 hfg with ⟨hfg₁, hfg₂⟩
    rcases Prod.hom_ext_iff.1 hgf with ⟨hgf₁, hgf₂⟩
    exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
  · rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
    dsimp at hfg₁ hgf₁ hfg₂ hgf₂
    refine ⟨⟨(g₁, g₂), by aesop_cat, by aesop_cat⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.unop.op = f

Tactic:
by (ext; rfl)

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ f.op.unop = f

Tactic:
by (ext; rfl)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), X = Y

Tactic:
rintro ⟨_⟩ ⟨_⟩ ⟨f⟩
    obtain rfl := obj_ext_of_isDiscrete f
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : D ⥤ E
X : D
⊢ (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)

Tactic:
dsimp [invFunIdAssoc]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G G' : C ≌ D
i : G.functor ≅ G'.functor
X : C
⊢ i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse.hom.app X = i.hom.app X

Tactic:
simp [← NatTrans.naturality]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝ ≫ x✝¹)

Tactic:
by
    rw [sInf_iff] at hf ⊢
    exact fun _ hW' ↦ (h _ hW').postcomp _ hi _ (hf _ hW')

Goal state after:
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
⊢ (refl X).conj f = f

Tactic:
by
  rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
      P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) =
    𝟙 s.pt

Tactic:
by
      apply hom_ext P; intro j
      dsimp [w']
      simp only [Limits.Cone.whisker_π, Limits.Cone.postcompose_obj_π, fac, whiskerLeft_app,
        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
      rw [counit_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
      simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫ G.map ((e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))))

Tactic:
rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| f ≫ f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)

Tactic:
Category.comp_id,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (k ≫ tX.from j') = F.map (tX.from j)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePushoutShape J
a b : x✝¹ ⟶ x✝
⊢ a = b

Tactic:
casesm* WidePushoutShape _, (_ : WidePushoutShape _) ⟶ (_ : WidePushoutShape _)

Goal state after:
case none.none.id.id
J : Type w
⊢ Hom.id none = Hom.id none

case none.some.init.init
J : Type w
b : J
⊢ Hom.init b = Hom.init b

case some.some.id.id
J : Type w
x✝ : J
⊢ Hom.id (some x✝) = Hom.id (some x✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasCoproduct (g i)
inst✝ : HasCoproduct fun i ↦ ∐ g i
⊢ ∀ (t : Cofan fun p ↦ g p.fst p.snd)
    (m : (Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).pt ⟶ t.pt),
    (∀ (j : (i : ι) × f i),
        (Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).inj j ≫ m =
          t.inj j) →
      m = Sigma.desc fun b ↦ Sigma.desc fun c ↦ t.inj ⟨b, c⟩

Tactic:
by intro s (m : (∐ fun i ↦ ∐ g i) ⟶ _) w; aesop_cat (add norm simp Sigma.forall)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
j : Discrete β
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        j =
    s.π.app j

Tactic:
by
        obtain rfl := Subsingleton.elim j default
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ f₁ ≫ i₁ ≫ inl g₁ g₂ = f₂ ≫ i₂ ≫ inr g₁ g₂

Tactic:
simp only [reassoc_of% eq₁, reassoc_of% eq₂, condition]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ : T
f✝ g : Under X✝
φ : f✝ ⟶ g
F✝ : T ⥤ D
X : T
F : T ⥤ D
G : D ⥤ T
a : F ⊣ G
x✝¹ x✝ : Under (F.obj ((𝟭 T).obj X))
f : x✝¹ ⟶ x✝
⊢ Hom.right (((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x✝.right) ⋯) =
    Hom.right (homMk (a.counit.app x✝¹.right) ⋯ ≫ (𝟭 (Under (F.obj ((𝟭 T).obj X)))).map f)

Tactic:
exact (a.counit_naturality f.right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ (s.fst ≫ 𝟙 X) ≫ f = s.snd ≫ f

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ s.fst ≫ f = s.snd ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
⊢ t.fst ≫ x ≫ h = t.snd ≫ y ≫ h

Tactic:
rw [← Category.assoc, ← Category.assoc]
      apply congrArg (· ≫ h) t.condition

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).1

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).2

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).1.left

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).2.left

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ Arrow.Hom.right sq
⊢ (image.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

Tactic:
simp [map_ι]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ ((imageMap sq1).map ≫ (imageMap sq2).map) ≫ image.ι h.hom = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)

Tactic:
rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Arrow.comp_right]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (F.mapBiprod X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)

Tactic:
by
  rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (whiskerEquiv e w).inv = lift fun j ↦ π g (e j) ≫ (w j).hom

Tactic:
simp only [whiskerEquiv_inv]
  ext j k
  by_cases h : k = e j
  · subst h
    simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
      lift_π, bicone_ι_π_self_assoc]
  · simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · exact h
    · rintro rfl
      simp at h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
j : J
⊢ ((s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯)) ≫ π f j = s.ι ≫ π f j

Tactic:
KernelFork.ι_ofι,

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
j : J
⊢ ((s.ι ≫ toSubtype f fun j ↦ j ≠ i) ≫ fromSubtype f fun j ↦ j ≠ i) ≫ π f j = s.ι ≫ π f j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : BinaryBicone X Y
x✝ : b.toBicone.IsBilimit
h : IsLimit b.toBicone.toCone
h' : IsColimit b.toBicone.toCocone
⊢ (fun h ↦ { isLimit := b.toBiconeIsLimit.symm h.isLimit, isColimit := b.toBiconeIsColimit.symm h.isColimit })
      ((fun h ↦ { isLimit := b.toBiconeIsLimit h.isLimit, isColimit := b.toBiconeIsColimit h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
dsimp only

Goal state after:
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : BinaryBicone X Y
x✝ : b.toBicone.IsBilimit
h : IsLimit b.toBicone.toCone
h' : IsColimit b.toBicone.toCocone
⊢ { isLimit := b.toBiconeIsLimit.symm (b.toBiconeIsLimit h),
      isColimit := b.toBiconeIsColimit.symm (b.toBiconeIsColimit h') } =
    { isLimit := h, isColimit := h' }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : BinaryBicone X Y
x✝ : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ (fun h ↦ { isLimit := b.toBiconeIsLimit h.isLimit, isColimit := b.toBiconeIsColimit h.isColimit })
      ((fun h ↦ { isLimit := b.toBiconeIsLimit.symm h.isLimit, isColimit := b.toBiconeIsColimit.symm h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
dsimp only

Goal state after:
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : BinaryBicone X Y
x✝ : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ { isLimit := b.toBiconeIsLimit (b.toBiconeIsLimit.symm h),
      isColimit := b.toBiconeIsColimit (b.toBiconeIsColimit.symm h') } =
    { isLimit := h, isColimit := h' }
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι
⊢ m = (m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯)) ≫ toSubtype f fun j ↦ j ≠ i

Tactic:
KernelFork.ι_ofι,

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt
hm : m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι
⊢ m = (m ≫ fromSubtype f fun j ↦ j ≠ i) ≫ toSubtype f fun j ↦ j ≠ i
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
⊢ (fun h ↦
        { isLimit := b.toBinaryBiconeIsLimit.symm h.isLimit, isColimit := b.toBinaryBiconeIsColimit.symm h.isColimit })
      ((fun h ↦ { isLimit := b.toBinaryBiconeIsLimit h.isLimit, isColimit := b.toBinaryBiconeIsColimit h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
dsimp only

Goal state after:
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
⊢ { isLimit := b.toBinaryBiconeIsLimit.symm (b.toBinaryBiconeIsLimit h),
      isColimit := b.toBinaryBiconeIsColimit.symm (b.toBinaryBiconeIsColimit h') } =
    { isLimit := h, isColimit := h' }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ (fun h ↦ { isLimit := b.toBinaryBiconeIsLimit h.isLimit, isColimit := b.toBinaryBiconeIsColimit h.isColimit })
      ((fun h ↦
          { isLimit := b.toBinaryBiconeIsLimit.symm h.isLimit,
            isColimit := b.toBinaryBiconeIsColimit.symm h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
dsimp only

Goal state after:
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ { isLimit := b.toBinaryBiconeIsLimit (b.toBinaryBiconeIsLimit.symm h),
      isColimit := b.toBinaryBiconeIsColimit (b.toBinaryBiconeIsColimit.symm h') } =
    { isLimit := h, isColimit := h' }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_1.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

pp: case refine_1.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

pp: case refine_2.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

pp: case refine_2.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (let c' := CokernelCofork.ofπ (Cofork.π c) ⋯;
      let i' := isCokernelEpiComp i (retraction f) ⋯;
      let i'' := isColimitCoforkOfCokernelCofork i';
      (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_) ≫
      retraction f =
    0

Tactic:
dsimp only

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (splitEpiOfIdempotentOfIsColimitCofork C ⋯
          (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))).section_ ≫
      retraction f =
    0