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 2
h₀₁ : Arrow.mk (f.map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk (g.map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk (f.map' 1 2 _proof_8 _proof_9) = Arrow.mk (g.map' 1 2 _proof_8 _proof_9)
obtain :
  ∀ (x₀ x₁ x₂ : C) (f : x₀ ⟶ x₁) (f' : x₁ ⟶ x₂)
    (h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk (g.map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk (g.map' 1 2 _proof_8 _proof_9)), mk₂ f f' = g
⊢ f = g

Tactic:
obtain ⟨x₀, x₁, x₂, f, f', rfl⟩ := mk₂_surjective f

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
g : ComposableArrows.{v_1, u_1} C 2
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk (g.map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk (g.map' 1 2 _proof_8 _proof_9)
obtain :
  ∀ (y₀ y₁ y₂ : C) (g : y₀ ⟶ y₁) (g' : y₁ ⟶ y₂)
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ g g'
⊢ mk₂ f f' = g

Tactic:
obtain ⟨y₀, y₁, y₂, g, g', rfl⟩ := mk₂_surjective g

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₀ y₁ y₂ : C
g : y₀ ⟶ y₁
g' : y₁ ⟶ y₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
⊢ x₀ = y₀

Tactic:
congr_arg Arrow.leftFunc.obj h₀₁

Premises used: CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₀ y₁ y₂ : C
g : y₀ ⟶ y₁
g' : y₁ ⟶ y₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
obtain :
  ∀ (g : x₀ ⟶ y₁)
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ g g'
⊢ mk₂ f f' = mk₂ g g'

Tactic:
obtain rfl : x₀ = y₀ := congr_arg Arrow.leftFunc.obj h₀₁

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₁ y₂ : C
g' : y₁ ⟶ y₂
g : x₀ ⟶ y₁
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
⊢ x₁ = y₁

Tactic:
congr_arg Arrow.rightFunc.obj h₀₁

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, congr_arg, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₁ y₂ : C
g' : y₁ ⟶ y₂
g : x₀ ⟶ y₁
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
obtain :
  ∀ (g' : x₁ ⟶ y₂) (g : x₀ ⟶ x₁)
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ g g'
⊢ mk₂ f f' = mk₂ g g'

Tactic:
obtain rfl : x₁ = y₁ := congr_arg Arrow.rightFunc.obj h₀₁

Premises used: congr_arg, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₂ : C
g' : x₁ ⟶ y₂
g : x₀ ⟶ x₁
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
⊢ x₂ = y₂

Tactic:
congr_arg Arrow.rightFunc.obj h₁₂

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.ComposableArrows.Precomp.obj, congr_arg, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
y₂ : C
g' : x₁ ⟶ y₂
g : x₀ ⟶ x₁
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
obtain :
  ∀ (g' : x₁ ⟶ x₂)
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ g g'
⊢ mk₂ f f' = mk₂ g g'

Tactic:
obtain rfl : x₂ = y₂ := congr_arg Arrow.rightFunc.obj h₁₂

Premises used: congr_arg, CategoryTheory.Arrow.rightFunc, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
rwa rwa₁ rwa₂ rwa₃ : Arrow.mk f = Arrow.mk g
⊢ f = g

Tactic:
rwa [← Arrow.mk_inj]

Premises used: CategoryTheory.Arrow.mk_inj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
g : x₀ ⟶ x₁
g' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ g g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ g g').map' 1 2 _proof_8 _proof_9)
obtain :
  ∀
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ f g'
⊢ mk₂ f f' = mk₂ g g'

Tactic:
obtain rfl : f = g := by rwa [← Arrow.mk_inj]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_8 _proof_9)
rwa rwa₁ rwa₂ rwa₃ : Arrow.mk f' = Arrow.mk g'
⊢ f' = g'

Tactic:
rwa [← Arrow.mk_inj]

Premises used: CategoryTheory.Arrow.mk_inj
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' g' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ f g').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ f g').map' 1 2 _proof_8 _proof_9)
obtain :
  ∀
    (h₀₁ :
      Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8))
    (h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9)),
    mk₂ f f' = mk₂ f f'
⊢ mk₂ f f' = mk₂ f g'

Tactic:
obtain rfl : f' = g' := by rwa [← Arrow.mk_inj]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x₀ x₁ x₂ : C
f : x₀ ⟶ x₁
f' : x₁ ⟶ x₂
h₀₁ : Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8) = Arrow.mk ((mk₂ f f').map' 0 1 homMk₁._proof_2 _proof_8)
h₁₂ : Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9) = Arrow.mk ((mk₂ f f').map' 1 2 _proof_8 _proof_9)
⊢ mk₂ f f' = mk₂ f f'

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.ComposableArrows.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ⟶ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ⟶ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ⟶ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ⟶ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_26
⊢ (homMk₃ app₀ app₁ app₂ app₃ 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 3
app₀ : f.obj' 0 _proof_23 ⟶ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ⟶ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ⟶ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ⟶ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_26
⊢ (homMk₃ app₀ app₁ app₂ app₃ 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 3
app₀ : f.obj' 0 _proof_23 ⟶ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ⟶ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ⟶ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ⟶ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_26
⊢ (homMk₃ app₀ app₁ app₂ app₃ 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 3
app₀ : f.obj' 0 _proof_23 ⟶ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ⟶ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ⟶ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ⟶ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁ = app₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂ = app₁ ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃ = app₂ ≫ g.map' 2 3 _proof_25 _proof_26
⊢ (homMk₃ app₀ app₁ app₂ app₃ 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 3
φ φ' : f ⟶ g
h₀ : app' φ 0 _proof_23 = app' φ' 0 _proof_23
h₁ : app' φ 1 _proof_24 = app' φ' 1 _proof_24
h₂ : app' φ 2 _proof_25 = app' φ' 2 _proof_25
h₃ : app' φ 3 _proof_26 = app' φ' 3 _proof_26
⊢ φ = φ'

Tactic:
hom_ext_succ h₀ (hom_ext₂ 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 : ℕ
F G : ComposableArrows.{v_1, u_1} C n
f g : ComposableArrows.{v_1, u_1} C 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw :
  app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
rw₁ :
  f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom ≫ app₁.inv =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
rw₂ :
  f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ 𝟙 (f.obj' 1 _proof_24) =
    app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
rw₃ : f.map' 0 1 homMk₁._proof_2 _proof_24 = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
rw₄ rw₅ : f.map' 0 1 homMk₁._proof_2 _proof_24 = f.map' 0 1 homMk₁._proof_2 _proof_24
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24

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 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom ≫ app₂.inv = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₂ : f.map' 1 2 _proof_8 _proof_25 ≫ 𝟙 (f.obj' 2 _proof_25) = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₃ : f.map' 1 2 _proof_8 _proof_25 = app₁.hom ≫ app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25
rw₄ rw₅ : f.map' 1 2 _proof_8 _proof_25 = f.map' 1 2 _proof_8 _proof_25
⊢ g.map' 1 2 _proof_8 _proof_25 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_25

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 3
app₀ : f.obj' 0 _proof_23 ≅ g.obj' 0 _proof_23
app₁ : f.obj' 1 _proof_24 ≅ g.obj' 1 _proof_24
app₂ : f.obj' 2 _proof_25 ≅ g.obj' 2 _proof_25
app₃ : f.obj' 3 _proof_26 ≅ g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_2 _proof_24
w₁ : f.map' 1 2 _proof_8 _proof_25 ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_8 _proof_25
w₂ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26
rw : app₂.hom ≫ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₁ : f.map' 2 3 _proof_25 _proof_26 ≫ app₃.hom ≫ app₃.inv = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₂ : f.map' 2 3 _proof_25 _proof_26 ≫ 𝟙 (f.obj' 3 _proof_26) = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₃ : f.map' 2 3 _proof_25 _proof_26 = app₂.hom ≫ app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26
rw₄ rw₅ : f.map' 2 3 _proof_25 _proof_26 = f.map' 2 3 _proof_25 _proof_26
⊢ g.map' 2 3 _proof_25 _proof_26 ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 _proof_25 _proof_26

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 3
h₀ : f.obj' 0 _proof_23 = g.obj' 0 _proof_23
h₁ : f.obj' 1 _proof_24 = g.obj' 1 _proof_24
h₂ : f.obj' 2 _proof_25 = g.obj' 2 _proof_25
h₃ : f.obj' 3 _proof_26 = g.obj' 3 _proof_26
w₀ : f.map' 0 1 homMk₁._proof_2 _proof_24 = eqToHom h₀ ≫ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ eqToHom ⋯
w₁ : f.map' 1 2 _proof_8 _proof_25 = eqToHom h₁ ≫ g.map' 1 2 _proof_8 _proof_25 ≫ eqToHom ⋯
w₂ : f.map' 2 3 _proof_25 _proof_26 = eqToHom h₂ ≫ g.map' 2 3 _proof_25 _proof_26 ≫ eqToHom ⋯
⊢ f = g

Tactic:
ext_succ h₀ (ext₂ h₁ h₂ h₃ w₁ 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 3
⊢ X.map' 0 1 homMk₁._proof_2 _proof_24 =
    eqToHom ⋯ ≫
      (mk₃ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))).map'
          0 1 homMk₁._proof_2 _proof_24 ≫
        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 3
⊢ X.map' 1 2 _proof_8 _proof_25 =
    eqToHom ⋯ ≫
      (mk₃ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))).map'
          1 2 _proof_8 _proof_25 ≫
        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 3
⊢ X.map' 2 3 _proof_25 _proof_26 =
    eqToHom ⋯ ≫
      (mk₃ (X₀ := X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1))) (X₁ := X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X₂ := X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 0 1 ⋯ ⋯ :
                X.obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 1 2 ⋯ ⋯ :
                X.obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))
              (X.map' 2 3 ⋯ ⋯ :
                X.obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶ X.obj (⟨3, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))).map'
          2 3 _proof_25 _proof_26 ≫
        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 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 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 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 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 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 ⟨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 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 ⟨3, homMk₄._proof_4⟩ = app₃

Tactic:
rfl

Premises used: rfl