awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0

Tactic:
have wπ : f' ≫ (0 : S.X₁ ⟶ 0) = 0 := comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
rw : Epi.{v_1, u_1} (𝟙 (KernelFork.ofι S.f ⋯).pt)
⊢ Epi f'

Tactic:
rw [hf']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
⊢ Epi.{v_1, u_1} (𝟙 (KernelFork.ofι S.f ⋯).pt)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
have : (hπ : IsColimit (CokernelCofork.ofπ 0 wπ)) → S.LeftHomologyData
⊢ S.LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ 0 wπ) := CokernelCofork.IsColimit.ofEpiOfIsZero _
      (by rw [hf']; infer_instance) (isZero_zero _)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
hπ : IsColimit (CokernelCofork.ofπ 0 wπ)
⊢ S.LeftHomologyData

Tactic:
exact
    { K := S.X₁
      H := 0
      i := S.f
      wi := S.zero
      hi := hi
      π := 0
      wπ := wπ
      hπ := hπ }
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
Z' : C
x : S.X₂ ⟶ Z'
hx : S.f ≫ x = 0
⊢ S.g ≫ (fun {Z' : C} (x : S.X₂ ⟶ Z') (x_1 : S.f ≫ x = 0) ↦ s.s ≫ x) x hx = x

Tactic:
simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, sub_eq_self, CategoryTheory.ShortComplex.Splitting.g_s_assoc, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
Z' : C
x : S.X₂ ⟶ Z'
h : S.f ≫ x = 0
b : S.X₃ ⟶ Z'
hb : S.g ≫ b = x
⊢ b = (fun {Z' : C} (x : S.X₂ ⟶ Z') (x_1 : S.f ≫ x = 0) ↦ s.s ≫ x) x h

Tactic:
simp only [← hb, s.s_g_assoc]

Premises used: CategoryTheory.ShortComplex.Splitting.s_g_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
have : (hp : IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.RightHomologyData
⊢ S.RightHomologyData

Tactic:
have hp := CokernelCofork.IsColimit.ofπ S.g S.zero
    (fun x _ => s.s ≫ x)
    (fun x hx => by simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero])
    (fun x _ b hb => by simp only [← hb, s.s_g_assoc])
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
⊢ g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt

Tactic:
simp [g']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
⊢ g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt

Tactic:
have hg' : g' = 𝟙 _ := by simp [g']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
⊢ Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0

Tactic:
have wι : (0 : 0 ⟶ S.X₃) ≫ g' = 0 := zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
rw : Mono.{v_1, u_1} (𝟙 (CokernelCofork.ofπ S.g ⋯).pt)
⊢ Mono g'

Tactic:
rw [hg']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
dsimp : Mono.{v_1, u_1} (𝟙 S.X₃)
⊢ Mono.{v_1, u_1} (𝟙 (CokernelCofork.ofπ S.g ⋯).pt)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
⊢ Mono.{v_1, u_1} (𝟙 S.X₃)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
have : (hι : IsLimit (KernelFork.ofι 0 wι)) → S.RightHomologyData
⊢ S.RightHomologyData

Tactic:
have hι : IsLimit (KernelFork.ofι 0 wι) := KernelFork.IsLimit.ofMonoOfIsZero _
      (by rw [hg']; dsimp; infer_instance) (isZero_zero _)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
hι : IsLimit (KernelFork.ofι 0 wι)
⊢ S.RightHomologyData

Tactic:
exact
    { Q := S.X₃
      H := 0
      p := S.g
      wp := S.zero
      hp := hp
      ι := 0
      wι := wι
      hι := hι }
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
⊢ S.Exact

Tactic:
⟨s.homologyData, isZero_zero _⟩

Premises used: CategoryTheory.ShortComplex.Exact.mk, CategoryTheory.ShortComplex.Splitting.homologyData, CategoryTheory.Limits.isZero_zero, Exists.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
dsimp : F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
⊢ f (S.map F) ≫ F.map s.r = 𝟙 (X₁ (S.map F))

Tactic:
dsimp [ShortComplex.map]

Premises used: CategoryTheory.ShortComplex.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
rw : F.map (S.f ≫ s.r) = 𝟙 (F.obj S.X₁)
rw₁ : F.map (𝟙 S.X₁) = 𝟙 (F.obj S.X₁)
rw₂ rw₃ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj S.X₁) (𝟙 (F.obj S.X₁)) (𝟙 (F.obj S.X₁))
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)

Tactic:
rw [← F.map_comp, f_r, F.map_id]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.ShortComplex.Splitting.f_r
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
dsimp : F.map s.s ≫ F.map S.g = 𝟙 (F.obj S.X₃)
⊢ F.map s.s ≫ g (S.map F) = 𝟙 (X₃ (S.map F))

Tactic:
dsimp [ShortComplex.map]

Premises used: CategoryTheory.ShortComplex.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ F.map s.s ≫ F.map S.g = 𝟙 (F.obj S.X₃)

Tactic:
simp only [← F.map_comp, s_g, F.map_id]

Premises used: CategoryTheory.ShortComplex.Splitting.s_g, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
dsimp : F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)
⊢ HAdd.hAdd (α := X₂ (S.map F) ⟶ X₂ (S.map F)) (β := X₂ (S.map F) ⟶ X₂ (S.map F)) (F.map s.r ≫ f (S.map F))
      (g (S.map F) ≫ F.map s.s) =
    𝟙 (X₂ (S.map F))

Tactic:
dsimp [ShortComplex.map]

Premises used: CategoryTheory.ShortComplex.map
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)

Tactic:
simp only [← F.map_id, ← s.id, Functor.map_comp, Functor.map_add]

Premises used: CategoryTheory.ShortComplex.Splitting.id, CategoryTheory.Functor.map_add, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₁ : e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₂ : (e.inv ≫ e.hom).τ₁ = 𝟙 S₂.X₁
rw₃ : Hom.τ₁ (𝟙 S₂) = 𝟙 S₂.X₁
rw₄ rw₅ : Eq.{v_1 + 1} (α := S₂.X₁ ⟶ S₂.X₁) (𝟙 S₂.X₁) (𝟙 S₂.X₁)
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.comp_τ₁, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc, CategoryTheory.ShortComplex.id_τ₁, CategoryTheory.ShortComplex.Splitting.f_r_assoc, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₃ : e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₄ : (e.inv ≫ e.hom).τ₃ = 𝟙 S₂.X₃
rw₅ : Hom.τ₃ (𝟙 S₂) = 𝟙 S₂.X₃
rw₆ rw₇ : Eq.{v_1 + 1} (α := S₂.X₃ ⟶ S₂.X₃) (𝟙 S₂.X₃) (𝟙 S₂.X₃)
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃

Tactic:
rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.Splitting.s_g_assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.comp_τ₃, CategoryTheory.ShortComplex.id_τ₃, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂

Tactic:
have eq := e.inv.τ₂ ≫= s.id =≫ e.hom.τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂
⊢ e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
rw [id_comp, ← comp_τ₂, e.inv_hom_id, id_τ₂] at eq

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.ShortComplex.id_τ₂, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₄ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₅ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + S₁.g ≫ s.s ≫ e.hom.τ₂)
rw₆ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
rw₇ :
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
rw₈ rw₉ :
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂

Tactic:
rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CategoryTheory.ShortComplex.Hom.comm₂₃_assoc, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
X₁ X₂ : C
inst_4 : HasBinaryBiproduct.{v_1, u_1} X₁ X₂
⊢ Eq.{v_1 + 1} (α := X₁ ⟶ X₂) (CategoryStruct.comp (Y := biprod.{v_1, u_1} X₁ X₂) biprod.inl biprod.snd) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Splitting
⊢ (S.op.f ≫ h.s.op).unop = Quiver.Hom.unop (𝟙 S.op.X₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Splitting
⊢ Eq (α := Opposite.unop S.op.X₃ ⟶ Opposite.unop S.op.X₃) (Quiver.Hom.unop (h.r.op ≫ S.op.g))
    (Quiver.Hom.unop (𝟙 S.op.X₃))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Splitting
simp : S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
⊢ (h.s.op ≫ S.op.f + S.op.g ≫ h.r.op).unop = Quiver.Hom.unop (𝟙 S.op.X₂)

Tactic:
simp only [op_X₂, Opposite.unop_op, op_X₁, op_f, op_X₃, op_g, unop_add, unop_comp,
      Quiver.Hom.unop_op, unop_id, ← h.id]

Premises used: CategoryTheory.ShortComplex.op_g, Quiver.Hom.unop_op, CategoryTheory.ShortComplex.Splitting.id, CategoryTheory.ShortComplex.op_X₁, CategoryTheory.unop_comp, CategoryTheory.unop_add, Opposite.unop_op, CategoryTheory.ShortComplex.op_f, CategoryTheory.ShortComplex.op_X₃, CategoryTheory.unop_id, CategoryTheory.ShortComplex.op_X₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Splitting
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S_1 : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : Splitting.{v_1, u_1} (C := Cᵒᵖ) S
⊢ (S.unop.f ≫ h.s.unop).op = Quiver.Hom.op (𝟙 S.unop.X₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S_1 : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : Splitting.{v_1, u_1} (C := Cᵒᵖ) S
⊢ (h.r.unop ≫ S.unop.g).op = Quiver.Hom.op (𝟙 S.unop.X₃)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S_1 : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : Splitting.{v_1, u_1} (C := Cᵒᵖ) S
simp : S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
⊢ (h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = Quiver.Hom.op (𝟙 S.unop.X₂)

Tactic:
simp only [unop_X₂, Opposite.op_unop, unop_X₁, unop_f, unop_X₃, unop_g, op_add,
      op_comp, Quiver.Hom.op_unop, op_id, ← h.id]

Premises used: CategoryTheory.op_comp, CategoryTheory.ShortComplex.unop_X₂, CategoryTheory.ShortComplex.Splitting.id, Opposite.op_unop, Quiver.Hom.op_unop, CategoryTheory.ShortComplex.unop_f, CategoryTheory.ShortComplex.unop_X₁, CategoryTheory.ShortComplex.unop_X₃, CategoryTheory.op_add, CategoryTheory.ShortComplex.unop_g, CategoryTheory.op_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S_1 : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : Splitting.{v_1, u_1} (C := Cᵒᵖ) S
⊢ S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.Splitting
inst_4 : HasBinaryBiproduct.{v_1, u_1} S.X₁ S.X₃
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} S.X₁ S.X₃) (biprod.lift h.r S.g) (biprod.desc S.f h.s) = 𝟙 S.X₂

Tactic:
simp [h.id]

Premises used: CategoryTheory.ShortComplex.Splitting.id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
⊢ Epi h.f'

Tactic:
have := hS.epi_f' h