awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
have eq₁ : ∀ (j : J),
  Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
    (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
Tactic: have eq₁ := h₁.fac (π₁.mapCone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
have eq₂ : ∀ (j : J),
  Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
    (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
Tactic: have eq₂ := h₂.fac (π₂.mapCone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
have eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂
Tactic: have eq₁₂ := fun j => (c.π.app j).comm₁₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
have eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) s.pt) j).f ≫ (s.π.app j).τ₂
Tactic: have eq₁₂' := fun j => (s.π.app j).comm₁₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) s.pt) j).f ≫ (s.π.app j).τ₂
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
have dsimp : (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
Tactic: dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw₁ : Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
  (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
rw₁ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw₂ : Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ ≫ (F.obj j).f : s.pt.X₁ ⟶ (F.obj j).X₂)
  (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
rw₁ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₂ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ ≫ (F.obj j).f : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw₃ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
rw₁ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₂ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ ≫ (F.obj j).f : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₃ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw₄ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
rw₁ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₂ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ ≫ (F.obj j).f : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₃ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂
rw₄ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
have rw₅ : s.pt.f ≫ (s.π.app j).τ₂ = s.pt.f ≫ (s.π.app j).τ₂
Tactic: rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
have eq₂ : ∀ (j : J),
  Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
    (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
Tactic: have eq₂ := h₂.fac (π₂.mapCone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
have eq₃ : ∀ (j : J),
  Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
    (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
Tactic: have eq₃ := h₃.fac (π₃.mapCone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
have eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) j).g ≫ (c.π.app j).τ₃
Tactic: have eq₂₃ := fun j => (c.π.app j).comm₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) j).g ≫ (c.π.app j).τ₃
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
have eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) s.pt) j).g ≫ (s.π.app j).τ₃
Tactic: have eq₂₃' := fun j => (s.π.app j).comm₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) j).g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) s.pt) j).g ≫ (s.π.app j).τ₃
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
have dsimp : (h₂.lift (mapCone π₂ s) ≫ c.pt.g) ≫ (c.π.app j).τ₃ = (s.pt.g ≫ h₃.lift (mapCone π₃ s)) ≫ (c.π.app j).τ₃
Tactic: dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢