awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
have obtain : ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁),
  Epi π₂ →
    ∀ (y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) sorry n₁ n₂ sorry).sc sorry 0 sorry).X₁)
      (hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) sorry n₁ n₂ sorry).sc sorry 0 sorry).f),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry),
        π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry
Tactic: obtain ⟨A₂, π₂, _, y₁, hy₁⟩ :=
    ((X.sequenceΨ_exact f₂ f₃ f₄ f₂₃ h₂₃ _ rfl n₁ n₂).exact 0).exact_up_to_refinements y₂ hy₂'.symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : Eq (α := A ⟶ X.E f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯) (x₂ ≫ X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯) 0
A₁ : C
π₁ : A₁ ⟶ A
w : Epi π₁
y₂ : A₁ ⟶ X.cycles f₃ f₄ n₁
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.πE f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯
hy₂' : 0 = y₂ ≫ X.Ψ f₂ f₃ f₄ n₁ n₂ ⋯
A₂ : C
π₂ : A₂ ⟶ A₁
w_1 : Epi π₂
y₁ : A₂ ⟶ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).X₁
hy₁ : π₂ ≫ y₂ = y₁ ≫ ((X.sequenceΨ f₂ f₃ f₄ f₂₃ h₂₃ (f₃ ≫ f₄) ⋯ n₁ n₂ ⋯).sc ⋯ 0 ⋯).f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ X.E f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯),
    π ≫ x₂ = x₁ ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
have refine : (π₂ ≫ π₁) ≫ x₂ =
  (y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry) ≫ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry
Tactic: refine ⟨A₂, π₂ ≫ π₁, inferInstance, y₁ ≫ X.πE f₂₃ f₄ f₅ n₀ n₁ n₂, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Homology (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ i₆ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₆ : i₅ ⟶ i₆
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₅₆ : i₄ ⟶ i₆
h₅₆ : f₅ ≫ f₆ = f₅₆
n₁ n₂ n₃ : ℤ
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ ⋯ ⋯ ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯ ≫
      X.map f₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯)
    (X.map f₂₃ f₄ f₅ f₂₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ ⋯) n₁ n₂ n₃ ⋯ ⋯ ≫
      X.map f₂₃ f₄ f₅₆ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ ⋯) n₁ n₂ n₃ ⋯ ⋯)
have simp : Eq (α := X.E f₂₃ f₄ f₅ n₁ n₂ n₃ sorry sorry ⟶ X.E f₃ f₄ f₅₆ n₁ n₂ n₃ sorry sorry)
  (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ sorry ≫ fourδ₄Toδ₃ f₃ f₄ f₅ f₆ f₅₆ sorry) n₁ n₂ n₃ sorry sorry)
  (X.map f₂₃ f₄ f₅ f₃ f₄ f₅₆ (fourδ₄Toδ₃ f₂₃ f₄ f₅ f₆ f₅₆ sorry ≫ fourδ₁Toδ₀ f₂ f₃ f₄ f₅₆ f₂₃ sorry) n₁ n₂ n₃ sorry sorry)
Tactic: simp only [← map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
have h₁ : (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
  ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
⊢ X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
have h₂ : (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
  ShortComplex.Hom.τ₂ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
h₂ :
  (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
⊢ X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
have h₃ : (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
  ShortComplex.Hom.τ₃ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    ShortComplex.Hom.τ₁ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
have h₁ : (X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) sorry) = 𝟙 ((X.H n₀).obj (mk₁ f₃))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) ⋯) =
    𝟙 ((X.H n₀).obj (mk₁ f₃))
have h : homMk₁ (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 3)) sorry = 𝟙 (mk₁ f₃)
Tactic: convert! (X.H _).map_id _
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    ShortComplex.Hom.τ₂ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
have h₂ : (X.H n₁).map (homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) sorry) = 𝟙 ((X.H n₁).obj (mk₁ f₂))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) ⋯) = 𝟙 ((X.H n₁).obj (mk₁ f₂))
have h : homMk₁ (𝟙 j) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i 2)) sorry = 𝟙 (mk₁ f₂)
Tactic: convert! (X.H _).map_id _
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    ShortComplex.Hom.τ₃ (𝟙 (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯))
have h₃ : (X.H n₂).map (homMk₁ (𝟙 i) (𝟙 j) sorry) = 𝟙 ((X.H n₂).obj (mk₁ f₁))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₂).map (homMk₁ (𝟙 i) (𝟙 j) ⋯) = 𝟙 ((X.H n₂).obj (mk₁ f₁))
have h : homMk₁ (𝟙 i) (𝟙 j) sorry = 𝟙 (mk₁ f₁)
Tactic: convert! (X.H _).map_id _
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂
have h₁ : (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁
⊢ X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂
have h₂ : (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁
h₂ :
  (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂
⊢ X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂ =
    X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂
have h₃ : (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
  (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
      X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₁ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₁
have h₁ : Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
  ((X.H n₀).map
    (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) sorry))
  (CategoryStruct.comp (Y := (X.H n₀).obj (mk₁ f₃')) ((X.H n₀).map (homMk₁ (α.app 2) (α.app 3) sorry))
    ((X.H n₀).map (homMk₁ (β.app 2) (β.app 3) sorry)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₀).obj (mk₁ f₃')) ((X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯))
      ((X.H n₀).map (homMk₁ (β.app 2) (β.app 3) ⋯)))
have h₁ : Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
  ((X.H n₀).map
    (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) sorry))
  ((X.H n₀).map (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) sorry) (homMk₁ (β.app 2) (β.app 3) sorry)))
Tactic: rw [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₀).obj (mk₁ f₃) ⟶ (X.H n₀).obj (mk₁ f₃''))
    ((X.H n₀).map
      (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) ⋯))
    ((X.H n₀).map (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) ⋯) (homMk₁ (β.app 2) (β.app 3) ⋯)))
have h₁ : Eq.{v_2 + 1} (α := mk₁ f₃ ⟶ mk₁ f₃'')
  (homMk₁ (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2))
    (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 3) (α.app 3) (β.app 3)) sorry)
  (CategoryStruct.comp (Y := mk₁ f₃') (homMk₁ (α.app 2) (α.app 3) sorry) (homMk₁ (β.app 2) (β.app 3) sorry))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₂ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₂
have h₂ : Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
  ((X.H n₁).map
    (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) sorry))
  (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f₂')) ((X.H n₁).map (homMk₁ (α.app 1) (α.app 2) sorry))
    ((X.H n₁).map (homMk₁ (β.app 1) (β.app 2) sorry)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    (CategoryStruct.comp (Y := (X.H n₁).obj (mk₁ f₂')) ((X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯))
      ((X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)))
have h₂ : Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
  ((X.H n₁).map
    (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
      (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) sorry))
  ((X.H n₁).map (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) sorry) (homMk₁ (β.app 1) (β.app 2) sorry)))
Tactic: rw [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₁).obj (mk₁ f₂) ⟶ (X.H n₁).obj (mk₁ f₂''))
    ((X.H n₁).map
      (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) ⋯))
    ((X.H n₁).map (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) ⋯) (homMk₁ (β.app 1) (β.app 2) ⋯)))
have h₂ : Eq.{v_2 + 1} (α := mk₁ f₂ ⟶ mk₁ f₂'')
  (homMk₁ (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
    (CategoryStruct.comp (Y := Precomp.obj (mk₂ f₂' f₃') i' 2) (α.app 2) (β.app 2)) sorry)
  (CategoryStruct.comp (Y := mk₁ f₂') (homMk₁ (α.app 1) (α.app 2) sorry) (homMk₁ (β.app 1) (β.app 2) sorry))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (α ≫ β) n₀ n₁ n₂ hn₁ hn₂).τ₃ =
    (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂ ≫
        X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂).τ₃
have h₃ : Eq (α := (X.H n₂).obj (mk₁ f₁) ⟶ (X.H n₂).obj (mk₁ f₁''))
  ((X.H n₂).map
    (homMk₁ (CategoryStruct.comp (Y := i') (α.app 0) (β.app 0)) (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1)) sorry))
  (CategoryStruct.comp (Y := (X.H n₂).obj (mk₁ f₁')) ((X.H n₂).map (homMk₁ (α.app 0) (α.app 1) sorry))
    ((X.H n₂).map (homMk₁ (β.app 0) (β.app 1) sorry)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Page (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
i'' j'' k'' l'' : ι
f₁'' : i'' ⟶ j''
f₂'' : j'' ⟶ k''
f₃'' : k'' ⟶ l''
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α := (X.H n₂).obj (mk₁ f₁) ⟶ (X.H n₂).obj (mk₁ f₁''))
    ((X.H n₂).map
      (homMk₁ (CategoryStruct.comp (Y := i') (α.app 0) (β.app 0)) (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1))
        ⋯))
    (CategoryStruct.comp (Y := (X.H n₂).obj (mk₁ f₁')) ((X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯))
      ((X.H n₂).map (homMk₁ (β.app 0) (β.app 1) ⋯)))
have h₃ : Eq (α := (X.H n₂).obj (mk₁ f₁) ⟶ (X.H n₂).obj (mk₁ f₁''))
  ((X.H n₂).map
    (homMk₁ (CategoryStruct.comp (Y := i') (α.app 0) (β.app 0)) (CategoryStruct.comp (Y := j') (α.app 1) (β.app 1)) sorry))
  ((X.H n₂).map (CategoryStruct.comp (Y := mk₁ f₁') (homMk₁ (α.app 0) (α.app 1) sorry) (homMk₁ (β.app 0) (β.app 1) sorry)))
Tactic: rw [← Functor.map_comp]