awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesPointwiseRightKanExtension F L
inst_5 : L.HasPointwiseRightKanExtension F
a : A
⊢ Eq (α := (L.pointwiseRightKanExtension (F ⋙ G)).obj (L.obj a) ⟶ G.obj (F.obj a))
    (CategoryStruct.comp (Y := (L.pointwiseRightKanExtension F ⋙ G).obj (L.obj a))
        (NatTrans.app (Iso.inv (G.pointwiseRightKanExtensionCompIsoOfPreserves F L)) (L.obj a))
        (G.map (NatTrans.app (L.pointwiseRightKanExtensionCounit F) a)) :
      (L.pointwiseRightKanExtension (F ⋙ G)).obj (L.obj a) ⟶ G.obj (F.obj a))
    (NatTrans.app (L.pointwiseRightKanExtensionCounit (F ⋙ G)) a :
      (L ⋙ L.pointwiseRightKanExtension (F ⋙ G)).obj a ⟶ (F ⋙ G).obj a)

Tactic:
simpa [-pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasRightKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
hγ :
  CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.whiskerLeft
        ((L.ran ⋙ obj (whiskeringRight C B D) G).map η ≫
          Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
              F')))
      (L.rightKanExtensionCounit (F' ⋙ G)) =
    L.whiskerLeft
        (Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
              F) ≫
          (obj (whiskeringRight A B D) G ⋙ L.ran).map η) ≫
      L.rightKanExtensionCounit (F' ⋙ G)
⊢ (L.ran ⋙ obj (whiskeringRight C B D) G).map η ≫
      Iso.hom
        ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
            (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
          F') =
    Iso.hom
        ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
            (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
          F) ≫
      (obj (whiskeringRight A B D) G ⋙ L.ran).map η

Tactic:
apply hom_ext_of_isRightKanExtension
        (L.rightKanExtension <| F' ⋙ G)
        (L.rightKanExtensionCounit <| F' ⋙ G)

Premises used: CategoryTheory.Functor.rightKanExtensionCounit, CategoryTheory.Functor.comp, CategoryTheory.Functor.hom_ext_of_isRightKanExtension, CategoryTheory.Functor.rightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasRightKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
hγ :
  Eq (α := L ⋙ L.rightKanExtension F ⋙ G ⟶ F' ⋙ G)
    (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.whiskerLeft
            (whiskerRight
              ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F') (L.rightKanExtension F)
                (L.rightKanExtensionCounit F ≫ η))
              G) ≫
          L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F' L)) :
        L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.rightKanExtensionCounit (F' ⋙ G) : L ⋙ L.rightKanExtension (F' ⋙ G) ⟶ F' ⋙ G))
    (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F ⋙ G))
        (L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) :
          L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F ⋙ G))
        (L.whiskerLeft
            ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
              (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G)) :
          L ⋙ L.rightKanExtension (F ⋙ G) ⟶ L ⋙ L.rightKanExtension (F' ⋙ G)) ≫
      L.rightKanExtensionCounit (F' ⋙ G))
⊢ CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.whiskerLeft
        ((L.ran ⋙ obj (whiskeringRight C B D) G).map η ≫
          Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
              F')))
      (L.rightKanExtensionCounit (F' ⋙ G)) =
    L.whiskerLeft
        (Iso.hom
            ((fun (F : Functor.{v_1, v_2, u_1, u_2} A B) ↦
                (G.rightKanExtensionCompIsoOfPreserves F L : L.rightKanExtension F ⋙ G ≅ L.rightKanExtension (F ⋙ G)))
              F) ≫
          (obj (whiskeringRight A B D) G ⋙ L.ran).map η) ≫
      L.rightKanExtensionCounit (F' ⋙ G)

Tactic:
dsimp [ran]

Premises used: CategoryTheory.Functor.ran
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasRightKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
hγ :
  ∀ (x : A),
    Eq (α := (L ⋙ L.rightKanExtension F ⋙ G).obj x ⟶ (F' ⋙ G).obj x)
      (NatTrans.app
        (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
          (L.whiskerLeft
                (whiskerRight
                  ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F')
                    (L.rightKanExtension F) (L.rightKanExtensionCounit F ≫ η))
                  G) ≫
              L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F' L)) :
            L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F' ⋙ G))
          (L.rightKanExtensionCounit (F' ⋙ G) : L ⋙ L.rightKanExtension (F' ⋙ G) ⟶ F' ⋙ G))
        x)
      (NatTrans.app
        (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F ⋙ G))
            (L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) :
              L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F ⋙ G))
            (L.whiskerLeft
                ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
                  (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G)) :
              L ⋙ L.rightKanExtension (F ⋙ G) ⟶ L ⋙ L.rightKanExtension (F' ⋙ G)) ≫
          L.rightKanExtensionCounit (F' ⋙ G))
        x)
⊢ Eq (α := L ⋙ L.rightKanExtension F ⋙ G ⟶ F' ⋙ G)
    (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.whiskerLeft
            (whiskerRight
              ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F') (L.rightKanExtension F)
                (L.rightKanExtensionCounit F ≫ η))
              G) ≫
          L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F' L)) :
        L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F' ⋙ G))
      (L.rightKanExtensionCounit (F' ⋙ G) : L ⋙ L.rightKanExtension (F' ⋙ G) ⟶ F' ⋙ G))
    (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F ⋙ G))
        (L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) :
          L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F ⋙ G))
        (L.whiskerLeft
            ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
              (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G)) :
          L ⋙ L.rightKanExtension (F ⋙ G) ⟶ L ⋙ L.rightKanExtension (F' ⋙ G)) ≫
      L.rightKanExtensionCounit (F' ⋙ G))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasRightKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
x : A
hγ :
  Eq (α := G.obj ((L.rightKanExtension F).obj (L.obj x)) ⟶ G.obj (F'.obj x))
    (G.map
      (NatTrans.app
          ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F') (L.rightKanExtension F)
            (L.rightKanExtensionCounit F ≫ η))
          (L.obj x) ≫
        NatTrans.app (L.rightKanExtensionCounit F') x))
    (G.map (NatTrans.app (L.rightKanExtensionCounit F) x ≫ η.app x))
⊢ Eq (α := (L ⋙ L.rightKanExtension F ⋙ G).obj x ⟶ (F' ⋙ G).obj x)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F' ⋙ G))
        (L.whiskerLeft
              (whiskerRight
                ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F')
                  (L.rightKanExtension F) (L.rightKanExtensionCounit F ≫ η))
                G) ≫
            L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F' L)) :
          L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F' ⋙ G))
        (L.rightKanExtensionCounit (F' ⋙ G) : L ⋙ L.rightKanExtension (F' ⋙ G) ⟶ F' ⋙ G))
      x)
    (NatTrans.app
      (CategoryStruct.comp (Y := L ⋙ L.rightKanExtension (F ⋙ G))
          (L.whiskerLeft (Iso.hom (G.rightKanExtensionCompIsoOfPreserves F L)) :
            L ⋙ L.rightKanExtension F ⋙ G ⟶ L ⋙ L.rightKanExtension (F ⋙ G))
          (L.whiskerLeft
              ((L.rightKanExtension (F' ⋙ G)).liftOfIsRightKanExtension (L.rightKanExtensionCounit (F' ⋙ G))
                (L.rightKanExtension (F ⋙ G)) (L.rightKanExtensionCounit (F ⋙ G) ≫ whiskerRight η G)) :
            L ⋙ L.rightKanExtension (F ⋙ G) ⟶ L ⋙ L.rightKanExtension (F' ⋙ G)) ≫
        L.rightKanExtensionCounit (F' ⋙ G))
      x)

Tactic:
simp only [comp_obj, Category.assoc, rightKanExtensionCompIsoOfPreserves_hom_fac,
        NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, associator_inv_app, Category.id_comp,
        liftOfIsRightKanExtension_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc,
        ← G.map_comp]

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Functor.associator_inv_app, CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac, CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac_assoc, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesRightKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasRightKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasRightKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
x : A
⊢ Eq (α := G.obj ((L.rightKanExtension F).obj (L.obj x)) ⟶ G.obj (F'.obj x))
    (G.map
      (NatTrans.app
          ((L.rightKanExtension F').liftOfIsRightKanExtension (L.rightKanExtensionCounit F') (L.rightKanExtension F)
            (L.rightKanExtensionCounit F ≫ η))
          (L.obj x) ≫
        NatTrans.app (L.rightKanExtensionCounit F') x))
    (G.map (NatTrans.app (L.rightKanExtensionCounit F) x ≫ η.app x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
rw rw₁ : X j = X j
⊢ X i = X j

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
rw rw₁ : X (j + 1) = X (j + 1)
⊢ X (j + 1) = X (i + 1)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
subst : f i = eqToHom ⋯ ≫ f i ≫ eqToHom ⋯
⊢ f i = eqToHom ⋯ ≫ f j ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ f i = eqToHom ⋯ ≫ f i ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f_1 : (n : ℕ) → X n ⟶ X (n + 1)
x : ℕ → C
f : (n : ℕ) → x n ⟶ x (n + 1)
l : ℕ
h : 0 ≤ l + 1
⊢ 0 ≤ l

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f_1 : (n : ℕ) → X n ⟶ X (n + 1)
x : ℕ → C
f : (n : ℕ) → x n ⟶ x (n + 1)
k l : ℕ
h : k + 1 ≤ l + 1
⊢ k ≤ l

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ i ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
revert : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i i ⋯ = 𝟙 (X i)
⊢ map f i i ⋯ = 𝟙 (X i)

Tactic:
revert X f
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f 0 0 ⋯ = 𝟙 (X 0)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n n ⋯ = 𝟙 (X n)
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ map f (n + 1) (n + 1) ⋯ = 𝟙 (X (n + 1))

Tactic:
apply hi
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
zero : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f 0 0 ⋯ = 𝟙 (X 0)
succ :
  ∀ (n : ℕ) (hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n n ⋯ = 𝟙 (X n)) {X : ℕ → C}
    (f : (n : ℕ) → X n ⟶ X (n + 1)), map f (n + 1) (n + 1) ⋯ = 𝟙 (X (n + 1))
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i i ⋯ = 𝟙 (X i)

Tactic:
induction i with
  | zero => intros; rfl
  | succ _ hi =>
      intro X f
      apply hi
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ i ≤ i + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
revert : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i (i + 1) ⋯ = f i
⊢ map f i (i + 1) ⋯ = f i

Tactic:
revert X f
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ Eq (α := X 0 ⟶ X (HAdd.hAdd (α := ℕ) 0 1)) (map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯) (f 0)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n (n + 1) ⋯ = f n
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
⊢ Eq (α := X (n + 1) ⟶ X (n + 1 + 1)) (map f (n + 1) (n + 1 + 1) ⋯) (f (n + 1))

Tactic:
apply hi
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
i : ℕ
zero :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)),
    Eq (α := X 0 ⟶ X (HAdd.hAdd (α := ℕ) 0 1)) (map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯) (f 0)
succ :
  ∀ (n : ℕ) (hi : ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f n (n + 1) ⋯ = f n) {X : ℕ → C}
    (f : (n : ℕ) → X n ⟶ X (n + 1)), Eq (α := X (n + 1) ⟶ X (n + 1 + 1)) (map f (n + 1) (n + 1 + 1) ⋯) (f (n + 1))
⊢ ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)), map f i (i + 1) ⋯ = f i

Tactic:
induction i with
  | zero => intros; rfl
  | succ _ hi =>
      intro X f
      apply hi
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : LE.le (α := ℕ) 0 0
hjk : 0 ≤ k
zero : map f 0 k ⋯ = 𝟙 (X 0) ≫ map f 0 k hjk
zero₁ zero₂ : map f 0 k ⋯ = map f 0 k hjk
⊢ map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk

Tactic:
rw [map_id, id_comp]

Premises used: CategoryTheory.Functor.OfSequence.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
k : ℕ
hij : 0 ≤ j + 1
hjk : j + 1 ≤ k
zero : ∀ (hjk : j + 1 ≤ 0), map f 0 0 ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) 0 hjk
zero₁ :
  ∀ (hjk : j + 1 ≤ HAdd.hAdd (α := ℕ) 0 1),
    map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (HAdd.hAdd (α := ℕ) 0 1) hjk
zero₂ : ∀ (k : ℕ) (hjk : j + 1 ≤ k + 1 + 1), map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk
⊢ map f 0 k ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) k hjk

Tactic:
obtain (_ | _ | k) := k
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ 0
⊢ map f 0 0 ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) 0 hjk

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ HAdd.hAdd (α := ℕ) 0 1
⊢ j = 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ HAdd.hAdd (α := ℕ) 0 1
zero :
  ∀
    (hj :
      ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
        map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk)
    (hij : 0 ≤ HAdd.hAdd (α := ℕ) 0 1) (hjk : HAdd.hAdd (α := ℕ) 0 1 ≤ HAdd.hAdd (α := ℕ) 0 1),
    map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ =
      map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ map f (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1) hjk
⊢ map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (HAdd.hAdd (α := ℕ) 0 1) hjk

Tactic:
obtain rfl : j = 0 := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : LE.le (α := ℕ) 0 0) (hjk : 0 ≤ k),
    map f 0 k ⋯ = map f 0 0 hij ≫ map f 0 k hjk
hij : 0 ≤ HAdd.hAdd (α := ℕ) 0 1
hjk : HAdd.hAdd (α := ℕ) 0 1 ≤ HAdd.hAdd (α := ℕ) 0 1
zero : map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ = map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ 𝟙 (X (HAdd.hAdd (α := ℕ) 0 1))
zero₁ zero₂ : map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ = map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij
⊢ map f 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ =
    map f 0 (HAdd.hAdd (α := ℕ) 0 1) hij ≫ map f (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 1) hjk

Tactic:
rw [map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.OfSequence.map_id
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
zero :
  Eq (α := X 0 ⟶ X (k + 1 + 1)) (f 0 ≫ map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯)
    (map f 0 (j + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯)
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
simp only [map, Nat.reduceAdd]

Premises used: CategoryTheory.Functor.OfSequence.map, Nat.reduceAdd
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ 0 ≤ j

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ j ≤ k + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Functor.OfSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
zero :
  Eq (α := X 0 ⟶ X (k + 1 + 1))
    (f 0 ≫
      CategoryStruct.comp (Y := X (j + 1)) (map (fun (n : ℕ) ↦ f (n + 1)) 0 j ⋯)
        (map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯))
    (map f 0 (j + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯)
⊢ Eq (α := X 0 ⟶ X (k + 1 + 1)) (f 0 ≫ map (fun (n : ℕ) ↦ f (n + 1)) 0 (k + 1) ⋯)
    (map f 0 (j + 1) hij ≫ map (fun (n : ℕ) ↦ f (n + 1)) j (k + 1) ⋯)

Tactic:
rw [hj (fun n ↦ f (n + 1)) (k + 1) (by lia) (by lia)]

Premises used: HAdd.hAdd, OfNat.ofNat