awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_8 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_8
have rw₄ : f.map' 0 1 homMk₁._proof_2 _proof_8 = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
have 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
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
have 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
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
have 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
Tactic: rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id,
      comp_id, app₁.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
have rw₃ : f.map' 1 2 _proof_8 _proof_9 = app₁.hom ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 1 2 _proof_8 _proof_9 ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 _proof_8 _proof_9
have rw₄ : f.map' 1 2 _proof_8 _proof_9 = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : ComposableArrows.{v_1, u_1} C 2
f : F ⟶ G
⊢ 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)
have 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)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ IsIso (f.app i)
have 0 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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, ⋯⟩))
⊢ IsIso (f.app i)
have 1 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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, ⋯⟩))
⊢ IsIso (f.app i)
have 2 : IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩))
  (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
have 0 : 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, sorry⟩))
        (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, sorry⟩))
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
have 1 : 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, sorry⟩))
        (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, sorry⟩))
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ IsIso (X := F.obj ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
    (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
have 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, sorry⟩))
        (f.app ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, sorry⟩))
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ f = g
have 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
Tactic: obtain ⟨x₀, x₁, x₂, f, f', rfl⟩ := mk₂_surjective f
Cleared hypotheses: f, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = g
have 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'
Tactic: obtain ⟨y₀, y₁, y₂, g, g', rfl⟩ := mk₂_surjective g
Cleared hypotheses: g, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = mk₂ g g'
have 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'
Tactic: obtain rfl : x₀ = y₀ := congr_arg Arrow.leftFunc.obj h₀₁
Cleared hypotheses: y₀, g, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = mk₂ g g'
have 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'
Tactic: obtain rfl : x₁ = y₁ := congr_arg Arrow.rightFunc.obj h₀₁
Cleared hypotheses: y₁, g', g, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = mk₂ g g'
have 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'
Tactic: obtain rfl : x₂ = y₂ := congr_arg Arrow.rightFunc.obj h₁₂
Cleared hypotheses: y₂, g', h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ f = g
have rwa : Arrow.mk f = Arrow.mk g
Tactic: rwa [← Arrow.mk_inj]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = mk₂ g g'
have 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'
Tactic: obtain rfl : f = g := by rwa [← Arrow.mk_inj]
Cleared hypotheses: g, h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ f' = g'
have rwa : Arrow.mk f' = Arrow.mk g'
Tactic: rwa [← Arrow.mk_inj]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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)
⊢ mk₂ f f' = mk₂ f g'
have 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'
Tactic: obtain rfl : f' = g' := by rwa [← Arrow.mk_inj]
Cleared hypotheses: g', h₀₁, h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
have 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
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
have 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
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
have 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
Tactic: rw [← cancel_epi app₀.hom, ← reassoc_of% w₀, app₁.hom_inv_id,
      comp_id, app₀.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
have rw₃ : f.map' 0 1 homMk₁._proof_2 _proof_24 = app₀.hom ≫ 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
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
⊢ g.map' 0 1 homMk₁._proof_2 _proof_24 ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 homMk₁._proof_2 _proof_24
have rw₄ : f.map' 0 1 homMk₁._proof_2 _proof_24 = 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]