awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Retract (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        ⋯)
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        ⋯) =
    𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁))
have h₁ : Arrow.Hom.left
    (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        sorry)
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        sorry)) =
  Arrow.Hom.left (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Retract (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
h₁ :
  Arrow.Hom.left
      (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯)
        (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯)) =
    Arrow.Hom.left (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))
⊢ CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        ⋯)
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        ⋯) =
    𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁))
have h₂ : Arrow.Hom.right
    (CategoryStruct.comp (Y := Arrow.mk (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂))
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.i;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.i;
          this))
        sorry)
      (Arrow.homMk
        (homologyMap
          (have this := Arrow.Hom.left h.r;
          this))
        (homologyMap
          (have this := Arrow.Hom.right h.r;
          this))
        sorry)) =
  Arrow.Hom.right (𝟙 (Arrow.mk (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Retract (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ T₁ S₂ T₂ : ShortComplex.{v_1, u_1} C
inst_2 : S₁.HasHomology
inst_3 : T₁.HasHomology
inst_4 : S₂.HasHomology
inst_5 : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (X := S₂.homology) (Y := T₂.homology) (homologyMap f₂)
⊢ IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)
have have : ∀
  (h :
    RetractArrow (X := S₁.homology) (Y := T₁.homology) (Z := S₂.homology) (W := T₂.homology) (homologyMap f₁)
      (homologyMap f₂)),
  IsIso (X := S₁.homology) (Y := T₁.homology) (homologyMap f₁)
Tactic: have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
    { i := Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left))
        (v := homologyMap (show T₁ ⟶ T₂ from h.i.right)) (by simp [← homologyMap_comp])
      r := Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left))
        (v := homologyMap (show T₂ ⟶ T₁ from h.r.right)) (by simp [← homologyMap_comp])
      retract := by ext <;> simp [← homologyMap_comp] }
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0
have rw : S.f ≫ S.g ≫ x = 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
⊢ S.f ≫ k = 0
have rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
rw : S.f ≫ S.g ≫ x = 0
rw₁ : Eq (α := S.X₁ ⟶ A) (0 ≫ x) 0
⊢ S.f ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A) 0 0
Tactic: rw [hx, S.zero_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0
have rw : h.ι ≫ h.descQ k sorry = h.ι ≫ h.g' ≫ x
Tactic: rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x
have e_a : h.descQ k sorry = h.g' ≫ x
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hf : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
have rw : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) (0 ≫ 𝟙 S.X₂) 0
Tactic: rw [hf, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hf : S.f = 0
rw : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) (0 ≫ 𝟙 S.X₂) 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [hf, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
⊢ 𝟙 h.Q ≫ h.g' = 0
have rw : h.p ≫ 𝟙 h.Q ≫ h.g' = h.p ≫ 0
Tactic: rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
rw : h.p ≫ 𝟙 h.Q ≫ h.g' = h.p ≫ 0
⊢ 𝟙 h.Q ≫ h.g' = 0
have rw₁ : h.p ≫ h.g' = h.p ≫ 0
Tactic: rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
rw : h.p ≫ 𝟙 h.Q ≫ h.g' = h.p ≫ 0
rw₁ : h.p ≫ h.g' = h.p ≫ 0
⊢ 𝟙 h.Q ≫ h.g' = 0
have rw₂ : S.g = h.p ≫ 0
Tactic: rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
rw : h.p ≫ 𝟙 h.Q ≫ h.g' = h.p ≫ 0
rw₁ : h.p ≫ h.g' = h.p ≫ 0
rw₂ : S.g = h.p ≫ 0
rw₃ : S.g = 0
⊢ 𝟙 h.Q ≫ h.g' = 0
have rw₄ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
⊢ IsIso h.ι
have have : ∀ (φ : h.Q ⟶ (KernelFork.ofι h.ι sorry).pt) (hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι sorry) = 𝟙 h.Q), IsIso h.ι
Tactic: have ⟨φ, hφ⟩ := KernelFork.IsLimit.lift' h.hι' (𝟙 _)
    (by rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι ≫ φ = 𝟙 h.H
have rw : (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι
Tactic: rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
rw : (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι
⊢ h.ι ≫ φ = 𝟙 h.H
have rw₁ : h.ι ≫ φ ≫ h.ι = 𝟙 h.H ≫ h.ι
Tactic: rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
rw : (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι
rw₁ : h.ι ≫ φ ≫ h.ι = 𝟙 h.H ≫ h.ι
⊢ h.ι ≫ φ = 𝟙 h.H
have rw₂ : h.ι ≫ 𝟙 h.Q = 𝟙 h.H ≫ h.ι
Tactic: rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
rw : (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι
rw₁ : h.ι ≫ φ ≫ h.ι = 𝟙 h.H ≫ h.ι
rw₂ : h.ι ≫ 𝟙 h.Q = 𝟙 h.H ≫ h.ι
⊢ h.ι ≫ φ = 𝟙 h.H
have rw₃ : h.ι = 𝟙 h.H ≫ h.ι
Tactic: rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
rw : (h.ι ≫ φ) ≫ h.ι = 𝟙 h.H ≫ h.ι
rw₁ : h.ι ≫ φ ≫ h.ι = 𝟙 h.H ≫ h.ι
rw₂ : h.ι ≫ 𝟙 h.Q = 𝟙 h.H ≫ h.ι
rw₃ : h.ι = 𝟙 h.H ≫ h.ι
⊢ h.ι ≫ φ = 𝟙 h.H
have rw₄ : h.ι = h.ι
Tactic: rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [comp_id, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g
have rw : (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).g' = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
Tactic: rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
    ofIsLimitKernelFork_p, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).g' = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g
have rw₁ : S.g = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
Tactic: rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
    ofIsLimitKernelFork_p, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).g' = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
rw₁ : S.g = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g
have rw₂ : S.g = 𝟙 S.X₂ ≫ S.g
Tactic: rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
    ofIsLimitKernelFork_p, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
rw : (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).g' = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
rw₁ : S.g = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
rw₂ : S.g = 𝟙 S.X₂ ≫ S.g
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g
have rw₃ : S.g = S.g
Tactic: rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
    ofIsLimitKernelFork_p, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = φ
have rw : φ = (ofIsLimitKernelFork S hf c hc).p ≫ φ
Tactic: rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_descQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0
have rw : (ofIsColimitCokernelCofork S hg c hc).p ≫ (ofIsColimitCokernelCofork S hg c hc).g' =
  (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
Tactic: rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
rw :
  (ofIsColimitCokernelCofork S hg c hc).p ≫ (ofIsColimitCokernelCofork S hg c hc).g' =
    (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0
have rw₁ : S.g = (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
Tactic: rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
rw :
  (ofIsColimitCokernelCofork S hg c hc).p ≫ (ofIsColimitCokernelCofork S hg c hc).g' =
    (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
rw₁ : S.g = (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0
have rw₂ : Eq (α := S.X₂ ⟶ S.X₃) 0 ((ofIsColimitCokernelCofork S hg c hc).p ≫ 0)
Tactic: rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
rw :
  (ofIsColimitCokernelCofork S hg c hc).p ≫ (ofIsColimitCokernelCofork S hg c hc).g' =
    (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
rw₁ : S.g = (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
rw₂ : Eq (α := S.X₂ ⟶ S.X₃) 0 ((ofIsColimitCokernelCofork S hg c hc).p ≫ 0)
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
rw : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [comp_id, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ Eq (α := S.X₂ ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    (𝟙 S.X₂ ≫ (CokernelCofork.IsColimit.ofId S.f hf).desc (CokernelCofork.ofπ S.g ⋯)) 0
have change : 𝟙 S.X₂ ≫ S.g = 0
Tactic: change 𝟙 _ ≫ S.g = 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
⊢ (ofZeros S hf hg).g' = 0
have rw : (ofZeros S hf hg).p ≫ (ofZeros S hf hg).g' = (ofZeros S hf hg).p ≫ 0
Tactic: rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
rw : (ofZeros S hf hg).p ≫ (ofZeros S hf hg).g' = (ofZeros S hf hg).p ≫ 0
⊢ (ofZeros S hf hg).g' = 0
have rw₁ : (ofZeros S hf hg).p ≫ (ofZeros S hf hg).g' = 0
Tactic: rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hf : S.f = 0
hg : S.g = 0
rw : (ofZeros S hf hg).p ≫ (ofZeros S hf hg).g' = (ofZeros S hf hg).p ≫ 0
rw₁ : (ofZeros S hf hg).p ≫ (ofZeros S hf hg).g' = 0
rw₂ : S.g = 0
⊢ (ofZeros S hf hg).g' = 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
⊢ S.f ≫ h.p ≫ eQ.inv = 0
have rw : (S.f ≫ h.p) ≫ eQ.inv = 0
Tactic: rw [← assoc, h.wp, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
rw : (S.f ≫ h.p) ≫ eQ.inv = 0
⊢ S.f ≫ h.p ≫ eQ.inv = 0
have rw₁ : Eq (α := S.X₁ ⟶ Q') (0 ≫ eQ.inv) 0
Tactic: rw [← assoc, h.wp, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
A Q' H' : C
eQ : Q' ≅ h.Q
eH : H' ≅ h.H
rw : (S.f ≫ h.p) ≫ eQ.inv = 0
rw₁ : Eq (α := S.X₁ ⟶ Q') (0 ≫ eQ.inv) 0
⊢ S.f ≫ h.p ≫ eQ.inv = 0
have rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ Q') 0 0
Tactic: rw [← assoc, h.wp, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁.φQ = ψ₂.φQ
have rw : h₁.p ≫ ψ₁.φQ = h₁.p ≫ ψ₂.φQ
Tactic: rw [← cancel_epi h₁.p, commp, commp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
rw : h₁.p ≫ ψ₁.φQ = h₁.p ≫ ψ₂.φQ
⊢ ψ₁.φQ = ψ₂.φQ
have rw₁ : φ.τ₂ ≫ h₂.p = h₁.p ≫ ψ₂.φQ
Tactic: rw [← cancel_epi h₁.p, commp, commp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
rw : h₁.p ≫ ψ₁.φQ = h₁.p ≫ ψ₂.φQ
rw₁ : φ.τ₂ ≫ h₂.p = h₁.p ≫ ψ₂.φQ
⊢ ψ₁.φQ = ψ₂.φQ
have rw₂ : φ.τ₂ ≫ h₂.p = φ.τ₂ ≫ h₂.p
Tactic: rw [← cancel_epi h₁.p, commp, commp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁ = ψ₂
have hQ : ψ₁.φQ = ψ₂.φQ
Tactic: have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH
have rw : ψ₁.φH ≫ h₂.ι = ψ₂.φH ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, commι, commι, hQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
rw : ψ₁.φH ≫ h₂.ι = ψ₂.φH ≫ h₂.ι
⊢ ψ₁.φH = ψ₂.φH
have rw₁ : h₁.ι ≫ ψ₁.φQ = ψ₂.φH ≫ h₂.ι
Tactic: rw [← cancel_mono h₂.ι, commι, commι, hQ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.RightHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
rw : ψ₁.φH ≫ h₂.ι = ψ₂.φH ≫ h₂.ι
rw₁ : h₁.ι ≫ ψ₁.φQ = ψ₂.φH ≫ h₂.ι
⊢ ψ₁.φH = ψ₂.φH
have rw₂ : h₁.ι ≫ ψ₁.φQ = h₁.ι ≫ ψ₂.φQ
Tactic: rw [← cancel_mono h₂.ι, commι, commι, hQ]