awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ Eq (α := (mk₂ f g).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨2, ⋯⟩)
    ((mk₂ f g).map' 2 2 ⋯ ⋯ : (mk₂ f g).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj ⟨2, ⋯⟩)
    (𝟙 ((mk₂ f g).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) :
      (mk₂ f g).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ (mk₂ f g).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 1 ⋯ ⋯ = f

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 1 2 ⋯ ⋯ = g

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 2 3 ⋯ ⋯ = h

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 3 ⋯ ⋯ = f ≫ g ≫ h

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).hom = f ≫ g ≫ h

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 0 2 ⋯ ⋯ = f ≫ g

Tactic:
dsimp
-- 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₀ X₁ X₂ X₃ X₄ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
h : X₂ ⟶ X₃
i : X₃ ⟶ X₄
⊢ (mk₃ f g h).map' 1 3 ⋯ ⋯ = g ≫ h

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n_1 m : ℕ
F G : ComposableArrows.{v_1, u_1} C n_1
n k l : ℕ
h : k + l ≤ n
x : Fin (l + 1)
i : ℕ
isLt : i < l + 1
⊢ k + i < n + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n_1 m : ℕ
F G : ComposableArrows.{v_1, u_1} C n_1
n k l : ℕ
h : k + l ≤ n
x x_1 : Fin (l + 1)
hij : x ⟶ x_1
⊢ (↑(match (motive := Fin (l + 1) → Fin (n + 1)) x with
        | ⟨i, isLt⟩ => (⟨k + i, ⋯⟩ : Fin (n + 1))) :
      ℕ) ≤
    (↑(match (motive := Fin (l + 1) → Fin (n + 1)) x_1 with
        | ⟨i, isLt⟩ => ⟨k + i, ⋯⟩) :
      ℕ)

Tactic:
simpa using (leOfHom hij)

Premises used: CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n k l i : ℕ
h : k + l ≤ n
R : ComposableArrows.{v_1, u_1} C n
h_1 : i ≤ l
⊢ (Functor.obj (natAddLEFunctor h) R).obj' i h_1 = R.obj' (k + i) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n k l i : ℕ
h : k + l ≤ n
R₁ R₂ : ComposableArrows.{v_1, u_1} C n
φ : R₁ ⟶ R₂
h_1 : i ≤ l
⊢ app' (Functor.map (natAddLEFunctor h) φ) i h_1 = app' φ (k + i) ⋯

Tactic:
rfl

Premises used: 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
f : X ⟶ F.left
⊢ (F.precomp f).δ₀ = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.whiskerLeft, 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_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
hi : 0 < n + 1
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i ⋯ :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i ⋯ :
                F.obj i ⟶ G.obj i))
            ⟨0, ⋯⟩ :
          F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, ⋯⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
          G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)

Tactic:
w

Premises used: Fin.succ
-- 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 (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
hi : 0 < n + 1
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (F.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i ⋯ :
              F.obj i ⟶ G.obj i))
          ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩ :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨0, ⋯⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i ⋯ :
                F.obj i ⟶ G.obj i))
            ⟨0, ⋯⟩ :
          F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, ⋯⟩)
        (G.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ hi :
          G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨HAdd.hAdd (α := ℕ) 0 1, ⋯⟩) :
      F.obj (⟨0, ⋯⟩ : Fin (n + 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
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i + 1 < n + 1
⊢ Eq (α := F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)
    (F.map' (i + 1) (i + 1 + 1) ⋯ hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i ⋯ :
              F.obj i ⟶ G.obj i))
          ⟨i + 1 + 1, ⋯⟩ :
      F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨i + 1, ⋯⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i ⋯ :
                F.obj i ⟶ G.obj i))
            ⟨i + 1, ⋯⟩ :
          F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, ⋯⟩)
        (G.map' (i + 1) (i + 1 + 1) ⋯ hi : G.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩) :
      F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)

Tactic:
naturality' β i (i + 1)

Premises used: Fin.succ, CategoryTheory.ComposableArrows.naturality', HAdd.hAdd, CategoryTheory.homOfLE, OfNat.ofNat
-- 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 (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i + 1 < n + 1
⊢ Eq (α := F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)
    (F.map' (i + 1) (i + 1 + 1) ⋯ hi ≫
        (fun (i : Fin (n + 1 + 1)) ↦
            (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
              | ⟨0, isLt⟩ => α
              | ⟨i.succ, hi⟩ => app' β i ⋯ :
              F.obj i ⟶ G.obj i))
          ⟨i + 1 + 1, ⋯⟩ :
      F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)
    (CategoryStruct.comp (Y := G.obj ⟨i + 1, ⋯⟩)
        ((fun (i : Fin (n + 1 + 1)) ↦
              (match (motive := (i : Fin (n + 1 + 1)) → F.obj i ⟶ G.obj i) i with
                | ⟨0, isLt⟩ => α
                | ⟨i.succ, hi⟩ => app' β i ⋯ :
                F.obj i ⟶ G.obj i))
            ⟨i + 1, ⋯⟩ :
          F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, ⋯⟩)
        (G.map' (i + 1) (i + 1 + 1) ⋯ hi : G.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩) :
      F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1 + 1, ⋯⟩)

Tactic:
exact naturality' β i (i + 1)

Premises used: CategoryTheory.ComposableArrows.naturality', HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ (homMkSucc α β w).app 0 = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ Eq (α := F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, hi⟩)
    ((homMkSucc α β w).app ⟨i + 1, hi⟩ : F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, hi⟩)
    (app' β i ⋯ : F.δ₀.obj' i ⋯ ⟶ G.δ₀.obj' i ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
w :
  ∀ (i : ℕ) (hi : i < n + 1 + 1),
    Eq (α := F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i, hi⟩) (f.app ⟨i, hi⟩) (g.app ⟨i, hi⟩)
⊢ f = g

Tactic:
ext ⟨i, hi⟩
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
i : ℕ
hi : i < n + 1 + 1
w : ∀ (hi : 0 < n + 1 + 1), Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) (f.app ⟨0, hi⟩) (g.app ⟨0, hi⟩)
w₁ :
  ∀ (i : ℕ) (hi : i + 1 < n + 1 + 1),
    Eq (α := F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, hi⟩) (f.app ⟨i + 1, hi⟩) (g.app ⟨i + 1, hi⟩)
⊢ Eq (α := F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i, hi⟩) (f.app ⟨i, hi⟩) (g.app ⟨i, hi⟩)

Tactic:
obtain _ | i := i
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
hi : 0 < n + 1 + 1
⊢ Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) (f.app ⟨0, hi⟩) (g.app ⟨0, hi⟩)

Tactic:
h₀
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
hi : 0 < n + 1 + 1
⊢ Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) (f.app ⟨0, hi⟩) (g.app ⟨0, hi⟩)

Tactic:
exact h₀
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
f g : F ⟶ G
h₀ : app' f 0 ⋯ = app' g 0 ⋯
h₁ : Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor G) (Functor.map δ₀Functor f) (Functor.map δ₀Functor g)
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ Eq (α := F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨i + 1, hi⟩) (f.app ⟨i + 1, hi⟩) (g.app ⟨i + 1, hi⟩)

Tactic:
exact congr_app h₁ ⟨i, by valid⟩

Premises used: Fin.mk, CategoryTheory.congr_app
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
rw :
  Eq (α := F.obj' 0 ⋯ ⟶ F.δ₀.obj' 0 ⋯)
    (CategoryStruct.comp (Y := F.obj ⟨1, ⋯⟩)
        (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
        (𝟙 (F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) : F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1)) ⟶ F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
⊢ Eq (α := G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (G.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.inv 0 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (α.inv ≫ F.map' 0 1 homMk₁._proof_2 ⋯ : G.obj' 0 ⋯ ⟶ F.obj ⟨1, ⋯⟩)

Tactic:
rw [← cancel_epi α.hom, ← reassoc_of% w, α.hom_inv_id_assoc, β.hom_inv_id_app]

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
dsimp :
  Eq (α := F.obj 0 ⟶ F.obj 1)
    (CategoryStruct.comp (Y := F.obj 1) (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1) (𝟙 (F.obj 1) : F.obj 1 ⟶ F.obj 1) :
      F.obj 0 ⟶ F.obj 1)
    (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1)
⊢ Eq (α := F.obj' 0 ⋯ ⟶ F.δ₀.obj' 0 ⋯)
    (CategoryStruct.comp (Y := F.obj ⟨1, ⋯⟩)
        (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
        (𝟙 (F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) : F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1)) ⟶ F.δ₀.obj (⟨0, ⋯⟩ : Fin (n + 1))) :
      F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)

Tactic:
dsimp
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
rw rw₁ : Eq (α := F.obj 0 ⟶ F.obj 1) (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1) (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1)
⊢ Eq (α := F.obj 0 ⟶ F.obj 1)
    (CategoryStruct.comp (Y := F.obj 1) (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1) (𝟙 (F.obj 1) : F.obj 1 ⟶ F.obj 1) :
      F.obj 0 ⟶ F.obj 1)
    (F.map (homOfLE ⋯) : F.obj 0 ⟶ F.obj 1)

Tactic:
rw [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
n m : ℕ
F_1 G_1 : ComposableArrows.{v_1, u_1} C n
F G : ComposableArrows.{v_1, u_1} C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
h₀ : app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) 0 ⋯ = app' (𝟙 F) 0 ⋯
h₁ :
  Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor F)
    (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯)) (Functor.map δ₀Functor (𝟙 F))
⊢ homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯ = 𝟙 F

Tactic:
apply hom_ext_succ

Premises used: CategoryTheory.ComposableArrows.hom_ext_succ
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ app' (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) 0 ⋯ = app' (𝟙 F) 0 ⋯

Tactic:
simp
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
h₁ :
  ∀ (i : ℕ) (hi : i < n + 1),
    Eq (α := (Functor.obj δ₀Functor F).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor F).obj ⟨i, hi⟩)
      (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯)) ⟨i, hi⟩)
      (NatTrans.app (Functor.map δ₀Functor (𝟙 F)) ⟨i, hi⟩)
⊢ Eq (α := Functor.obj δ₀Functor F ⟶ Functor.obj δ₀Functor F)
    (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯)) (Functor.map δ₀Functor (𝟙 F))

Tactic:
ext ⟨i, 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i < n + 1
⊢ Eq (α := (Functor.obj δ₀Functor F).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor F).obj ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯)) ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (𝟙 F)) ⟨i, hi⟩)

Tactic:
simp
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
h₀ : app' (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) 0 ⋯ = app' (𝟙 G) 0 ⋯
h₁ :
  Eq (α := Functor.obj δ₀Functor G ⟶ Functor.obj δ₀Functor G)
    (Functor.map δ₀Functor (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)) (Functor.map δ₀Functor (𝟙 G))
⊢ homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w = 𝟙 G

Tactic:
apply hom_ext_succ

Premises used: CategoryTheory.ComposableArrows.hom_ext_succ
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
⊢ app' (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) 0 ⋯ = app' (𝟙 G) 0 ⋯

Tactic:
simp
-- 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
h₁ :
  ∀ (i : ℕ) (hi : i < n + 1),
    Eq (α := (Functor.obj δ₀Functor G).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor G).obj ⟨i, hi⟩)
      (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)) ⟨i, hi⟩)
      (NatTrans.app (Functor.map δ₀Functor (𝟙 G)) ⟨i, hi⟩)
⊢ Eq (α := Functor.obj δ₀Functor G ⟶ Functor.obj δ₀Functor G)
    (Functor.map δ₀Functor (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)) (Functor.map δ₀Functor (𝟙 G))

Tactic:
ext ⟨i, 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 (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' β.hom 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (α.hom ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)
i : ℕ
hi : i < n + 1
⊢ Eq (α := (Functor.obj δ₀Functor G).obj (⟨i, hi⟩ : Fin (n + 1)) ⟶ (Functor.obj δ₀Functor G).obj ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w)) ⟨i, hi⟩)
    (NatTrans.app (Functor.map δ₀Functor (𝟙 G)) ⟨i, hi⟩)

Tactic:
simp