awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
w : C
h : P w
w_1 : S.obj w ⟶ T
⊢ P (mk w_1).left

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ P X.left ↔ ∃ (a : C), P a ∧ ∃ (b : S.obj a ⟶ T), mk b = X

Tactic:
exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
rw :
  EssentiallySmall.{w, w, max v₂ w}
    (CostructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) (Equivalence.inverse (equivSmallModel C) ⋙ S) T)
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (CostructuredArrow S T)

Tactic:
rw [← essentiallySmall_congr
    (CostructuredArrow.pre (equivSmallModel.{w} C).inverse S T).asEquivalence]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w}
    (CostructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) (Equivalence.inverse (equivSmallModel C) ⋙ S) T)

Tactic:
essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w}
    (CostructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) (Equivalence.inverse (equivSmallModel C) ⋙ S) T)

Tactic:
exact essentiallySmall_of_small_of_locallySmall _

Premises used: CategoryTheory.essentiallySmall_of_small_of_locallySmall
-- 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
i : ℕ
hi : i ≤ n
⊢ i < n + 1

Tactic:
lia
-- 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
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_2
⊢ i < n + 1

Tactic:
lia
-- 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
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_2
⊢ j < n + 1

Tactic:
lia
-- 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
i j : ℕ
hij : i ≤ j
hjn : j ≤ n
simp : i ≤ j
⊢ (⟨i, ⋯⟩ : Fin (n + 1)) ≤ ⟨j, ⋯⟩

Tactic:
simp only [Fin.mk_le_mk]

Premises used: Fin.mk_le_mk
-- 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
i j : ℕ
hij : i ≤ j
hjn : j ≤ n
⊢ i ≤ j

Tactic:
valid
-- 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
i : ℕ
hi : i ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i, ⋯⟩) (F.map' i i ⋯ hi : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨i, ⋯⟩)
    (𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj (⟨i, ⋯⟩ : Fin (n + 1)))

Tactic:
F.map_id _

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.homOfLE
-- 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
i j k : ℕ
hij : i ≤ j
hjk : j ≤ k
hk : k ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩) (F.map' i k ⋯ hk : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)
    (F.map' i j hij ⋯ ≫ F.map' j k hjk hk : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ F.obj ⟨k, ⋯⟩)

Tactic:
F.map_comp _ _

Premises used: CategoryTheory.homOfLE, CategoryTheory.Functor.map_comp
-- 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
φ : F ⟶ G
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ F.map' i j hij hj ≫ app' φ j hj = app' φ i ⋯ ≫ G.map' i j hij hj

Tactic:
φ.naturality _

Premises used: CategoryTheory.NatTrans.naturality
-- 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₁ : C
f : X₀ ⟶ X₁
i : Fin 2
⊢ i ≤ i

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i : Fin 2
⊢ map f i i ⋯ = 𝟙 (obj X₀ X₁ i)

Tactic:
match i with
    | 0 => rfl
    | 1 => rfl

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Mk₁.map_id._proof_1, CategoryTheory.CategoryStruct.id, _private.0.CategoryTheory.ComposableArrows.Mk₁.map_id.match_1, CategoryTheory.ComposableArrows.Mk₁.map, Eq, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ i = j ∨ j = k

Tactic:
lia
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
inl : ∀ (hij : i ≤ i) (hjk : i ≤ k), map f i k ⋯ = map f i i hij ≫ map f i k hjk
inr : ∀ (hjk : j ≤ j), map f i j ⋯ = map f i j hij ≫ map f j j hjk
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk

Tactic:
obtain rfl | rfl : i = j ∨ j = k := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
inl : map f i k ⋯ = 𝟙 (obj X₀ X₁ i) ≫ map f i k hjk
inl₁ inl₂ : map f i k ⋯ = map f i k hjk
⊢ map f i k ⋯ = map f i i hij ≫ map f i k hjk

Tactic:
rw [map_id, id_comp]

Premises used: CategoryTheory.ComposableArrows.Mk₁.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
inr : map f i j ⋯ = map f i j hij ≫ 𝟙 (obj X₀ X₁ j)
inr₁ inr₂ : map f i j ⋯ = map f i j hij
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk

Tactic:
rw [map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ComposableArrows.Mk₁.map_id
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
⊢ (⟨i, hi⟩ : Fin (n + 1)) ≤ ⟨j, hj⟩

Tactic:
have hij' := leOfHom hij
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
hij' : (⟨i, hi⟩ : Fin (n + 1)) ≤ ⟨j, hj⟩
⊢ i ≤ j

Tactic:
simp only [Fin.mk_le_mk] at hij'

Premises used: Fin.mk_le_mk
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
hij' : i ≤ j
obtain : ∀ (k : ℕ) (hk : i + k = j), F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij
⊢ F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij

Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest hij'

Premises used: Nat.le.dest
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
hij' : i ≤ j
k : ℕ
hk : i + k = j
⊢ F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij

Tactic:
exact this k i j hk (by valid)
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
suffices :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
suffices ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
        F.map' i j ≫ app _ = app _ ≫ G.map' i j by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      have hij' := leOfHom hij
      simp only [Fin.mk_le_mk] at hij'
      obtain ⟨k, hk⟩ := Nat.le.dest hij'
      exact this k i j hk (by valid)
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj : i + 0 = j
hj' : j ≤ n
⊢ i = j

Tactic:
simp only [add_zero] at hj

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj_1 : i + 0 = j
hj' : j ≤ n
hj : i = j
zero :
  ∀ (hj : i + 0 = i) (hj' : i ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
      (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)

Tactic:
obtain rfl := hj

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 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hj : i + 0 = i
hj' : i ≤ n
zero : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj'
zero₁ : 𝟙 (F.obj (⟨i, ⋯⟩ : Fin (n + 1))) ≫ app (⟨i, ⋯⟩ : Fin (n + 1)) = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj ⟨i, ⋯⟩)
zero₂ : app ⟨i, ⋯⟩ = app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ 𝟙 (G.obj (⟨i, ⋯⟩ : Fin (n + 1)))
zero₃ zero₄ : Eq.{v_1 + 1} (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩) (app ⟨i, ⋯⟩) (app ⟨i, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (F.map' i i ⋯ hj' ≫ app ⟨i, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i i ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, ⋯⟩)

Tactic:
rw [F.map'_self i, G.map'_self i, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.ComposableArrows.map'_self, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i j : ℕ
hj : i + (k + 1) = j
hj' : j ≤ n
succ :
  ∀ (hj_1 : i + k + 1 = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)

Tactic:
rw [← add_assoc] at hj

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i j : ℕ
hj_1 : i + (k + 1) = j
hj : i + k + 1 = j
hj' : j ≤ n
succ :
  ∀ (hj : i + (k + 1) = i + k + 1) (hj' : i + k + 1 ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
      (F.map' i (i + k + 1) ⋯ hj' ≫ app ⟨i + k + 1, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i (i + k + 1) ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨i + k + 1, ⋯⟩)
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)

Tactic:
subst hj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
hk :
  ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hj : i + (k + 1) = i + k + 1
hj' : i + k + 1 ≤ n
⊢ i + k < n

Tactic:
valid
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
zero zero₁ :
  ∀ (i j : ℕ) (hj : i + 0 = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
succ succ₁ :
  ∀ (k : ℕ)
    (hk :
      ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
        Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
          (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
          (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩))
    (i j : ℕ) (hj : i + (k + 1) = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
⊢ ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)

Tactic:
induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]

Premises used: CategoryTheory.Category.assoc, add_assoc, CategoryTheory.Category.comp_id, add_zero, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
dsimp : G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ (fun (i : Fin (n + 1)) ↦ (app i).inv) ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (n + 1)) ↦ (app i).inv) (⟨i, ⋯⟩ : Fin (n + 1)) ≫ F.map' i (i + 1) ⋯ hi

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w :
  ∀ (i : ℕ) (hi : i < n),
    F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.hom (app ⟨i, ⋯⟩) ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
rw :
  Iso.hom (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₁ :
  F.map' i (i + 1) ⋯ hi ≫ Iso.hom (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₂ :
  F.map' i (i + 1) ⋯ hi ≫ 𝟙 (F.obj (⟨i + 1, ⋯⟩ : Fin (n + 1))) =
    Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₃ : F.map' i (i + 1) ⋯ hi = Iso.hom (app ⟨i, ⋯⟩) ≫ Iso.inv (app (⟨i, ⋯⟩ : Fin (n + 1))) ≫ F.map' i (i + 1) ⋯ hi
rw₄ rw₅ : F.map' i (i + 1) ⋯ hi = F.map' i (i + 1) ⋯ hi
⊢ G.map' i (i + 1) ⋯ hi ≫ Iso.inv (app (⟨i + 1, ⋯⟩ : Fin (n + 1))) = Iso.inv (app ⟨i, ⋯⟩) ≫ F.map' i (i + 1) ⋯ hi

Tactic:
rw [← cancel_epi ((app _).hom), ← reassoc_of% (w i hi), Iso.hom_inv_id, comp_id,
      Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C n
h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi ≫ Iso.hom ((fun (i : Fin (n + 1)) ↦ (eqToIso ⋯ : F.obj i ≅ G.obj i)) ⟨i + 1, ⋯⟩) =
    Iso.hom ((fun (i : Fin (n + 1)) ↦ (eqToIso ⋯ : F.obj i ≅ G.obj i)) (⟨i, ⋯⟩ : Fin (n + 1))) ≫ G.map' i (i + 1) ⋯ hi

Tactic:
simp [w 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 0
f : F.obj' 0 homMk₀._proof_1 ⟶ G.obj' 0 homMk₀._proof_1
i : ℕ
hi : i < 0
⊢ F.map' i (i + 1) ⋯ hi ≫
      (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => f :
            F.obj i ⟶ G.obj i))
        ⟨i + 1, ⋯⟩ =
    (fun (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (match (motive := (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) → F.obj i ⟶ G.obj i) i with
            | ⟨0, isLt⟩ => f :
            F.obj i ⟶ G.obj i))
        (⟨i, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
simp at hi
-- 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
w : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 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 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
w :
  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, ⋯⟩))
⊢ φ.app i = φ'.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 ⟶ 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:
h