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 4
app₀ : f.obj' 0 _proof_47 ⟶ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ⟶ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ⟶ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ⟶ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ⟶ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_51
⊢ (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨4, homMk₄._proof_5⟩ = 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 4
φ φ' : f ⟶ g
h₀ : app' φ 0 _proof_47 = app' φ' 0 _proof_47
h₁ : app' φ 1 _proof_48 = app' φ' 1 _proof_48
h₂ : app' φ 2 _proof_49 = app' φ' 2 _proof_49
h₃ : app' φ 3 _proof_50 = app' φ' 3 _proof_50
h₄ : app' φ 4 _proof_51 = app' φ' 4 _proof_51
⊢ φ = φ'

Tactic:
hom_ext_succ h₀ (hom_ext₃ h₁ h₂ 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 : ℕ
h : n + 1 ≤ m
f g : ComposableArrows.{v_1, u_1} C m
app : f.obj' n ⋯ ≅ g.obj' n ⋯
app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h
w : f.map' n (n + 1) ⋯ h ≫ app'.hom = app.hom ≫ g.map' n (n + 1) ⋯ h
rw : app.hom ≫ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₁ : f.map' n (n + 1) ⋯ h ≫ app'.hom ≫ app'.inv = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₂ : f.map' n (n + 1) ⋯ h ≫ 𝟙 (f.obj' (n + 1) h) = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₃ : f.map' n (n + 1) ⋯ h = app.hom ≫ app.inv ≫ f.map' n (n + 1) ⋯ h
rw₄ rw₅ : f.map' n (n + 1) ⋯ h = f.map' n (n + 1) ⋯ h
⊢ g.map' n (n + 1) ⋯ h ≫ app'.inv = app.inv ≫ f.map' n (n + 1) ⋯ h

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 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
rw rw₁ : app₀.inv ≫ f.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_48
⊢ g.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_48

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
rw rw₁ : app₁.inv ≫ f.map' 1 (HAdd.hAdd (α := ℕ) 1 1) ⋯ ⋯ = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_49
⊢ g.map' 1 2 _proof_8 _proof_49 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_49

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
rw rw₁ : app₂.inv ≫ f.map' 2 (HAdd.hAdd (α := ℕ) 2 1) ⋯ ⋯ = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_50
⊢ g.map' 2 3 _proof_25 _proof_50 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_50

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
⊢ HAdd.hAdd (α := ℕ) 3 1 ≤ 4

Tactic:
valid
-- 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 4
app₀ : f.obj' 0 _proof_47 ≅ g.obj' 0 _proof_47
app₁ : f.obj' 1 _proof_48 ≅ g.obj' 1 _proof_48
app₂ : f.obj' 2 _proof_49 ≅ g.obj' 2 _proof_49
app₃ : f.obj' 3 _proof_50 ≅ g.obj' 3 _proof_50
app₄ : f.obj' 4 _proof_51 ≅ g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_48
w₁ : f.map' 1 2 _proof_8 _proof_49 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_49
w₂ : f.map' 2 3 _proof_25 _proof_50 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_50
w₃ : f.map' 3 4 _proof_50 _proof_51 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_51
rw rw₁ : app₃.inv ≫ f.map' 3 (HAdd.hAdd (α := ℕ) 3 1) ⋯ ⋯ = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_51
⊢ g.map' 3 4 _proof_50 _proof_51 ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_51

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 4
h₀ : f.obj' 0 _proof_47 = g.obj' 0 _proof_47
h₁ : f.obj' 1 _proof_48 = g.obj' 1 _proof_48
h₂ : f.obj' 2 _proof_49 = g.obj' 2 _proof_49
h₃ : f.obj' 3 _proof_50 = g.obj' 3 _proof_50
h₄ : f.obj' 4 _proof_51 = g.obj' 4 _proof_51
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_48 = eqToHom h₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_48 ≫ eqToHom ⋯
w₁ : f.map' 1 2 _proof_8 _proof_49 = eqToHom h₁ ≫ g.map' 1 2 _proof_8 _proof_49 ≫ eqToHom ⋯
w₂ : f.map' 2 3 _proof_25 _proof_50 = eqToHom h₂ ≫ g.map' 2 3 _proof_25 _proof_50 ≫ eqToHom ⋯
w₃ : f.map' 3 4 _proof_50 _proof_51 = eqToHom h₃ ≫ g.map' 3 4 _proof_50 _proof_51 ≫ eqToHom ⋯
⊢ f = g

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

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

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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ 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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ 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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ 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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨3, homMk₅._proof_4⟩ = 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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, homMk₅._proof_5⟩ = 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 5
app₀ : f.obj' 0 _proof_83 ⟶ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ⟶ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ⟶ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ⟶ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ⟶ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ⟶ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄ = app₃ ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅ = app₄ ≫ g.map' 4 5 _proof_87 _proof_88
⊢ (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨5, homMk₅._proof_6⟩ = 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 5
φ φ' : f ⟶ g
h₀ : app' φ 0 _proof_83 = app' φ' 0 _proof_83
h₁ : app' φ 1 _proof_84 = app' φ' 1 _proof_84
h₂ : app' φ 2 _proof_85 = app' φ' 2 _proof_85
h₃ : app' φ 3 _proof_86 = app' φ' 3 _proof_86
h₄ : app' φ 4 _proof_87 = app' φ' 4 _proof_87
h₅ : app' φ 5 _proof_88 = app' φ' 5 _proof_88
⊢ φ = φ'

Tactic:
hom_ext_succ h₀ (hom_ext₄ h₁ h₂ h₃ h₄ h₅)

Premises used: CategoryTheory.ComposableArrows.hom_ext₄, 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 G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
rw rw₁ : app₀.inv ≫ f.map' 0 (HAdd.hAdd (α := ℕ) 0 1) ⋯ ⋯ = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_84
⊢ g.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_84

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₀ app₁ w₀]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
rw rw₁ : app₁.inv ≫ f.map' 1 (HAdd.hAdd (α := ℕ) 1 1) ⋯ ⋯ = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_85
⊢ g.map' 1 2 _proof_8 _proof_85 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_85

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₁ app₂ w₁]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
rw rw₁ : app₂.inv ≫ f.map' 2 (HAdd.hAdd (α := ℕ) 2 1) ⋯ ⋯ = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_86
⊢ g.map' 2 3 _proof_25 _proof_86 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_86

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₂ app₃ w₂]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'
-- 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 5
app₀ : f.obj' 0 _proof_83 ≅ g.obj' 0 _proof_83
app₁ : f.obj' 1 _proof_84 ≅ g.obj' 1 _proof_84
app₂ : f.obj' 2 _proof_85 ≅ g.obj' 2 _proof_85
app₃ : f.obj' 3 _proof_86 ≅ g.obj' 3 _proof_86
app₄ : f.obj' 4 _proof_87 ≅ g.obj' 4 _proof_87
app₅ : f.obj' 5 _proof_88 ≅ g.obj' 5 _proof_88
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_84 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_84
w₁ : f.map' 1 2 _proof_8 _proof_85 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_85
w₂ : f.map' 2 3 _proof_25 _proof_86 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_86
w₃ : f.map' 3 4 _proof_50 _proof_87 ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_50 _proof_87
w₄ : f.map' 4 5 _proof_87 _proof_88 ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_87 _proof_88
rw rw₁ : app₃.inv ≫ f.map' 3 (HAdd.hAdd (α := ℕ) 3 1) ⋯ ⋯ = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_87
⊢ g.map' 3 4 _proof_50 _proof_87 ≫ app₄.inv = app₃.inv ≫ f.map' 3 4 _proof_50 _proof_87

Tactic:
rw [map'_inv_eq_inv_map' (by valid) app₃ app₄ w₃]

Premises used: CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'