awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Augment (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
C : CochainComplex.{v, u, 0} V ℕ
i j : ℕ
succ :
  (ComplexShape.up ℕ).Rel 0 (j + 1 + 1) →
    Eq.{v + 1} (α := C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X 0)
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) 0 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d 0 (j + 1 + 1)) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d 0 (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X 0 ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    Eq.{v + 1} (α := C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      ((match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x) i with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) ≫
          ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).d i (j + 1 + 1) :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d i (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X i ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) ⋯).X (j + 1 + 1))
have succ₁ : ∀ (i : ℕ),
  (ComplexShape.up ℕ).Rel (i + 1) (j + 1 + 1) →
    Eq.{v + 1} (α := C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (j + 1 + 1))
      (CategoryStruct.comp (Y := ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (i + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x)
            i + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)))
          (((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).d (i + 1) (j + 1 + 1)) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (j + 1 + 1))
      (CategoryStruct.comp (Y := C.X (j + 1 + 1)) (C.d (i + 1) (j + 1 + 1))
          (match (motive := (x : ℕ) → C.X x ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X x)
            j + 1 + 1 with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1))) :
        C.X (i + 1) ⟶ ((Functor.obj truncate C).augment (X := C.X 0) (C.d 0 1) sorry).X (j + 1 + 1))
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) 0
have rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
Tactic: rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) 0
have rw₁ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
Tactic: rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
h₁ : ¬c₁.Rel i₁ i₁'
i₂ : I₂
rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
rw₁ :
  Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) 0
have rw₂ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁')).obj (K₂.X i₂)) 0 0
Tactic: rw [K₁.shape _ _ h₁, Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : ¬c₂.Rel i₂ i₂'
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0
have rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂')) ((F.obj (K₁.X i₁)).map 0) 0
Tactic: rw [K₂.shape _ _ h₂, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' : I₂
h₂ : ¬c₂.Rel i₂ i₂'
rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂')) ((F.obj (K₁.X i₁)).map 0) 0
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0
have rw₁ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂')) 0 0
Tactic: rw [K₂.shape _ _ h₂, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
have rw : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
  ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
Tactic: rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
          Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
have rw₁ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
  ((F.map (K₁.d i₁ i₁' ≫ K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
Tactic: rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
          Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₁ :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁' ≫ K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
have rw₂ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
Tactic: rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
          Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₁ :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁' ≫ K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₂ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
have rw₃ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
Tactic: rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
          Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁') ≫ F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₁ :
  Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁' ≫ K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
rw₂ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app (F.map 0) (K₂.X i₂)) 0
rw₃ :
  Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) (NatTrans.app 0 (K₂.X i₂)) 0
⊢ Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂))
    ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂)) 0
have rw₄ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁'')).obj (K₂.X i₂)) 0 0
Tactic: rw [← NatTrans.comp_app, ← Functor.map_comp, HomologicalComplex.d_comp_d,
          Functor.map_zero, zero_app]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' i₂'' : I₂
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0
have rw : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂' ≫ K₂.d i₂' i₂'') = 0
Tactic: rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' i₂'' : I₂
rw : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂' ≫ K₂.d i₂' i₂'') = 0
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0
have rw₁ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂'')) ((F.obj (K₁.X i₁)).map 0) 0
Tactic: rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ : I₁
i₂ i₂' i₂'' : I₂
rw : (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂' ≫ K₂.d i₂' i₂'') = 0
rw₁ : Eq (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂'')) ((F.obj (K₁.X i₁)).map 0) 0
⊢ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0
have rw₂ : Eq.{v_3 + 1} (α := (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (F.obj (K₁.X i₁)).obj (K₂.X i₂'')) 0 0
Tactic: rw [← Functor.map_comp, HomologicalComplex.d_comp_d, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
i₁ i₁' : I₁
i₂ i₂' : I₂
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
    (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂')
have rw : (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
  (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂')
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ K₂' : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
φ : K₂ ⟶ K₂'
i₁ i₁' : I₁
i₂ : I₂
h : c₁.Rel i₁ i₁'
⊢ (F.obj (K₁.X i₁)).map (φ.f i₂) ≫ (F.map (K₁.d i₁ i₁')).app (K₂'.X i₂) =
    (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)
have rw : (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂) =
  (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (φ.f i₂)
Tactic: rw [NatTrans.naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Bifunctor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
inst_3 : HasZeroMorphisms.{v_1, u_1} C₁
inst_4 : HasZeroMorphisms.{v_2, u_2} C₂
inst_5 : HasZeroMorphisms.{v_3, u_3} D
F : C₁ ⥤ Functor.{v_2, v_3, u_2, u_3} C₂ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst_6 : F.PreservesZeroMorphisms
inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ : HomologicalComplex.{v_1, u_1, u_4} C₁ c₁
K₂ : HomologicalComplex.{v_2, u_2, u_5} C₂ c₂
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex₂.{v_3, u_3, u_4, u_5} D c₁ c₂)
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯)
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
    (HomologicalComplex₂.homMk (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) ⋯
      ⋯)
    (𝟙
      (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
        (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
        (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) ⋯ ⋯ ⋯ ⋯ ⋯))
have h : ∀ (i : I₁) (i_1 : I₂),
  Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) sorry sorry sorry sorry sorry)
          i)
        i_1 ⟶
      HomologicalComplex.X.{v_3, u_3, u_5}
        (HomologicalComplex.X
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) sorry sorry sorry sorry sorry)
          i)
        i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (HomologicalComplex₂.homMk
          (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).map (HomologicalComplex.Hom.f (𝟙 K₂))) sorry sorry)
        i)
      i_1)
    (HomologicalComplex.Hom.f
      (HomologicalComplex.Hom.f
        (𝟙
          (HomologicalComplex₂.ofGradedObject c₁ c₂ (((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X)
            (fun (i₁ i₁' : I₁) (i₂ : I₂) ↦ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂))
            (fun (i₁ : I₁) (i₂ i₂' : I₂) ↦ (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) sorry sorry sorry sorry sorry))
        i)
      i_1)
Tactic: ext