awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.WithZero (goal)
Goal:
M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst : MulZeroOneClass M₀
inst_1 : Nontrivial M₀
inst_2 : NoZeroDivisors M₀
inst_3 : MulZeroOneClass N₀
inst_4 : MulZeroOneClass G₀
inst_5 : DecidablePred fun (x : M₀) ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
hx : x ≠ 0
inr : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) ((1 : (a : M₀) → G₀) x : G₀)
inr₁ : Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) 1 : G₀) (1 : G₀)
⊢ Eq.{u_3 + 1} (α := G₀) ((f : (a : N₀) → G₀) ((1 : (a : M₀) → N₀) x : N₀) : G₀) ((1 : (a : M₀) → G₀) x : G₀)
have inr₂ : Eq.{u_3 + 1} (α := G₀) 1 1
Tactic: rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j : ι
w : ¬c.Rel i j
⊢ F.map (C.d i j) = 0
have rw : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X j)) (F.map 0) 0
Tactic: rw [C.shape _ _ w, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j : ι
w : ¬c.Rel i j
rw : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X j)) (F.map 0) 0
⊢ F.map (C.d i j) = 0
have rw₁ : Eq.{v_3 + 1} (α := F.obj (C.X i) ⟶ F.obj (C.X j)) 0 0
Tactic: rw [C.shape _ _ w, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0
have rw : F.map (C.d i j ≫ C.d j k) = 0
Tactic: rw [← F.map_comp, C.d_comp_d, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
rw : F.map (C.d i j ≫ C.d j k) = 0
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0
have rw₁ : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X k)) (F.map 0) 0
Tactic: rw [← F.map_comp, C.d_comp_d, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C_1 D : HomologicalComplex.{v, u, u_1} V c_1
f : C_1 ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex.{v_2, u_3, u_1} W₁ c
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
rw : F.map (C.d i j ≫ C.d j k) = 0
rw₁ : Eq (α := F.obj (C.X i) ⟶ F.obj (C.X k)) (F.map 0) 0
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0
have rw₂ : Eq.{v_3 + 1} (α := F.obj (C.X i) ⟶ F.obj (C.X k)) 0 0
Tactic: rw [← F.map_comp, C.d_comp_d, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
⊢ Eq (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂)
      (HomologicalComplex.X.{v_3, u_4, u_1} (c := c)
        { X := fun (i : ι) ↦ F.obj (X.X i), d := fun (i j : ι) ↦ F.map (X.d i j), shape := ⋯, d_comp_d' := ⋯ } i)
      (HomologicalComplex.X.{v_3, u_4, u_1} (c := c)
        { X := fun (i : ι) ↦ F.obj (Y.X i), d := fun (i j : ι) ↦ F.map (Y.d i j), shape := ⋯, d_comp_d' := ⋯ } j))
    (F.map (f.f i) ≫
      d { X := fun (i : ι) ↦ F.obj (Y.X i), d := fun (i j : ι) ↦ F.map (Y.d i j), shape := ⋯, d_comp_d' := ⋯ } i j)
    (d { X := fun (i : ι) ↦ F.obj (X.X i), d := fun (i j : ι) ↦ F.map (X.d i j), shape := ⋯, d_comp_d' := ⋯ } i j ≫
      F.map (f.f j))
have dsimp : F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
⊢ F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
have rw : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
Tactic: rw [← F.map_comp, ← F.map_comp, f.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
rw : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
⊢ F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
have rw₁ : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j ≫ f.f j)
Tactic: rw [← F.map_comp, ← F.map_comp, f.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
c : ComplexShape ι
X Y : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : X ⟶ Y
i j : ι
h : c.Rel i j
rw : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
rw₁ : F.map (f.f i ≫ Y.d i j) = F.map (X.d i j ≫ f.f j)
⊢ F.map (f.f i) ≫ F.map (Y.d i j) = F.map (X.d i j) ≫ F.map (f.f j)
have rw₂ : F.map (X.d i j ≫ f.f j) = F.map (X.d i j ≫ f.f j)
Tactic: rw [← F.map_comp, ← F.map_comp, f.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
⊢ IsIso f
have this : ∀ (n : ι), IsIso (F.map (f.f n))
Tactic: haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
        ((HomologicalComplex.eval W₂ c n).mapIso
          (asIso ((F.mapHomologicalComplex c).map f))).isIso_hom
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (hypothesis)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
this : ∀ (n : ι), IsIso (F.map (f.f n))
⊢ IsIso f
have this₁ : ∀ (n : ι), IsIso (f.f n)
Tactic: haveI := fun n => isIso_of_reflects_iso (f.f n) F
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
α : Type u_5
inst_8 : AddRightCancelSemigroup α
inst_9 : One α
inst_10 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_11 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ Eq.{v_3 + 1} (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (CategoryStruct.comp (Y := (fun (n : α) ↦ F.obj (X n)) (n + 1)) ((fun (n : α) ↦ F.map (d n)) (n + 1))
      ((fun (n : α) ↦ F.map (d n)) n))
    0
have rw : F.map (d (n + 1) ≫ d n) = 0
Tactic: rw [← F.map_comp, sq n, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
α : Type u_5
inst_8 : AddRightCancelSemigroup α
inst_9 : One α
inst_10 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_11 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
rw : F.map (d (n + 1) ≫ d n) = 0
⊢ Eq.{v_3 + 1} (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (CategoryStruct.comp (Y := (fun (n : α) ↦ F.obj (X n)) (n + 1)) ((fun (n : α) ↦ F.map (d n)) (n + 1))
      ((fun (n : α) ↦ F.map (d n)) n))
    0
have rw₁ : Eq (α := Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
  (F.map 0) 0
Tactic: rw [← F.map_comp, sq n, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
α : Type u_5
inst_8 : AddRightCancelSemigroup α
inst_9 : One α
inst_10 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_11 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
rw : F.map (d (n + 1) ≫ d n) = 0
rw₁ :
  Eq (α := Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (F.map 0) 0
⊢ Eq.{v_3 + 1} (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (CategoryStruct.comp (Y := (fun (n : α) ↦ F.obj (X n)) (n + 1)) ((fun (n : α) ↦ F.map (d n)) (n + 1))
      ((fun (n : α) ↦ F.map (d n)) n))
    0
have rw₂ : Eq.{v_3 + 1} (α :=
  Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n)) 0 0
Tactic: rw [← F.map_comp, sq n, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
α : Type u_5
inst_4 : AddRightCancelSemigroup α
inst_5 : One α
inst_6 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_7 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ Eq (α := HomologicalComplex.{v_3, u_4, u_5} W₂ (ComplexShape.down α))
    (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq))
    (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯)
have refine : ∀ (i j : α),
  (ComplexShape.down α).Rel i j →
    Eq (α :=
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) i ⟶
        HomologicalComplex.X.{v_3, u_4, u_5} (c := ComplexShape.down α)
          (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) sorry) j)
      (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) i j ≫ eqToHom sorry)
      (eqToHom sorry ≫ HomologicalComplex.d (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) sorry) i j)
Tactic: refine HomologicalComplex.ext rfl ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W_1 : Type u_2
inst_2 : Category.{v_1, u_2} W_1
inst_3 : Preadditive.{v_1, u_2} W_1
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f_1 : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
W : Type u_5
inst_10 : Category.{v_4, u_5} W
inst_11 : Preadditive.{v_4, u_5} W
inst_12 : HasZeroObject.{v_4, u_5} W
inst_13 : DecidableEq ι
j : ι
x x_1 : W
f g : x ⟶ x_1
⊢ CategoryTheory.Functor.map (single W c j) (f + g) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := HomologicalComplex.{v_4, u_5, u_1} W c) (Functor.obj (single W c j) x)
        (Functor.obj (single W c j) x_1))
      (CategoryTheory.Functor.map (single W c j) f) (CategoryTheory.Functor.map (single W c j) g)
have hfg : Hom.f (CategoryTheory.Functor.map (single W c j) (f + g)) j =
  (HAdd.hAdd (α :=
        Quiver.Hom (V := HomologicalComplex.{v_4, u_5, u_1} W c) (Functor.obj (single W c j) x)
          (Functor.obj (single W c j) x_1))
        (CategoryTheory.Functor.map (single W c j) f) (CategoryTheory.Functor.map (single W c j) g)).f
    j
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
      (Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
    (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) X)
      { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }
      { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ })
    (𝟙
      (Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
have h : ∀ (i : ι),
  Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i)
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) X)
        { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry }
        { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry })
      i)
    (Hom.f
      (𝟙
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
      i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i ⟶
      HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i)
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) X)
        { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }
        { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ })
      i)
    (Hom.f
      (𝟙
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
      i)
have h : Eq.{v_3 + 1} (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
  (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
    (if h : i = j then eqToHom sorry else 0) (if h : i = j then eqToHom sorry else 0))
  (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
      (if h : i = j then eqToHom ⋯ else 0) (if h : i = j then eqToHom ⋯ else 0))
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have pos : ∀ (h : i = j),
  Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
        (eqToHom sorry) (eqToHom sorry) :
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)) :
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
Tactic: split_ifs with h