mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
⊢ ∀ (s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }) (j : J),
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫
        h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } =
      s.ι.app j

Tactic:
intro s j

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
j : J
⊢ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫
      h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } =
    s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
⊢ IsIso (α.app c.pt)

Tactic:
let e := IsColimit.coconePointsIsoOfNatIso
    (isColimitOfPreserves L hc) (isColimitOfPreserves L' hc) (asIso (whiskerLeft K α))

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
⊢ IsIso (α.app c.pt)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3✝ : L.obj c.pt = (L.mapCocone c).pt
e_4✝ : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ (K.whiskerLeft α).app j ≫ (L'.mapCocone c).ι.app j = α.app (K.obj j) ≫ L'.map (c.ι.app j)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), f ≫ (x + y) = f ≫ x + f ≫ y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (m : R) (x : Y ⟶ Z), f ≫ (m • x) = (RingHom.id R) m • f ≫ x

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (x + y) ≫ g = x ≫ g + y ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (m : R) (x : X ⟶ Y), (m • x) ≫ g = (RingHom.id R) m • x ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝¹ y✝ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ (leftComp S Z (x✝¹ + y✝)) x✝ = (leftComp S Z x✝¹ + leftComp S Z y✝) x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
m✝ : S
x✝¹ : X ⟶ Y
x✝ : Y ⟶ Z
⊢ (leftComp S Z (m✝ • x✝¹)) x✝ = ((RingHom.id S) m✝ • leftComp S Z x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
g : Q ⟶ R
f f' : P ⟶ Q
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso g
⊢ f ≫ g = 0 ↔ f = 0

Tactic:
rw [← IsIso.eq_comp_inv, Limits.zero_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteLimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasLimitsOfShape J C

Tactic:
apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
  apply HasFiniteLimits.out

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteColimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasColimitsOfShape J C

Tactic:
by
  refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
  apply HasFiniteColimits.out

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
⊢ HasColimitsOfShape J C

Tactic:
have l : @Equivalence J (ULiftHom (ULift J)) hJ
                           (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
      @ULiftHomULiftCategory.equiv J hJ

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.47, 0} J)
⊢ HasColimitsOfShape J C
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ zero ∈ [zero, one].toFinset

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
⊢ one ∈ [zero, one].toFinset

Tactic:
simp

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

Goal state before:
pp: case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn none (Option.casesOn none {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = none then ⋯.mpr {Hom.id none} else ∅

Tactic:
simp

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

Goal state before:
pp: case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (some val✝) (Option.casesOn (some val✝) {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = some val✝ then ⋯.mpr {Hom.id (some val✝)} else ∅

Tactic:
simp

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

Goal state before:
pp: case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅

Tactic:
simp

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

Goal state before:
pp: case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn none (Option.casesOn none {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = none then ⋯.mpr {Hom.id none} else ∅

Tactic:
simp

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

Goal state before:
pp: case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (some val✝) (Option.casesOn (some val✝) {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = some val✝ then ⋯.mpr {Hom.id (some val✝)} else ∅

Tactic:
simp

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

Goal state before:
pp: case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn none (Option.casesOn (some j✝) {Hom.id none} fun j' ↦ {Hom.init j'}) fun j ↦
      if h : some j = some j✝ then ⋯.mpr {Hom.id (some j✝)} else ∅

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.left ∈ {WalkingPair.left, WalkingPair.right}

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.right ∈ {WalkingPair.left, WalkingPair.right}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ ∀ {X Y : C} (x : X ≅ Y), ⊤ X → ⊤ Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
⊢ (⨆ a, P a) X ↔ ∃ a, P a X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X : C
inst✝ : ∀ (a : α), (P a).IsClosedUnderIsomorphisms
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : (⨅ a, P a) X✝
⊢ (⨅ a, P a) Y✝

Tactic:
by
    simp only [iInf_apply, iInf_Prop_eq] at h ⊢
    intro a
    exact (P a).prop_of_iso e (h a)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
hY : P Y
e : X ≅ Y
⊢ ⊤ { obj := Y, property := hY }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ s.π.app one = 0

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app
      { as := WalkingPair.left } =
    (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      (BinaryFan.mk (G.map f) (G.map g)).π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app
      { as := WalkingPair.right } =
    (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      (BinaryFan.mk (G.map f) (G.map g)).π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    (BinaryCofan.mk (G.map f) (G.map g)).ι.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    (BinaryCofan.mk (G.map f) (G.map g)).ι.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : KernelFork f
lift : (s : KernelFork f) → s.pt ⟶ t.pt
fac : ∀ (s : KernelFork f), lift s ≫ Fork.ι t = Fork.ι s
uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), m ≫ Fork.ι t = Fork.ι s → m = lift s
s : Cone (parallelPair f 0)
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
⊢ hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c ≫ e.hom = s

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf' : IsLimit kf'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ (Fork.ι kf ≫ Arrow.Hom.left φ) ≫ f' = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf.mapOfIsLimit hf' φ.hom ≫ kf'.mapOfIsLimit hf φ.inv) ≫ Fork.ι kf = 𝟙 kf.pt ≫ Fork.ι kf

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
kf : KernelFork f
kf' : KernelFork f'
hf : IsLimit kf
hf' : IsLimit kf'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ (kf'.mapOfIsLimit hf φ.inv ≫ kf.mapOfIsLimit hf' φ.hom) ≫ Fork.ι kf' = 𝟙 kf'.pt ≫ Fork.ι kf'

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (Iso.refl (limit.cone (parallelPair f 0)).pt).hom ≫ (Fork.ofι (kernel.ι f) ⋯).ι =
    Fork.ι (limit.cone (parallelPair f 0))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h ≫ equalizer.ι f 0 = 0 ≫ equalizer.ι f 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝³ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ (kernel.ι f' ≫ inv p) ≫ f = 0

Tactic:
simp [← cancel_mono q, w]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : Epi (kernel.ι f)
⊢ kernel.ι f ≫ f = kernel.ι f ≫ 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ 𝟙 X ≫ 0 = 0

Tactic:
simp

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

Goal state before:
pp: case left
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✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).hom ≫ kernel.ι f = kernel.ι f

Tactic:
simp

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

Goal state before:
pp: case right
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✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (F.mapBicone b.toBicone).toCone).pt).hom ≫
      (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).inv ≫ kernel.ι f = kernel.ι f

Tactic:
simp

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

Goal state before:
pp: case left
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✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.left }

Tactic:
simp

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

Goal state before:
pp: case right
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✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
he : e ≫ f = 0
inst✝ : HasKernel f
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).hom = kernel.lift f e ⋯

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
inst✝ : HasKernel f
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).inv = kernel.lift f e ⋯

Tactic:
simp

Goal state after: