mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₁'.IsRightKanExtension α₁ → F₂'.IsRightKanExtension α₂
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : L ⋙ F₁' ⟶ F₁
α₂ : L ⋙ F₂' ⟶ F₂
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : L.whiskerLeft e'.hom ≫ α₂ = α₁ ≫ e.hom
eq : CostructuredArrow.IsUniversal (RightExtension.mk F₁' α₁) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk F₂' α₂) := ⋯
⊢ F₂'.IsRightKanExtension α₂ → F₁'.IsRightKanExtension α₁
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ (limitCompWhiskeringRightIsoLimitComp F G).hom ≫ whiskerRight (limit.π G j) F =
    limit.π (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
by
  simp [← Iso.eq_inv_comp]

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

Goal state before:
pp: case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this✝ : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsFiltered J] (d : J) (n : ℕ),
    d ≤ (sequentialFunctor J).obj n →
      Nonempty (StructuredArrow d (sequentialFunctor J)) →
        ∀ (i j : StructuredArrow d (sequentialFunctor J)), j.right ≤ i.right → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : i.right < j.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsFiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
·

Goal state after:
case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this✝ : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsFiltered J] (d : J) (n : ℕ),
    d ≤ (sequentialFunctor J).obj n →
      Nonempty (StructuredArrow d (sequentialFunctor J)) →
        ∀ (i j : StructuredArrow d (sequentialFunctor J)), j.right ≤ i.right → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : i.right < j.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsFiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
·

Goal state after:
J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsFiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this✝ : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsCofiltered J] (d : J) (n : ℕ),
    (sequentialFunctor J).obj (op n) ≤ d →
      Nonempty (CostructuredArrow (sequentialFunctor J) d) →
        ∀ (i j : CostructuredArrow (sequentialFunctor J) d),
          unop i.left ≤ unop j.left → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
·

Goal state after:
case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this✝ : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsCofiltered J] (d : J) (n : ℕ),
    (sequentialFunctor J).obj (op n) ≤ d →
      Nonempty (CostructuredArrow (sequentialFunctor J) d) →
        ∀ (i j : CostructuredArrow (sequentialFunctor J) d),
          unop i.left ≤ unop j.left → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
·

Goal state after:
J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)

pp: case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)

Tactic:
apply IsInitial.isInitialIffObj Ψ.inverse _ |>.invFun

Goal state after:
case refine_1
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := ⋯
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension β
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
⊢ IsInitial (Ψ.inverse.obj (LeftExtension.mk F₂ γ))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := leftExtensionEquivalenceOfIso₁ e F₀
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₂ β)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (cokernelOrderHom X).comp (kernelOrderHom X) = OrderHom.id

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (kernelOrderHom X).comp (cokernelOrderHom X) = OrderHom.id

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (cokernelOrderHom X).comp (kernelOrderHom X) = OrderHom.id
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A

pp: case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))

pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_1 ≫ ?refine_1.refine_2).unop = (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_2 ≫ ?refine_1.refine_1).unop = (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := ?refine_1.refine_1, inv := ?refine_1.refine_2, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
·

Goal state after:
case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ op (cokernel (kernel.ι f.unop)) ⟶ A
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))

pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ ?refine_1.refine_2).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ (?refine_1.refine_2 ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop = (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := ?refine_1.refine_2, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ A ⟶ op (cokernel (kernel.ι f.unop))
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
·

Goal state after:
case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
·

Goal state after:
case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
·

Goal state after:
case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (kernelOrderHom X).comp (cokernelOrderHom X) = OrderHom.id

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ (kernelOrderHom X).comp (cokernelOrderHom X) = OrderHom.id
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A

pp: case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)

pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_1 ≫ ?refine_2.refine_2 = 𝟙 (kernel (cokernel.π f))

pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_2 ≫ ?refine_2.refine_1 = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := ?refine_2.refine_1, inv := ?refine_2.refine_2, hom_inv_id := ?refine_2.refine_3,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel (cokernel.π f) ⟶ A
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)

pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ ?refine_2.refine_2 = 𝟙 (kernel (cokernel.π f))

pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ?refine_2.refine_2 ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := ?refine_2.refine_2, hom_inv_id := ?refine_2.refine_3,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ A ⟶ kernel (cokernel.π f)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (cokernel.π f))

pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯,
          hom_inv_id := ?refine_2.refine_3, inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
·

Goal state after:
case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (cokernel.π f))
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
·

Goal state after:
case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A