awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
⊢ { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
have have : (H :
    { l :
      A ⟶
        Cone.pt (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
          (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) sorry) //
      l ≫ Fork.ι (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) sorry) = k ≫ S.X₂.iCycles i }) →
  { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
Tactic: have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
have refine_1 : Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
Tactic: refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 : Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
⊢ { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
have refine_2 : CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) sorry sorry) (cyclesMap S.f i) = k
Tactic: refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1 : Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₁ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₃ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i ≫ S.X₂.d i (c.next i)) 0
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
refine_1₃ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i ≫ S.X₂.d i (c.next i)) 0
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₄ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i)) 0
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
refine_1₃ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i ≫ S.X₂.d i (c.next i)) 0
refine_1₄ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i)) 0
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₅ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ 0) 0
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
refine_1₃ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i ≫ S.X₂.d i (c.next i)) 0
refine_1₄ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i)) 0
refine_1₅ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ 0) 0
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
have refine_1₆ : Eq.{v_1 + 1} (α := A ⟶ S.X₂.X (c.next i)) 0 0
Tactic: rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k
have refine_2 : CategoryStruct.comp (Y := S.X₂.cycles i)
    (CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) sorry sorry) (cyclesMap S.f i))
    (S.X₂.iCycles i) =
  k ≫ S.X₂.iCycles i
Tactic: rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.cycles i)
      (CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i))
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
⊢ CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k
have refine_2₁ : CategoryStruct.comp (Y := S.X₂.cycles i) (S.X₂.liftCycles ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i) (c.next i) sorry sorry)
    (S.X₂.iCycles i) =
  k ≫ S.X₂.iCycles i
Tactic: rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.cycles i)
      (CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i))
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.cycles i) (S.X₂.liftCycles ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i) (c.next i) ⋯ ⋯)
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
⊢ CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k
have refine_2₂ : (↑H : A ⟶ S.X₁.X i) ≫ S.f.f i = k ≫ S.X₂.iCycles i
Tactic: rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.cycles i)
      (CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i))
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.cycles i) (S.X₂.liftCycles ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i) (c.next i) ⋯ ⋯)
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
refine_2₂ : (↑H : A ⟶ S.X₁.X i) ≫ S.f.f i = k ≫ S.X₂.iCycles i
⊢ CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k
have refine_2₃ : k ≫ S.X₂.iCycles i = k ≫ S.X₂.iCycles i
Tactic: rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)
have h₁ : IsLimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₁)
  (Functor.mapCone ShortComplex.π₁ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) sorry))
Tactic: apply ShortComplex.isLimitOfIsLimitπ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)
have h₂ : IsLimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₂)
  (Functor.mapCone ShortComplex.π₂ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) sorry))
Tactic: apply ShortComplex.isLimitOfIsLimitπ
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
h₂ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCone ShortComplex.π₂ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)
have h₃ : IsLimit (F :=
  Functor.comp (D := ShortComplex.{v_1, u_1} C)
    (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
      Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
      (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
        Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
      0)
    ShortComplex.π₃)
  (Functor.mapCone ShortComplex.π₃ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) sorry))
Tactic: apply ShortComplex.isLimitOfIsLimitπ