awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j
have h₄ : Hom.τ₁
    (c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
        comm₂₃ := sorry }) =
  (s.ι.app j).τ₁
Tactic: ext
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
h₄ :
  Hom.τ₁
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₁
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j
have h₅ : Hom.τ₂
    (c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
        comm₂₃ := sorry }) =
  (s.ι.app j).τ₂
Tactic: ext
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
h₄ :
  Hom.τ₁
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₁
h₅ :
  Hom.τ₂
      (c.ι.app j ≫
        { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }) =
    (s.ι.app j).τ₂
⊢ c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } =
    s.ι.app j
have h₆ : Hom.τ₃
    (c.ι.app j ≫
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
        comm₂₃ := sorry }) =
  (s.ι.app j).τ₃
Tactic: ext
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m =
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }
have h₄ : m.τ₁ =
  Hom.τ₁
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
      comm₂₃ := sorry }
Tactic: ext
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
h₄ :
  m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
⊢ m =
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }
have h₅ : m.τ₂ =
  Hom.τ₂
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
      comm₂₃ := sorry }
Tactic: ext
-- 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 : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
h₄ :
  m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
h₅ :
  m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
⊢ m =
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }
have h₆ : m.τ₃ =
  Hom.τ₃
    { τ₁ := h₁.desc (mapCocone π₁ s), τ₂ := h₂.desc (mapCocone π₂ s), τ₃ := h₃.desc (mapCocone π₃ s), comm₁₂ := sorry,
      comm₂₃ := sorry }
Tactic: ext
-- 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
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    F.obj x ⟶
      obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        x_1)
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
        comm₂₃ := ⋯ })
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        f)
have h₁ : Eq (α :=
  (F.obj x).X₁ ⟶
    (obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        x_1).X₁)
  (Hom.τ₁
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := sorry,
        comm₂₃ := sorry }))
  (Hom.τ₁
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := sorry, comm₂₃ := sorry } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        f))
Tactic: ext
-- 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
inst_3 : HasColimit (F ⋙ π₁)
inst_4 : HasColimit (F ⋙ π₂)
inst_5 : HasColimit (F ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
h₁ :
  Eq (α :=
    (F.obj x).X₁ ⟶
      (obj
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x_1).X₁)
    (Hom.τ₁
      (F.map f ≫
        { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₁
      ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        Functor.map
          (obj (const J)
            (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
              (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f))
⊢ Eq (α :=
    F.obj x ⟶
      obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        x_1)
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := ⋯,
        comm₂₃ := ⋯ })
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) ⋯))
        f)
have h₂ : Eq (α :=
  (F.obj x).X₂ ⟶
    (obj
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        x_1).X₂)
  (Hom.τ₂
    (F.map f ≫
      { τ₁ := colimit.ι (F ⋙ π₁) x_1, τ₂ := colimit.ι (F ⋙ π₂) x_1, τ₃ := colimit.ι (F ⋙ π₃) x_1, comm₁₂ := sorry,
        comm₂₃ := sorry }))
  (Hom.τ₂
    ({ τ₁ := colimit.ι (F ⋙ π₁) x, τ₂ := colimit.ι (F ⋙ π₂) x, τ₃ := colimit.ι (F ⋙ π₃) x, comm₁₂ := sorry, comm₂₃ := sorry } ≫
      Functor.map
        (obj (const J)
          (mk (X₁ := colimit (F ⋙ π₁)) (X₂ := colimit (F ⋙ π₂)) (X₃ := colimit (F ⋙ π₃))
            (colimMap (F.whiskerLeft π₁Toπ₂)) (colimMap (F.whiskerLeft π₂Toπ₃)) sorry))
        f))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ (a • φ₁).τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + (a • φ₂).τ₁
have dsimp : a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
have rw : a • (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
Tactic: rw [h.comm₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ (a • φ₁).τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + (a • φ₂).τ₂
have dsimp : a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
have rw : a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
Tactic: rw [h.comm₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ (a • φ₁).τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + (a • φ₂).τ₃
have dsimp : a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Linear (goal)
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
have rw : a • (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
Tactic: rw [h.comm₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range
have rw : (∀ (x₂ : (↑S.X₂ : Type v)),
    Eq (α := (↑S.X₃ : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                ModuleCat.carrier) S.g :
              (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
            x₂ :
          (↑S.X₃ : Type v))
        (0 : (↑S.X₃ : Type v)) →
      ∃ (x₁ : (↑S.X₁ : Type v)),
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                ModuleCat.carrier) S.f :
              (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            x₁ =
          x₂) ↔
  (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range
Tactic: rw [moduleCat_exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
have rw : (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range ↔
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
Tactic: rw [moduleCat_exact_iff_ker_sub_range]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.Exact ↔
    Function.Exact (M := (↑S.X₁ : Type v)) (N := (↑S.X₂ : Type v)) (P := (↑S.X₃ : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) S.f) :
        (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) S.g) :
        (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
have rw : (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.g).ker =
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.f).range
Tactic: rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
have mp : (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.g).ker =
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.f).range
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
mp :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker →
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
have mpr : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.g).ker =
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        ModuleCat.carrier) S.f).range →
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
X₁ X₂ X₃ : ModuleCat.{v, u} R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker
have rw : (ModuleCat.Hom.hom g).ker ≤ (ModuleCat.Hom.hom g).ker
Tactic: rw [hfg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f = 0
have hf : ∀ (x : (↑(ModuleCat.of R ↥f.ker) : Type v)),
  Eq (α := (↑(ModuleCat.of R N) : Type v))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f) :
          (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v))
        x :
      (↑(ModuleCat.of R N) : Type v))
    ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v)) x :
      (↑(ModuleCat.of R N) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
⊢ ((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) ∘ₗ ((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M') = 0
have h : ∀ (x : M),
  Eq (α := L)
    ((((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) ∘ₗ ((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M') :
          (a : M) → L)
        x :
      L)
    ((0 : (a : M) → L) x : L)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
⊢ Function.Exact (M := M) (N := N) (P := L) (⇑(((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M')) : (a : M) → N)
    (⇑((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) : (a : N) → L)
have rwa : Function.Exact.{u_1, v, v} (M := M') (N := N) (P := L) (⇑((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) : (a : M') → N)
  (⇑((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) : (a : N) → L)
Tactic: rwa [LinearEquiv.precomp_exact_iff_exact, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact]