awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
hk : S.f ≫ k = 0
⊢ h.p ≫ h.descQ k hk = k

Tactic:
h.hp.fac _ WalkingParallelPair.one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.ShortComplex.RightHomologyData.hp, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.ShortComplex.RightHomologyData.descQ
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ h.p ≫ h.g' = S.g

Tactic:
p_descQ _ _ _

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.ShortComplex.RightHomologyData.g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ h.ι ≫ h.g' = 0

Tactic:
h.wι

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wι, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.RightHomologyData.descQ
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ A) 0 0
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Premises used: CategoryTheory.ShortComplex.zero_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ 0 = h.ι ≫ h.g' ≫ x

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw : h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0

Tactic:
rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
e_a : h.descQ k ⋯ = h.g' ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = h.ι ≫ h.g' ≫ x

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.descQ k ⋯ = h.g' ≫ x

Tactic:
simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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 : A ⟶ h.Q
hk : k ≫ h.g' = 0
⊢ h.liftH k hk ≫ h.ι = k

Tactic:
h.hι.fac (KernelFork.ofι k hk) WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.ShortComplex.RightHomologyData.hι, CategoryTheory.ShortComplex.RightHomologyData.liftH, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
rw [hf, comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ h.descQ (𝟙 S.X₂) ⋯ ≫ h.p = 𝟙 h.Q

Tactic:
simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc, CategoryTheory.Category.comp_id, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₄ rw₅ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ 𝟙 h.Q ≫ h.g' = 0

Tactic:
rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.Category.id_comp, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
have : ∀ (φ : h.Q ⟶ (KernelFork.ofι h.ι ⋯).pt) (hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι ⋯) = 𝟙 h.Q), IsIso h.ι
⊢ IsIso h.ι

Tactic:
have ⟨φ, hφ⟩ := KernelFork.IsLimit.lift' h.hι' (𝟙 _)
    (by rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg])
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.ι
rw₄ rw₅ : h.ι = h.ι
⊢ h.ι ≫ φ = 𝟙 h.H

Tactic:
rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.RightHomologyData.ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ IsIso h.ι

Tactic:
exact ⟨φ, by rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp], hφ⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
rw [comp_id, hf]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ Iso.hom (Iso.refl c.pt) ≫ Fork.ι (KernelFork.ofι (Fork.ι c) ⋯) = Fork.ι c

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₃ rw₄ : S.g = S.g
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g

Tactic:
rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g',
    ofIsLimitKernelFork_p, id_comp]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_p, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.Category.id_comp, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
T : C
φ : S.X₂ ⟶ T
⊢ S.f ≫ φ = 0

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw : φ = (ofIsLimitKernelFork S hf c hc).p ≫ φ
⊢ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = φ

Tactic:
rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_descQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_descQ, CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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).p ≫ φ

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ Iso.hom (Iso.refl c.pt) = Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Eq (α := S.X₂ ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    (Cofork.π c ≫ 𝟙 c.pt ≫ (hc.ofIsoColimit (Cofork.ext (Iso.refl c.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
    (Cofork.π c ≫ 0)

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Eq (α := S.X₂ ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    (Cofork.π c ≫ (hc.ofIsoColimit (Cofork.ext (Iso.refl c.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) (Cofork.π c ≫ 0)

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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)
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0

Tactic:
rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
rw [comp_id, hf]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
change : 𝟙 S.X₂ ≫ 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

Tactic:
change 𝟙 _ ≫ S.g = 0

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
simp only [hg, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ (ofZeros S hf hg).g' = 0

Tactic:
rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofZeros, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ Q') 0 0
⊢ S.f ≫ h.p ≫ eQ.inv = 0

Tactic:
rw [← assoc, h.wp, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ Cofork.π (CokernelCofork.ofπ h.p ⋯) ≫ eQ.symm.hom = h.p ≫ eQ.inv

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ Eq (α := H' ⟶ (CokernelCofork.ofπ S.g ⋯).pt)
    ((eH.hom ≫ h.ι ≫ eQ.inv) ≫
      (IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯))
    0

Tactic:
simp [IsCokernel.cokernelIso]

Premises used: CategoryTheory.Limits.IsCokernel.cokernelIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ (parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt) (h.hp.desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl S.X₃) =
    eQ.symm.hom ≫
      (parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
            ((IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.left

Tactic:
simp [IsCokernel.cokernelIso]

Premises used: CategoryTheory.Limits.IsCokernel.cokernelIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ (parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt) (h.hp.desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl S.X₃) =
    eQ.symm.hom ≫
      (parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
            ((IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯)) 0).map
        WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ Cone.pt (F :=
      parallelPair (Y := (CokernelCofork.ofπ S.g ⋯).pt)
        ((IsCokernel.cokernelIso S.f (h.p ≫ eQ.inv) h.hp eQ.symm ⋯).desc (CokernelCofork.ofπ S.g ⋯)) 0)
      (Functor.obj (Cone.postcompose (Iso.hom (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯))) (KernelFork.ofι h.ι ⋯)) ≅
    (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).pt

Tactic:
exact eH.symm

Premises used: CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ NatTrans.app
      (Cone.π
        (Functor.obj (Cone.postcompose (Iso.hom (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯)))
          (KernelFork.ofι h.ι ⋯)))
      WalkingParallelPair.zero =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.zero

Tactic:
simp [IsCokernel.cokernelIso]

Premises used: CategoryTheory.Limits.IsCokernel.cokernelIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ NatTrans.app
      (Cone.π
        (Functor.obj (Cone.postcompose (Iso.hom (parallelPair.ext eQ.symm (Iso.refl S.X₃) ⋯ ⋯)))
          (KernelFork.ofι h.ι ⋯)))
      WalkingParallelPair.one =
    eH.symm.hom ≫ (KernelFork.ofι (eH.hom ≫ h.ι ≫ eQ.inv) ⋯).π.app WalkingParallelPair.one

Tactic:
simp [IsCokernel.cokernelIso]

Premises used: CategoryTheory.Limits.IsCokernel.cokernelIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ S.HasRightHomology

Tactic:
⟨Nonempty.intro h⟩

Premises used: Nonempty.intro, CategoryTheory.ShortComplex.HasRightHomology.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : HasCokernel S.f
inst_3 : HasKernel (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
⊢ S.HasRightHomology

Tactic:
HasRightHomology.mk' (RightHomologyData.ofHasCokernelOfHasKernel S)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel, CategoryTheory.ShortComplex.HasRightHomology.mk'
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
Y Z : C
g : Y ⟶ Z
X : C
inst_2 : HasKernel g
⊢ HasRightHomology (ShortComplex.mk (X₁ := X) 0 g ⋯)

Tactic:
HasRightHomology.mk' (RightHomologyData.ofHasKernel _ rfl)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel, CategoryTheory.ShortComplex.HasRightHomology.mk', rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
X Y : C
f : X ⟶ Y
Z : C
inst_2 : HasCokernel f
⊢ HasRightHomology (ShortComplex.mk (X₃ := Z) f 0 ⋯)

Tactic:
HasRightHomology.mk' (RightHomologyData.ofHasCokernel _ rfl)

Premises used: CategoryTheory.ShortComplex.HasRightHomology.mk', CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
X Y Z : C
⊢ HasRightHomology.{v_1, u_1} (C := C) (ShortComplex.mk (X₁ := X) (X₂ := Y) (X₃ := Z) 0 0 ⋯)

Tactic:
HasRightHomology.mk' (RightHomologyData.ofZeros _ rfl rfl)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ofZeros, CategoryTheory.ShortComplex.HasRightHomology.mk', rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ h.op.f' = h.g'.op

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.RightHomologyData.descQ, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
⊢ h.unop.f' = h.g'.unop

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.LeftHomologyData
⊢ h.op.g' = h.f'.op

Tactic:
rfl

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.ShortComplex.LeftHomologyData.liftK, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.RightHomologyData.descQ, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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.LeftHomologyData
⊢ h.unop.g' = h.f'.unop

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.ShortComplex.RightHomologyData.g', CategoryTheory.ShortComplex.RightHomologyData.descQ, rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : S.HasLeftHomology
⊢ S.op.HasRightHomology

Tactic:
HasRightHomology.mk' S.leftHomologyData.op

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.HasRightHomology.mk', CategoryTheory.ShortComplex.LeftHomologyData.op
-- Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology
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
inst_2 : S.HasRightHomology
⊢ S.op.HasLeftHomology

Tactic:
HasLeftHomology.mk' S.rightHomologyData.op

Premises used: CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.RightHomologyData.op, CategoryTheory.ShortComplex.HasLeftHomology.mk'