mathlib-initiative/mathlib-tactics huggingface dataset:
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ∀ (j : Discrete WalkingPair),
    ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app j =
      (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 j

Tactic:
by

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 : Fork f 0
⊢ ∀ (j : WalkingParallelPair), s.π.app j = (Iso.refl s.pt).hom ≫ (Fork.ofι s.ι ⋯).π.app j

Tactic:
by

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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ ι' ≫ f = 0

Tactic:
by

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)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G

Tactic:
by

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
⊢ (iso G X Y).inv ≫ G.map prod.fst = prod.fst

Tactic:
by

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
⊢ (iso G X Y).inv ≫ G.map prod.snd = prod.snd

Tactic:
by

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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (prodComparison G X Y)

Tactic:
by

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
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
i : ∀ {X Y : C}, IsIso (prodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesLimit K G

Tactic:
by

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
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ∀ (j : Discrete WalkingPair),
    ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app j ≫
        (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 j

Tactic:
by

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✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G

Tactic:
by

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
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (coprodComparison G X Y)

Tactic:
by

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
D : Type u'
inst✝² : Category.{v, u'} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
app : (j : WalkingParallelPair) → (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
  fun j ↦
    match j with
    | zero => Iso.refl ((parallelPair f 0 ⋙ F).obj zero)
    | one => Iso.refl ((parallelPair f 0 ⋙ F).obj one)
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f 0 ⋙ F).map f_1 ≫ (app Y_1).hom = (app X_1).hom ≫ (parallelPair (F.map f) 0).map f_1

Tactic:
by

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
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesColimit K G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : leftExactFunctor C D X✝
⊢ leftExactFunctor C D Y✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X✝ Y✝ : C ⥤ D
e : X✝ ≅ Y✝
h : rightExactFunctor C D X✝
⊢ rightExactFunctor C D Y✝

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (exactFunctor C D).IsClosedUnderIsomorphisms

Tactic:
by

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
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)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
⊢ leftExactFunctor C D F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteColimits F
⊢ rightExactFunctor C D F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ exactFunctor C D F

Tactic:
by

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

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
F : C ⥤ₗ D
G : D ⥤ₗ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
by

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

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
F : D ⥤ₗ E
G : C ⥤ₗ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
by

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

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
F : C ⥤ᵣ D
G : D ⥤ᵣ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
by

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 K : C
f : X ⟶ Y
i : K ⟶ X
w : i ≫ f = 0
h : {A : C} → (k : A ⟶ X) → k ≫ f = 0 → { l // l ≫ i = k }
hi : Mono i
A : C
k : A ⟶ X
hk : k ≫ f = 0
m : A ⟶ K
hm : m ≫ i = k
⊢ m = ↑(h k hk)

Tactic:
by

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

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
F : D ⥤ᵣ E
G : C ⥤ᵣ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
by

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
⊢ Fork.ι c ≫ h = 0

Tactic:
by

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

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
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
by

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

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
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
by

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 : Fork h 0
⊢ s.ι ≫ f = s.ι ≫ 0

Tactic:
by

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

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
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
by

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

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
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
by

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 : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = s.ι
⊢ m✝ = ↑l

Tactic:
by

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 ≫ f = Fork.ι s ≫ 0

Tactic:
by

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
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ s.ι ≫ h = 0

Tactic:
by

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
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ i.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι

Tactic:
by

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
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m = i.lift (KernelFork.ofι s.ι ⋯)

Tactic:
by

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
hf : f = 0
W'✝ : C
x✝² : W'✝ ⟶ X
x✝¹ : x✝² ≫ f = 0
x✝ : W'✝ ⟶ X
hb : x✝ ≫ 𝟙 X = x✝²
⊢ x✝ = x✝²

Tactic:
by

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
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 ≫ Fork.ι c = Fork.ι s

Tactic:
by

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
⊢ (Fork.ι c ≫ e.hom) ≫ g' = 0

Tactic:
by

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
⊢ (s ≫ e.inv) ≫ g = 0

Tactic:
by

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:
by

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
m : W'✝ ⟶ c.pt
hm : m ≫ Fork.ι c ≫ e.hom = s
⊢ m ≫ Fork.ι c = hc.lift (ofι (s ≫ e.inv) ⋯) ≫ Fork.ι c

Tactic:
by

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
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ Fork.ι c ≫ g' = 0

Tactic:
by

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
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ (Iso.refl X).hom ≫ g' = 0

Tactic:
by

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
hc : IsLimit c
inst✝ : Mono f
⊢ IsZero c.pt

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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 = 0

Tactic:
by

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
k : W ⟶ X
h : k ≫ f = 0
inst✝ : Mono k
Z : C
g g' : Z ⟶ W
w : g ≫ lift f k h = g' ≫ lift f k h
⊢ g = g'

Tactic:
by

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'
⊢ (ι f ≫ p) ≫ f' = 0

Tactic:
by

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
q : Y ⟶ Y
w : f ≫ q = 𝟙 X ≫ f
⊢ map f f (𝟙 X) q w = 𝟙 (kernel f)

Tactic:
by

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:
by

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.map f f' p q w ≫ kernel.lift f (kernel.ι f' ≫ inv p) ⋯ = 𝟙 (kernel f)

Tactic:
by

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.lift f (kernel.ι f' ≫ inv p) ⋯ ≫ kernel.map f f' p q w = 𝟙 (kernel f')

Tactic:
by

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 X' Y' Z' : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasKernel g
w : f ≫ g = 0
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
inst✝ : HasKernel g'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ lift g f w ≫ map g g' q r h₂ = p ≫ lift g' f' w'

Tactic:
by

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 X' Y' : C
f : X ⟶ Y
f' : X' ⟶ Y'
inst✝¹ : HasKernel f
inst✝ : HasKernel f'
q : Y ⟶ Y'
w : f ≫ q = 0 ≫ f'
⊢ map f f' 0 q w = 0

Tactic:
by

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.hom = p.hom ≫ f'
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
by

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:
by

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:
by

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
⊢ kernelZeroIsoSource.inv = kernel.lift 0 (𝟙 X) ⋯

Tactic:
by

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
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j) ≫ F.map (b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
by

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
inst✝ : PreservesBiproducts F
J : Type
x✝ : Finite J
⊢ PreservesBiproductsOfShape J F

Tactic:
by

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✝
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
by

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
h : f = f
⊢ kernelIsoOfEq h = Iso.refl (kernel f)

Tactic:
by

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 g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Tactic:
by

Goal state after: