awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
pos : ∀ (h : i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0
neg : ∀ (h : i + 1 = j) (h' : ¬j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) ((d i ≫ eqToHom ⋯) ≫ 0) 0
⊢ i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0
have pos₁ : ∀ (h : ¬i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (0 ≫ d j ≫ eqToHom sorry) 0
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
pos : ∀ (h : i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0
neg : ∀ (h : i + 1 = j) (h' : ¬j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) ((d i ≫ eqToHom ⋯) ≫ 0) 0
pos₁ : ∀ (h : ¬i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (0 ≫ d j ≫ eqToHom ⋯) 0
⊢ i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0
have neg₁ : ∀ (h : ¬i + 1 = j) (h' : ¬j + 1 = k),
  i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (CategoryStruct.comp (Y := X j) 0 0) 0
Tactic: split_ifs with h h' h'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0
have pos : i + 1 = i + 1 → i + 1 + 1 = i + 1 + 1 → (d i ≫ eqToHom sorry) ≫ d (i + 1) ≫ eqToHom sorry = 0
Tactic: substs h h'
Cleared hypotheses: j, k, h, h'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
⊢ of.d X d j (j + 1) = d j
have dsimp : (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
Tactic: dsimp [of.d]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
have rw : d j ≫ 𝟙 (X (j + 1)) = d j
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
rw : d j ≫ 𝟙 (X (j + 1)) = d j
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
have rw₁ : d j = d j
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀
have change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
Tactic: change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
have rw : d₀ ≫ 𝟙 X₁ = d₀
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
rw : d₀ ≫ 𝟙 X₁ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
have rw₁ : d₀ = d₀
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁
have change : (if 2 = HAdd.hAdd (α := ℕ) 1 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
Tactic: change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
have rw : d₁ ≫ 𝟙 X₂ = d₁
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
rw : d₁ ≫ 𝟙 X₂ = d₁
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
have rw₁ : d₁ = d₁
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0 1 = d₀
have change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
Tactic: change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
have rw : d₀ ≫ 𝟙 X₁ = d₀
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
rw : d₀ ≫ 𝟙 X₁ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
have rw₁ : d₀ = d₀
Tactic: rw [if_pos rfl, Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
⊢ S.Exact
have simp : ∀ (hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))), IsZero S.homology
Tactic: simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))
⊢ IsZero S.homology
have rw : Eq (α := S.homology ⟶ S.homology) (𝟙 S.homology) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))
⊢ Eq (α := S.homology ⟶ S.homology) (𝟙 S.homology) 0
have h : ∀ (i : ι), Hom.f (𝟙 S.homology) i = Hom.f 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ S.Exact ↔ ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
have mp : S.Exact → ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
mp : S.Exact → ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
⊢ S.Exact ↔ ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
have mpr : (∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))) → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ S.ShortExact ↔ ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))
have mp : S.ShortExact → ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
mp : S.ShortExact → ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))
⊢ S.ShortExact ↔ ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))
have mpr : (∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))) → S.ShortExact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
⊢ ShortComplex.ShortExact (S.map (eval C c i))
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (hypothesis)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
this : Mono S.f
⊢ ShortComplex.ShortExact (S.map (eval C c i))
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
have pos : ∀ (hij : j = i), Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
Tactic: by_cases hij : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
pos : ∀ (hij : j = i), Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
have neg : ∀ (hij : ¬j = i), Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
Tactic: by_cases hij : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
hij : j = i
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
have pos : Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) I) j)
Tactic: subst hij
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
have pos : ∀ (hij : j = i), Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
Tactic: by_cases hij : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
pos : ∀ (hij : j = i), Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
have neg : ∀ (hij : ¬j = i), Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
Tactic: by_cases hij : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexAbelian (goal)
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
hij : j = i
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
have pos : Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) P) j)
Tactic: subst hij
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ HasBinaryBiproduct.{v_1, u_1} (Functor.obj (eval C c i) K) (Functor.obj (eval C c i) L)
have dsimp : HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
Tactic: dsimp [eval]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ HasLimit (pair K L ⋙ eval C c i)
have have : ∀ (e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)), HasLimit (pair K L ⋙ eval C c i)
Tactic: have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ HasColimit (pair K L ⋙ eval C c i)
have have : ∀ (e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)), HasColimit (pair K L ⋙ eval C c i)
Tactic: have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.fst i) = 𝟙 (K.X i)
have rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.fst) i = 𝟙 (K.X i)
Tactic: rw [← comp_f, biprod.inl_fst, id_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.fst) i = 𝟙 (K.X i)
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.fst i) = 𝟙 (K.X i)
have rw₁ : Hom.f (𝟙 K) i = 𝟙 (K.X i)
Tactic: rw [← comp_f, biprod.inl_fst, id_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.fst) i = 𝟙 (K.X i)
rw₁ : Hom.f (𝟙 K) i = 𝟙 (K.X i)
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.fst i) = 𝟙 (K.X i)
have rw₂ : Eq.{v_1 + 1} (α := K.X i ⟶ K.X i) (𝟙 (K.X i)) (𝟙 (K.X i))
Tactic: rw [← comp_f, biprod.inl_fst, id_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.snd i)) 0
have rw : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.snd) i) 0
Tactic: rw [← comp_f, biprod.inl_snd, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.snd) i) 0
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.snd i)) 0
have rw₁ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f 0 i) 0
Tactic: rw [← comp_f, biprod.inl_snd, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inl biprod.snd) i) 0
rw₁ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (Hom.f 0 i) 0
⊢ Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f biprod.snd i)) 0
have rw₂ : Eq.{v_1 + 1} (α := K.X i ⟶ L.X i) 0 0
Tactic: rw [← comp_f, biprod.inl_snd, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.fst i)) 0
have rw : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.fst) i) 0
Tactic: rw [← comp_f, biprod.inr_fst, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.fst) i) 0
⊢ Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.fst i)) 0
have rw₁ : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f 0 i) 0
Tactic: rw [← comp_f, biprod.inr_fst, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.fst) i) 0
rw₁ : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (Hom.f 0 i) 0
⊢ Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) (CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.fst i)) 0
have rw₂ : Eq.{v_1 + 1} (α := L.X i ⟶ K.X i) 0 0
Tactic: rw [← comp_f, biprod.inr_fst, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.snd i) = 𝟙 (L.X i)
have rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.snd) i = 𝟙 (L.X i)
Tactic: rw [← comp_f, biprod.inr_snd, id_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.snd) i = 𝟙 (L.X i)
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.snd i) = 𝟙 (L.X i)
have rw₁ : Hom.f (𝟙 L) i = 𝟙 (L.X i)
Tactic: rw [← comp_f, biprod.inr_snd, id_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
rw : Hom.f (CategoryStruct.comp (Y := K ⊞ L) biprod.inr biprod.snd) i = 𝟙 (L.X i)
rw₁ : Hom.f (𝟙 L) i = 𝟙 (L.X i)
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f biprod.snd i) = 𝟙 (L.X i)
have rw₂ : Eq.{v_1 + 1} (α := L.X i ⟶ L.X i) (𝟙 (L.X i)) (𝟙 (L.X i))
Tactic: rw [← comp_f, biprod.inr_snd, id_f]