awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))
    (φ.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))
    (φ'.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
f : F ⟶ G
rw : (∀ (X : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsIso (f.app X)) ↔ IsIso (X := F.obj 0) (f.app 0)
⊢ IsIso f ↔ IsIso (X := F.obj 0) (f.app 0)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0)
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
0 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))
⊢ IsIso (f.app i)

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
f : F ⟶ G
⊢ (∀ (X : Fin (HAdd.hAdd (α := ℕ) 0 1)), IsIso (f.app X)) ↔ IsIso (X := F.obj 0) (f.app 0)

Tactic:
exact ⟨fun h ↦ h 0, fun _ i ↦ by fin_cases i; assumption⟩
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 0
h : F.obj' 0 homMk₀._proof_1 = G.obj 0
i : ℕ
hi : i < 0
⊢ F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : ComposableArrows.{v_1, u_1} C 0
⊢ ∃ (X : C), F = mk₀ X

Tactic:
⟨F.obj' 0, ext₀ rfl⟩

Premises used: Exists.intro, CategoryTheory.ComposableArrows.ext₀, CategoryTheory.ComposableArrows.obj', OfNat.ofNat, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ⟶ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ⟶ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
i : ℕ
hi : i < 1
⊢ i = 0

Tactic:
simpa using hi
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ⟶ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ⟶ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
i : ℕ
hi : i < 1
obtain :
  ∀ (hi : LT.lt (α := ℕ) 0 1),
    Eq (α := F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
      (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
          (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
              (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => left
                | ⟨1, isLt⟩ => right :
                F.obj i ⟶ G.obj i))
            ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
        F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
      (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
          ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
                (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
                  | ⟨0, isLt⟩ => left
                  | ⟨1, isLt⟩ => right :
                  F.obj i ⟶ G.obj i))
              ⟨0, ⋯⟩ :
            F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨0, ⋯⟩)
          (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
            G.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
        F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
⊢ F.map' i (i + 1) ⋯ hi ≫
      (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => left
            | ⟨1, isLt⟩ => right :
            F.obj i ⟶ G.obj i))
        ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => left
            | ⟨1, isLt⟩ => right :
            F.obj i ⟶ G.obj i))
        (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
obtain rfl : i = 0 := by simpa using hi

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ⟶ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ⟶ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
hi : LT.lt (α := ℕ) 0 1
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
        (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
            (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => left
              | ⟨1, isLt⟩ => right :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
      F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
              (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => left
                | ⟨1, isLt⟩ => right :
                F.obj i ⟶ G.obj i))
            ⟨0, ⋯⟩ :
          F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨0, ⋯⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
          G.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
      F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)

Tactic:
w
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ⟶ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ⟶ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
hi : LT.lt (α := ℕ) 0 1
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
        (fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
            (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => left
              | ⟨1, isLt⟩ => right :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
      F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦
              (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => left
                | ⟨1, isLt⟩ => right :
                F.obj i ⟶ G.obj i))
            ⟨0, ⋯⟩ :
          F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨0, ⋯⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
          G.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
      F.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
w : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), φ.app i = φ'.app i
⊢ φ = φ'

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 0) (φ.app 0) (φ'.app 0)

Tactic:
h₀

Premises used: Fin.ofNat
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 0) (φ.app 0) (φ'.app 0)

Tactic:
exact h₀
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := F.obj 1 ⟶ G.obj 1) (φ.app 1) (φ'.app 1)

Tactic:
h₁

Premises used: Fin.ofNat
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := F.obj 1 ⟶ G.obj 1) (φ.app 1) (φ'.app 1)

Tactic:
exact h₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
φ φ' : F ⟶ G
h₀ : app' φ 0 homMk₁._proof_2 = app' φ' 0 homMk₁._proof_2
h₁ : app' φ 1 homMk₁._proof_3 = app' φ' 1 homMk₁._proof_3
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ φ.app i = φ'.app i

Tactic:
match i with
    | 0 => exact h₀
    | 1 => exact h₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ≅ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ≅ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
rw :
  G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ 𝟙 (G.obj' 1 homMk₁._proof_3) = G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
⊢ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right.inv = left.inv ≫ F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3

Tactic:
rw [← cancel_mono right.hom, assoc, assoc, w, right.inv_hom_id, left.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C 1
left : F.obj' 0 homMk₁._proof_2 ≅ G.obj' 0 homMk₁._proof_2
right : F.obj' 1 homMk₁._proof_3 ≅ G.obj' 1 homMk₁._proof_3
w : F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ right.hom = left.hom ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3
⊢ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ 𝟙 (G.obj' 1 homMk₁._proof_3) = G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : ComposableArrows.{v_1, u_1} C 1
⊢ F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 = F.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
f : F ⟶ G
rw :
  (∀ (X : Fin (HAdd.hAdd (α := ℕ) 1 1)), IsIso (f.app X)) ↔
    IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
⊢ IsIso f ↔ IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
1 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
⊢ IsIso (f.app i)

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
0 h_1 h_2 :
  IsIso (X := F.obj 0) (f.app 0) →
    IsIso (X := F.obj 1) (f.app 1) →
      IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
        (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)
1 h_1 h_2 :
  IsIso (X := F.obj 0) (f.app 0) →
    IsIso (X := F.obj 1) (f.app 1) →
      IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
        (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
f : F ⟶ G
⊢ (∀ (X : Fin (HAdd.hAdd (α := ℕ) 1 1)), IsIso (f.app X)) ↔
    IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1)

Tactic:
exact ⟨fun h ↦ ⟨h 0, h 1⟩, fun _ i ↦ by fin_cases i <;> tauto⟩
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.map' 0 1 homMk₁._proof_2 homMk₁._proof_3 ≫ Iso.hom (eqToIso right) =
    Iso.hom (eqToIso left) ≫ G.map' 0 1 homMk₁._proof_2 homMk₁._proof_3

Tactic:
simp [map'_eq_hom₁, w]

Premises used: CategoryTheory.ComposableArrows.map'_eq_hom₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩)
1 :
  F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩)
⊢ F.obj i = G.obj i

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) =
    G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
0 :
  Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    ((isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (eqToHom ⋯)
1 :
  Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    ((isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    (eqToHom ⋯)
⊢ (isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app i = eqToHom ⋯

Tactic:
fin_cases i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    ((isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨0, ⋯⟩))
    (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 1
left : F.left = G.left
right : F.right = G.right
w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom ⋯
⊢ Eq (α :=
    F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1))) ⟶
      G.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    ((isoMk₁ (eqToIso left) (eqToIso right) ⋯).hom.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ i) ⟨1, ⋯⟩))
    (eqToHom ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 1
⊢ X.hom =
    eqToHom ⋯ ≫
      (mk₁ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)))
            (X.map' 0 1 ⋯ ⋯ :
              X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 1)))).hom ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 1
⊢ (mk₁ X.hom).hom = eqToHom ⋯ ≫ X.hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G : ComposableArrows.{v_1, u_1} C n
F : ComposableArrows.{v_1, u_1} C 1
⊢ hom ((fun (f : Arrow.{v_1, u_1} C) ↦ mk₁ f.hom) ((fun (F : ComposableArrows.{v_1, u_1} C 1) ↦ Arrow.mk F.hom) F)) =
    eqToHom ⋯ ≫ F.hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
⊢ obj F X 0 = X

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
⊢ obj F X 1 = F.obj' 0 ⋯

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ obj F X (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) = F.obj' i ⋯

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
i : ℕ
hi : i + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ≤ ⟨j + 1, hj⟩
⊢ i ≤ j

Tactic:
simpa using hij
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ LE.le (α := Fin (n + 1 + 1)) 0 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ map F f 0 0 ⋯ = 𝟙 X

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.map, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ LE.le (α := Fin (n + 1 + 1)) 1 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ map F f 1 1 ⋯ = F.map (𝟙 ⟨0, ⋯⟩)

Tactic:
rfl

Premises used: CategoryTheory.homOfLE, CategoryTheory.ComposableArrows.Precomp.map, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ LE.le (α := Fin (n + 1 + 1)) 0 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ map F f 0 1 ⋯ = f

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.map, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ HAdd.hAdd (α := ℕ) 0 1 < n + 1 + 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ LE.le (α := Fin (n + 1 + 1)) 0 ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
⊢ map F f 0 (⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ : Fin (n + 1 + 1)) ⋯ = f

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.map, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 2 < n + 1 + 1
⊢ 0 ≤ (⟨j + 2, hj⟩ : Fin (n + 1 + 1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows.{v_1, u_1} C n
X : C
f : X ⟶ F.left
j : ℕ
hj : j + 2 < n + 1 + 1
⊢ map F f 0 (⟨j + 2, hj⟩ : Fin (n + 1 + 1)) ⋯ = f ≫ F.map' 0 (j + 1) ⋯ ⋯

Tactic:
rfl

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.Precomp.map, rfl