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

Goal state before:
pp: case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0 = 0

Tactic:
·

Goal state after:
case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)

pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')

Tactic:
·

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)

pp: case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)

Tactic:
·

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)

Tactic:
·

Goal state after:
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')

Tactic:
·

Goal state after:
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')

pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

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

Goal state after:
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j ↦ {Hom.term j}) fun j' ↦
      if h : some j' = j then ⋯.mpr {Hom.id j} else ∅
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:
·

Goal state after:
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 ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')

pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')

Tactic:
·

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)

pp: case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')

Tactic:
·

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')

Tactic:
·

Goal state after:
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')

Tactic:
·

Goal state after:
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')

pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

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

Goal state after:
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Hom.id j ∈
    Option.casesOn j (Option.casesOn j {Hom.id none} fun j' ↦ {Hom.init j'}) fun j_1 ↦
      if h : some j_1 = j then ⋯.mpr {Hom.id j} else ∅
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:
·

Goal state after:
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 ∅
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ (P ⊔ Q).isoClosure X → P.isoClosure X ∨ Q.isoClosure X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ (P ⊔ Q).isoClosure X → P.isoClosure X ∨ Q.isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : P Y
⊢ P.isoClosure X ∨ Q.isoClosure X

pp: case mp.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
·

Goal state after:
case mp.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : P Y
⊢ P.isoClosure X ∨ Q.isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X

Tactic:
·

Goal state after:
case mp.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X Y : C
e : X ≅ Y
hY : Q Y
⊢ P.isoClosure X ∨ Q.isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ P.isoClosure X ∨ Q.isoClosure X → (P ⊔ Q).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

pp: case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
·

Goal state after:
case mpr.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

pp: case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
· exact monotone_isoClosure le_sup_left _ hY

Goal state after:
case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
·

Goal state after:
case mpr.inr
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : Q.isoClosure X
⊢ (P ⊔ Q).isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure ≤ ⨆ a, (P a).isoClosure

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ⨆ a, (P a).isoClosure ≤ (⨆ a, P a).isoClosure

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure ≤ ⨆ a, (P a).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ⨆ a, (P a).isoClosure ≤ (⨆ a, P a).isoClosure

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ ⨆ a, (P a).isoClosure ≤ (⨆ a, P a).isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X → P.isoClosure X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X → ⊤.map P.ι X

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X → P.isoClosure X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X → ⊤.map P.ι X

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X → ⊤.map P.ι X
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
  apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)
  apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
  refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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
this : PreservesColimit (pair (K.obj { as := WalkingPair.left }) (K.obj { as := WalkingPair.right })) G
⊢ PreservesColimit K G

Tactic:
apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

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

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

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

Goal state after:
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
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case pos
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
h : j = j'
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯

pp: case neg
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
h : ¬j = j'
⊢ F.map (b.ι j ≫ b.π j') = 0

Tactic:
·

Goal state after:
case pos
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
h : j = j'
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case neg
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
h : ¬j = j'
⊢ F.map (b.ι j ≫ b.π j') = 0

Tactic:
·

Goal state after:
case neg
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
h : ¬j = j'
⊢ F.map (b.ι j ≫ b.π j') = 0
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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h✝ : l ≫ i.hom = f
s✝ : KernelFork f
hs : IsLimit s✝
s : Fork l 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι s✝) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s✝) ⋯) = s.ι
⊢ m = hs.lift (KernelFork.ofι s.ι ⋯)

Tactic:
by
      apply Fork.IsLimit.hom_ext hs
      simpa using h

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ Discrete.functor f ⋙ G ≅ Discrete.functor fun j ↦ G.obj (f j)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (G.mapCone (Fan.mk P g)) ≅ Fan.mk (G.obj P) fun j ↦ G.map (g j)

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ Discrete.functor f ⋙ G ≅ Discrete.functor fun j ↦ G.obj (f j)
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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app zero = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app zero

pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app one

Tactic:
·

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app zero = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app zero
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Discrete.functor fun j ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Cocone.precompose (Iso.hom ?refine_1)).obj (G.mapCocone (Cofan.mk P g)) ≅ Cofan.mk (G.obj P) fun j ↦ G.map (g j)

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Discrete.functor fun j ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G
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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app one

Tactic:
·

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app one
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 : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one

Tactic:
·

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app zero ≫ desc s = s.ι.app zero
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 : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one

Tactic:
·

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
⊢ t.ι.app one ≫ desc s = s.ι.app one