mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map left ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map right ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
i : WalkingParallelPair
⊢ (parallelPair f g).map (WalkingParallelPairHom.id i) ≫ WalkingParallelPair.casesOn i (f ≫ π) π =
    WalkingParallelPair.casesOn i (f ≫ π) π ≫
      ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id i)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map left ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map right ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
i : WalkingParallelPair
⊢ (parallelPair f g).map (WalkingParallelPairHom.id i) ≫ WalkingParallelPair.casesOn i (f ≫ π) π =
    WalkingParallelPair.casesOn i (f ≫ π) π ≫
      ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift F'.ofCompIso ≫ F'.m = ((Image.monoFactorisation f).compMono g).m

Tactic:
rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m),
            ← IsIso.inv_hom_id g, ← Category.assoc]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ F.map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ F.map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ F.map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map left ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map right ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
X✝ : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X✝ : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map left ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ (parallelPair (F.map left) (F.map right)).map right ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X✝ : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsZero X ∧ IsZero Y → IsIso 0

Tactic:
intro ⟨hX, hY⟩

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
hX : IsZero X
hY : IsZero Y
⊢ IsIso 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

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

Tactic:
apply hm.right_cancellation

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
s : Fork (f ≫ h) (g ≫ h)
⊢ (s.ι ≫ f) ≫ h = (s.ι ≫ g) ≫ h
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

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

Tactic:
<;>

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

case one
C : Type u
inst✝ : Category.{v, u} C
⊢ one ∈ [zero, one].toFinset
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 ∅

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

Goal state after:
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 ∅

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 ∅
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 ∅

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

Goal state after:
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 ∅

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 ∅
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}

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

Tactic:
<;>

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

case right
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.right ∈ {WalkingPair.left, WalkingPair.right}
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 }

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

Goal state after:
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 }

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 }
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 }

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

Goal state after:
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 }

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 }
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case zero
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 zero = s.π.app zero

Tactic:
exact fac s

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

Goal state before:
pp: case left
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
⊢ PreservesFiniteLimits F

pp: case right
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
⊢ PreservesFiniteColimits F

Tactic:
<;>

Goal state after:
case left
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
⊢ PreservesFiniteLimits F

case right
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
⊢ PreservesFiniteColimits F
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 rw [zero_comp, ← cancel_mono f, zero_comp, s.condition]

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 }

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

Goal state after:
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 }

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 }
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✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
            (F.mapBicone b.toBicone).toCone).π.app
      j =
    (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 j

Tactic:
by
            rcases j with ⟨⟨⟩⟩ <;> simp

Goal state after: