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 : ℕ
F G : ComposableArrows.{v_1, u_1} C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
i : ℕ
hi : i < n + 1 + 1
zero : ∀ (hi : 0 < n + 1 + 1), F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨0, hi⟩
succ : ∀ (i : ℕ) (hi : i + 1 < n + 1 + 1), F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i + 1, hi⟩
⊢ F.obj (⟨i, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i, hi⟩

Tactic:
rcases i with - | 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
hi : 0 < n + 1 + 1
⊢ F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
hi : 0 < n + 1 + 1
⊢ F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
i : ℕ
hi : i + 1 < n + 1 + 1
⊢ F.obj (⟨i + 1, hi⟩ : Fin (n + 1 + 1)) = G.obj ⟨i + 1, hi⟩

Tactic:
exact Functor.congr_obj h ⟨i, by valid⟩

Premises used: CategoryTheory.Functor.congr_obj, Fin.mk
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
⊢ ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i

Tactic:
have : ∀ i, F.obj i = G.obj i := by
    intro ⟨i, hi⟩
    rcases i with - | i
    · exact h₀
    · exact Functor.congr_obj h ⟨i, by valid⟩
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0)) ≫
      app' (Iso.hom (eqToIso h)) 0 ⋯ =
    Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 ⋯
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (F.map' 0 1 homMk₁._proof_2 ⋯ ≫ app' (Iso.hom (eqToIso h)) 0 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.δ₀.obj' 0 ⋯)
    (Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 ⋯ : F.obj' 0 ⋯ ⟶ G.obj ⟨1, ⋯⟩)

Tactic:
rw [w]
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
dsimp :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)))
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0)) ≫
      app' (Iso.hom (eqToIso h)) 0 ⋯ =
    Iso.hom (eqToIso h₀) ≫ G.map' 0 1 homMk₁._proof_2 ⋯

Tactic:
dsimp [app']

Premises used: CategoryTheory.ComposableArrows.app'
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
rw :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₁ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := F.obj 1)
          (CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
          (eqToHom ⋯) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₂ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1)
          (CategoryStruct.comp (Y := F.obj 1) (eqToHom ⋯) (eqToHom ⋯) : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₃ :
  Eq (α := F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ G.obj 1) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
rw₄ :
  eqToHom h₀ ≫
      CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (𝟙 (G.obj 1) : G.obj 1 ⟶ G.obj 1) =
    eqToHom h₀ ≫ G.map (homOfLE ⋯)
rw₅ rw₆ :
  Eq (α := F.obj 0 ⟶ G.obj 1) (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)
⊢ Eq (α := F.obj 0 ⟶ G.obj 1)
    (CategoryStruct.comp (Y := F.obj 1)
        (eqToHom h₀ ≫
          CategoryStruct.comp (Y := G.obj 1) (G.map (homOfLE ⋯) : G.obj 0 ⟶ G.obj 1) (eqToHom ⋯ : G.obj 1 ⟶ F.obj 1))
        (NatTrans.app (eqToHom h) 0) :
      F.obj 0 ⟶ G.obj 1)
    (eqToHom h₀ ≫ G.map (homOfLE ⋯) : F.obj 0 ⟶ G.obj 1)

Tactic:
rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.eqToHom_trans
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
hi : 0 < n + 1 + 1
⊢ Eq (α := F.obj (⟨0, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨0, hi⟩) ((isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨0, hi⟩)
    (eqToHom ⋯)

Tactic:
simp
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
n_1 : ℕ
hi : n_1 + 1 < n + 1 + 1
⊢ Eq (α := F.obj (⟨n_1 + 1, hi⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨n_1 + 1, hi⟩)
    ((isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨n_1 + 1, hi⟩) (eqToHom ⋯)

Tactic:
simp
-- 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)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w :
  Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom h₀ ≫
        CategoryStruct.comp (Y := G.obj ⟨1, ⋯⟩)
          (G.map' 0 1 homMk₁._proof_2 ⋯ : G.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ G.obj ⟨1, ⋯⟩)
          (eqToHom ⋯ : G.obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F = G

Tactic:
exact Functor.ext_of_iso (isoMkSucc (eqToIso h₀) (eqToIso h) (by
      rw [w]
      dsimp [app']
      rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id])) this
    (by rintro ⟨_ | _, hi⟩ <;> simp)

Premises used: CategoryTheory.eqToIso, CategoryTheory.ComposableArrows.isoMkSucc, CategoryTheory.Functor.ext_of_iso
-- 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 + 1)
⊢ F.δ₀ = (F.δ₀.precomp (X := F.obj ⟨0, ⋯⟩) (F.map' 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 + 1)
⊢ Eq (α := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (F.map' 0 1 homMk₁._proof_2 ⋯ : F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶ F.obj ⟨1, ⋯⟩)
    (eqToHom ⋯ ≫
        CategoryStruct.comp (Y := (F.δ₀.precomp (X := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1))) (F.map' 0 1 ⋯ ⋯)).obj ⟨1, ⋯⟩)
          ((F.δ₀.precomp (X := F.obj ⟨0, ⋯⟩) (F.map' 0 1 ⋯ ⋯)).map' 0 1 homMk₁._proof_2 ⋯ :
            (F.δ₀.precomp (X := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1))) (F.map' 0 1 ⋯ ⋯)).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶
              (F.δ₀.precomp (X := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1))) (F.map' 0 1 ⋯ ⋯)).obj ⟨1, ⋯⟩)
          (eqToHom ⋯ :
            (F.δ₀.precomp (X := F.obj (⟨0, ⋯⟩ : Fin (n + 1 + 1))) (F.map' 0 1 ⋯ ⋯)).obj (⟨1, ⋯⟩ : Fin (n + 1 + 1)) ⟶
              F.δ₀.obj 0) :
      F.obj' 0 ⋯ ⟶ F.δ₀.obj 0)

Tactic:
simp
-- 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 2
app₀ : f.obj' 0 _proof_7 ⟶ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ⟶ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ⟶ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_9
⊢ (homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀

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 2
app₀ : f.obj' 0 _proof_7 ⟶ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ⟶ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ⟶ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_9
⊢ (homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁

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 2
app₀ : f.obj' 0 _proof_7 ⟶ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ⟶ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ⟶ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_9
⊢ (homMk₂ app₀ app₁ app₂ w₀ w₁).app 2 = app₂

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 2
app₀ : f.obj' 0 _proof_7 ⟶ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ⟶ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ⟶ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_9
⊢ (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, homMk₂._proof_3⟩ = app₂

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 2
φ φ' : f ⟶ g
h₀ : app' φ 0 _proof_7 = app' φ' 0 _proof_7
h₁ : app' φ 1 _proof_8 = app' φ' 1 _proof_8
h₂ : app' φ 2 _proof_9 = app' φ' 2 _proof_9
⊢ φ = φ'

Tactic:
hom_ext_succ h₀ (hom_ext₁ h₁ h₂)

Premises used: CategoryTheory.ComposableArrows.hom_ext_succ, CategoryTheory.ComposableArrows.hom_ext₁
-- 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
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
rw :
  app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₁ :
  f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom ≫ app₁.inv = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₂ :
  f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ 𝟙 (f.obj' 1 _proof_8) =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₃ : f.map' 0 1 homMk₁._proof_2 _proof_8 = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
rw₄ rw₅ : f.map' 0 1 homMk₁._proof_2 _proof_8 = f.map' 0 1 homMk₁._proof_2 _proof_8
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8

Tactic:
rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.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 m : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 2
app₀ : f.obj' 0 _proof_7 ≅ g.obj' 0 _proof_7
app₁ : f.obj' 1 _proof_8 ≅ g.obj' 1 _proof_8
app₂ : f.obj' 2 _proof_9 ≅ g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_8
w₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
rw₁ : f.map' 1 2 _proof_8 _proof_9 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
rw₂ : f.map' 1 2 _proof_8 _proof_9 ≫ 𝟙 (f.obj' 2 _proof_9) = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
rw₃ : f.map' 1 2 _proof_8 _proof_9 = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
rw₄ rw₅ : f.map' 1 2 _proof_8 _proof_9 = f.map' 1 2 _proof_8 _proof_9
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9

Tactic:
rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.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
F G : ComposableArrows.{v_1, u_1} C 2
f : F ⟶ G
rw :
  (∀ (X : Fin (HAdd.hAdd (α := ℕ) 2 1)), IsIso (f.app X)) ↔
    IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)
⊢ IsIso f ↔ IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)

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 2
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
0 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
1 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
2 :
  IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
⊢ 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 2
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)
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 2) (f.app 2) →
        IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
          (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 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 2
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)
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 2) (f.app 2) →
        IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
          (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 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 2
f : F ⟶ G
h : IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)
2 h_1 h_2 :
  IsIso (X := F.obj 0) (f.app 0) →
    IsIso (X := F.obj 1) (f.app 1) →
      IsIso (X := F.obj 2) (f.app 2) →
        IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
          (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))

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 2
f : F ⟶ G
⊢ (∀ (X : Fin (HAdd.hAdd (α := ℕ) 2 1)), IsIso (f.app X)) ↔
    IsIso (X := F.obj 0) (f.app 0) ∧ IsIso (X := F.obj 1) (f.app 1) ∧ IsIso (X := F.obj 2) (f.app 2)

Tactic:
exact ⟨fun h ↦ ⟨h 0, h 1, h 2⟩, 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 2
h₀ : f.obj' 0 _proof_7 = g.obj' 0 _proof_7
h₁ : f.obj' 1 _proof_8 = g.obj' 1 _proof_8
h₂ : f.obj' 2 _proof_9 = g.obj' 2 _proof_9
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_8 = eqToHom h₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ eqToHom ⋯
w₁ : f.map' 1 2 _proof_8 _proof_9 = eqToHom h₁ ≫ g.map' 1 2 _proof_8 _proof_9 ≫ eqToHom ⋯
⊢ f = g

Tactic:
ext_succ h₀ (ext₁ h₁ h₂ w₁) w₀

Premises used: CategoryTheory.ComposableArrows.ext_succ, CategoryTheory.ComposableArrows.ext₁
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : ComposableArrows.{v_1, u_1} C 2
⊢ X.map' 0 1 homMk₁._proof_2 _proof_8 =
    eqToHom ⋯ ≫
      (mk₂ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).map'
          0 1 homMk₁._proof_2 _proof_8 ≫
        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 2
⊢ X.map' 1 2 _proof_8 _proof_9 =
    eqToHom ⋯ ≫
      (mk₂ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))).map'
          1 2 _proof_8 _proof_9 ≫
        eqToHom ⋯

Tactic:
simp