awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Eq (α := 0 ⟶ S.X₂) (0 ≫ S.f) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Eq (α := X₁ (ShortComplex.mk (X₁ := 0) 0 S.f ⋯) ⟶ X₂ (ShortComplex.mk (X₁ := 0) 0 S.f ⋯))
    (f (ShortComplex.mk (X₁ := 0) 0 S.f ⋯)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Mono (X := X₁ (S.map F)) (f (S.map F))

Tactic:
have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono (X := X₁ (S.map F)) (f (S.map F))
⊢ Eq (α :=
    X₂ (ShortComplex.map (ShortComplex.mk (X₃ := 0) S.g 0 ⋯) F) ⟶
      X₃ (ShortComplex.map (ShortComplex.mk (X₃ := 0) S.g 0 ⋯) F))
    (g (ShortComplex.map (ShortComplex.mk (X₃ := 0) S.g 0 ⋯) F)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono (X := X₁ (S.map F)) (f (S.map F))
⊢ Eq (α := S.X₂ ⟶ 0) (S.g ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono (X := X₁ (S.map F)) (f (S.map F))
⊢ Eq (α := X₂ (ShortComplex.mk (X₃ := 0) S.g 0 ⋯) ⟶ X₃ (ShortComplex.mk (X₃ := 0) S.g 0 ⋯))
    (g (ShortComplex.mk (X₃ := 0) S.g 0 ⋯)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono (X := X₁ (S.map F)) (f (S.map F))
⊢ Epi (X := X₂ (S.map F)) (g (S.map F))

Tactic:
have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this_1 : Mono (X := X₁ (S.map F)) (f (S.map F))
this : Epi (X := X₂ (S.map F)) (g (S.map F))
⊢ ShortExact (S.map F)

Tactic:
⟨hF S hS.exact⟩

Premises used: CategoryTheory.ShortComplex.ShortExact.exact, CategoryTheory.ShortComplex.ShortExact.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
hF : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this_1 : Mono (X := X₁ (S.map F)) (f (S.map F))
this : Epi (X := X₂ (S.map F)) (g (S.map F))
⊢ ShortExact (S.map F)

Tactic:
exact ⟨hF S hS.exact⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
⊢ ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)

Tactic:
tfae_have 2 → 1
  | hF, S, hS => by
    have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
    have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
    exact ⟨hF S hS.exact⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
⊢ F.PreservesHomology

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
⊢ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
⊢ ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
⊢ ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
tfae_have 3 → 4
  | h => ⟨preservesFiniteLimits_of_preservesHomology F,
      preservesFiniteColimits_of_preservesHomology F⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ ∀ (a : PreservesFiniteLimits F ∧ PreservesFiniteColimits F) (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)

Tactic:
4 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
⊢ ∀ (a : PreservesFiniteLimits F ∧ PreservesFiniteColimits F) (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)

Tactic:
tfae_have 4 → 2
  | ⟨h1, h2⟩, _, h => h.map F
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
tfae_1_to_3 : ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F)), F.PreservesHomology
tfae_2_to_1 :
  ∀ (a : ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)) (S : ShortComplex.{v_1, u_1} C),
    S.ShortExact → ShortExact (S.map F)
tfae_3_to_4 : ∀ (a : F.PreservesHomology), PreservesFiniteLimits F ∧ PreservesFiniteColimits F
tfae_4_to_2 :
  ∀ (a : PreservesFiniteLimits F ∧ PreservesFiniteColimits F) (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F)
⊢ [∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → ShortExact (S.map F),
      ∀ (S : ShortComplex.{v_1, u_1} C), S.Exact → Exact (S.map F), F.PreservesHomology,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
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 : Abelian.{v_1, u_1} C
inst_3 : Abelian.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ PreservesFiniteColimits F ↔ ∀ (S : ShortComplex.{v_1, u_1} C), S.ShortExact → Exact (S.map F) ∧ Epi (F.map S.g)

Tactic:
(Functor.preservesFiniteColimits_tfae F).out 3 0

Premises used: List.TFAE.out, OfNat.ofNat, CategoryTheory.Functor.preservesFiniteColimits_tfae
-- Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
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
x : ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.map f ≫
        Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1))
            Y) =
      Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₁.obj x_1))
            X) ≫
        (obj (functor J C ⋙ inverse J C) x).X₁.map f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
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
x : ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.map f ≫
        Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1))
            Y) =
      Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₂.obj x_1))
            X) ≫
        (obj (functor J C ⋙ inverse J C) x).X₂.map f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
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
x : ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C)
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.map f ≫
        Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1))
            Y) =
      Iso.hom
          ((fun (x_1 : J) ↦
              (Iso.refl ((obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1) :
                (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1 ≅
                  (obj (𝟭 (ShortComplex (Functor.{v_1, v_2, u_1, u_2} J C))) x).X₃.obj x_1))
            X) ≫
        (obj (functor J C ⋙ inverse J C) x).X₃.map f

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
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
x : J ⥤ ShortComplex.{v_2, u_2} C
x_1 : J
⊢ Iso.hom (Iso.refl ((obj (inverse J C ⋙ functor J C) x).obj x_1).X₁) ≫
      ((obj (𝟭 (J ⥤ ShortComplex.{v_2, u_2} C)) x).obj x_1).f =
    ((obj (inverse J C ⋙ functor J C) x).obj x_1).f ≫
      Iso.hom (Iso.refl ((obj (inverse J C ⋙ functor J C) x).obj x_1).X₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
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
x : J ⥤ ShortComplex.{v_2, u_2} C
x_1 : J
⊢ Iso.hom (Iso.refl ((obj (inverse J C ⋙ functor J C) x).obj x_1).X₂) ≫
      ((obj (𝟭 (J ⥤ ShortComplex.{v_2, u_2} C)) x).obj x_1).g =
    ((obj (inverse J C ⋙ functor J C) x).obj x_1).g ≫
      Iso.hom (Iso.refl ((obj (inverse J C ⋙ functor J C) x).obj x_1).X₃)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ (K.XIsoOfEq hi).hom ≫ (Functor.obj (shortComplexFunctor' C c i j k) K).f =
    (Functor.obj (shortComplexFunctor C c j) K).f ≫ Iso.hom (Iso.refl (Functor.obj (shortComplexFunctor C c j) K).X₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ Iso.hom (Iso.refl (Functor.obj (shortComplexFunctor C c j) K).X₂) ≫
      (Functor.obj (shortComplexFunctor' C c i j k) K).g =
    (Functor.obj (shortComplexFunctor C c j) K).g ≫ (K.XIsoOfEq hk).hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
iso : K ≅ L
i : ι
inst_2 : K.HasHomology i
⊢ L.HasHomology i

Tactic:
ShortComplex.hasHomology_of_iso
    ((shortComplexFunctor _ _ i).mapIso iso : K.sc i ≅ L.sc i)

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.ShortComplex.hasHomology_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ Eq (α := A ⟶ K.X (c.next i)) (k ≫ K.d i (c.next i)) 0

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k_1 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
hk : Eq (α := A ⟶ K.X (c.next i)) (k ≫ K.d i (c.next i)) 0
⊢ k ≫ (K.sc i).g = 0

Tactic:
hk
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k_1 : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
hk : Eq (α := A ⟶ K.X (c.next i)) (k ≫ K.d i (c.next i)) 0
⊢ k ≫ (K.sc i).g = 0

Tactic:
exact hk
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
dsimp : CategoryStruct.comp (Y := K.cycles i) ((K.sc i).liftCycles k ⋯) (K.sc i).iCycles = k
⊢ CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj hk) (K.iCycles i) = k

Tactic:
dsimp [liftCycles, iCycles]

Premises used: HomologicalComplex.iCycles, HomologicalComplex.liftCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
⊢ CategoryStruct.comp (Y := K.cycles i) ((K.sc i).liftCycles k ⋯) (K.sc i).iCycles = k

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology i
pos : ∀ (hij : c.Rel i j), Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
neg : ∀ (hij : ¬c.Rel i j), Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology i
hij : c.Rel i j
pos : ∀ (hij : c.Rel i (c.next i)), Eq (α := K.cycles i ⟶ K.X (c.next i)) (K.iCycles i ≫ K.d i (c.next i)) 0
⊢ Eq (α := K.cycles i ⟶ K.X j) (K.iCycles i ≫ K.d i j) 0

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'