awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.moduleCatCyclesIso.inv ≫ S.homologyπ = S.moduleCatLeftHomologyData.π ≫ S.moduleCatHomologyIso.inv

Tactic:
S.moduleCatLeftHomologyData.π_comp_homologyIso_inv

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv, Quotient.liftOn', AddCon.liftOn, Quotient, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, Submodule.liftQ
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.Exact ↔
    Function.Surjective (α := (↑S.X₁ : Type v)) (β := ↥(ModuleCat.Hom.hom S.g).ker)
      (⇑S.moduleCatToCycles : (a : (↑S.X₁ : Type v)) → ↥(ModuleCat.Hom.hom S.g).ker)

Tactic:
simp [S.moduleCatLeftHomologyData.exact_iff_epi_f',
    ModuleCat.epi_iff_surjective, moduleCatLeftHomologyData_K]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f', ModuleCat.epi_iff_surjective, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf :
  ∀ (x : (↑(ModuleCat.of R ↥f.ker) : Type v)),
    Eq (α := (↑(ModuleCat.of R N) : Type v))
      ((ModuleCat.Hom.hom (ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f) :
            (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v))
          x :
        (↑(ModuleCat.of R N) : Type v))
      ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v)) x :
        (↑(ModuleCat.of R N) : Type v))
⊢ ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
x : (↑(ModuleCat.of R ↥f.ker) : Type v)
⊢ Eq (α := (↑(ModuleCat.of R N) : Type v))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom f.ker.subtype ≫ ModuleCat.ofHom f) :
          (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v))
        x :
      (↑(ModuleCat.of R N) : Type v))
    ((ModuleCat.Hom.hom 0 : (a : (↑(ModuleCat.of R ↥f.ker) : Type v)) → (↑(ModuleCat.of R N) : Type v)) x :
      (↑(ModuleCat.of R N) : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h : Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N)
x : (↑f.shortComplexKer.X₂ : Type v)
⊢ Eq (α := (↑f.shortComplexKer.X₃ : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f.shortComplexKer.g :
            (a : (↑f.shortComplexKer.X₂ : Type v)) → (↑f.shortComplexKer.X₃ : Type v))
          x :
        (↑f.shortComplexKer.X₃ : Type v))
      (0 : (↑f.shortComplexKer.X₃ : Type v)) ↔
    Membership.mem (γ := Set (↑f.shortComplexKer.X₂ : Type v))
      (Set.range (ι := (↑f.shortComplexKer.X₁ : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) f.shortComplexKer.f) :
          (a : (↑f.shortComplexKer.X₁ : Type v)) → (↑f.shortComplexKer.X₂ : Type v)))
      x

Tactic:
simp [shortComplexKer]

Premises used: LinearMap.shortComplexKer
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
exac :
  Function.Exact (M := (↑S.X₁ : Type v)) (N := (↑S.X₂ : Type v)) (P := (↑S.X₃ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) S.f) :
      (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) S.g) :
      (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
⊢ S.Exact

Tactic:
(ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mpr exac

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
h :
  ∀ (x : M),
    Eq (α := L)
      ((((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) ∘ₗ ((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M') :
            (a : M) → L)
          x :
        L)
      ((0 : (a : M) → L) x : L)
⊢ ((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) ∘ₗ ((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M') = 0

Tactic:
ext x
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
eq0 : g ∘ₗ f = 0
x : M
⊢ Eq (α := L)
    ((((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) ∘ₗ ((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M') :
          (a : M) → L)
        x :
      L)
    ((0 : (a : M) → L) x : L)

Tactic:
simpa using LinearMap.congr_fun eq0 (eM x)

Premises used: LinearMap.congr_fun, DFunLike.coe
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
rwa :
  Function.Exact.{u_1, v, v} (M := M') (N := N) (P := L) (⇑((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) : (a : M') → N)
    (⇑((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) : (a : N) → L)
rwa₁ :
  Function.Exact.{u_1, v, u_3} (M := M') (N := N) (P := L') (⇑((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) : (a : M') → N)
    (⇑(g ∘ₗ (↑eN : N →ₗ[R] N')) : (a : N) → L')
rwa₂ rwa₃ rwa₄ rwa₅ :
  Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
⊢ Function.Exact (M := M) (N := N) (P := L) (⇑(((↑eN.symm : N' →ₗ[R] N) ∘ₗ f) ∘ₗ (↑eM : M →ₗ[R] M')) : (a : M) → N)
    (⇑((↑eL.symm : L' →ₗ[R] L) ∘ₗ g ∘ₗ (↑eN : N →ₗ[R] N')) : (a : N) → L)

Tactic:
rwa [LinearEquiv.precomp_exact_iff_exact, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact]

Premises used: LinearEquiv.postcomp_exact_iff_exact, LinearEquiv.precomp_exact_iff_exact, LinearEquiv.conj_symm_exact_iff_exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
⊢ (shortComplexOfConj eM eN eL f g ⋯).Exact

Tactic:
ModuleCat.shortComplex_exact _ (exact_conj_of_exact eM eN eL f g exact)

Premises used: _private.0.exact_conj_of_exact, ModuleCat.shortComplex_exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M') (β := N') (⇑f : (a : M') → N')
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := N') (β := L') (⇑g : (a : N') → L')
⊢ (shortComplexOfConj eM eN eL f g ⋯).ShortExact

Tactic:
ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_

Premises used: _private.0.exact_conj_of_exact, ModuleCat.shortComplex_shortExact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M') (β := N') (⇑f : (a : M') → N')
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := N') (β := L') (⇑g : (a : N') → L')
refine_1 :
  Function.Injective (α := (↑(shortComplexOfConj eM eN eL f g ⋯).X₁ : Type v)) (β :=
    (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) (shortComplexOfConj eM eN eL f g ⋯).f) :
      (a : (↑(shortComplexOfConj eM eN eL f g ⋯).X₁ : Type v)) → (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v))
refine_2 :
  Function.Surjective (α := (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v)) (β :=
    (↑(shortComplexOfConj eM eN eL f g ⋯).X₃ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) (shortComplexOfConj eM eN eL f g ⋯).g) :
      (a : (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v)) → (↑(shortComplexOfConj eM eN eL f g ⋯).X₃ : Type v))
⊢ (shortComplexOfConj eM eN eL f g ⋯).ShortExact

Tactic:
refine ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_

Premises used: ModuleCat.shortComplex_shortExact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M') (β := N') (⇑f : (a : M') → N')
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := N') (β := L') (⇑g : (a : N') → L')
⊢ Function.Injective (α := (↑(shortComplexOfConj eM eN eL f g ⋯).X₁ : Type v)) (β :=
    (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) (shortComplexOfConj eM eN eL f g ⋯).f) :
      (a : (↑(shortComplexOfConj eM eN eL f g ⋯).X₁ : Type v)) → (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v))

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type v
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Type v
inst_5 : AddCommGroup L
inst_6 : Module R L
M' : Type u_1
N' : Type u_2
L' : Type u_3
inst_7 : AddCommGroup M'
inst_8 : AddCommGroup N'
inst_9 : AddCommGroup L'
inst_10 : Module R M'
inst_11 : Module R N'
inst_12 : Module R L'
eM : M ≃ₗ[R] M'
eN : N ≃ₗ[R] N'
eL : L ≃ₗ[R] L'
f : M' →ₗ[R] N'
g : N' →ₗ[R] L'
exact : Function.Exact.{u_1, u_2, u_3} (M := M') (N := N') (P := L') (⇑f : (a : M') → N') (⇑g : (a : N') → L')
inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M') (β := N') (⇑f : (a : M') → N')
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := N') (β := L') (⇑g : (a : N') → L')
⊢ Function.Surjective (α := (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v)) (β :=
    (↑(shortComplexOfConj eM eN eL f g ⋯).X₃ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) (shortComplexOfConj eM eN eL f g ⋯).g) :
      (a : (↑(shortComplexOfConj eM eN eL f g ⋯).X₂ : Type v)) → (↑(shortComplexOfConj eM eN eL f g ⋯).X₃ : Type v))

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b c : S₁ ⟶ S₂
h₁ : (a + b + c).τ₁ = (a + (b + c)).τ₁
h₂ : (a + b + c).τ₂ = (a + (b + c)).τ₂
h₃ : (a + b + c).τ₃ = (a + (b + c)).τ₃
⊢ a + b + c = a + (b + c)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₁ = (a + (b + c)).τ₁

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₂ = (a + (b + c)).τ₂

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b c : S₁ ⟶ S₂
⊢ (a + b + c).τ₃ = (a + (b + c)).τ₃

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
h₁ : (0 + a).τ₁ = a.τ₁
h₂ : (0 + a).τ₂ = a.τ₂
h₃ : (0 + a).τ₃ = a.τ₃
⊢ 0 + a = a

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₁ = a.τ₁

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₂ = a.τ₂

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₃ = a.τ₃

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
h₁ : (a + 0).τ₁ = a.τ₁
h₂ : (a + 0).τ₂ = a.τ₂
h₃ : (a + 0).τ₃ = a.τ₃
⊢ a + 0 = a

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₁ = a.τ₁

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₂ = a.τ₂

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (a + 0).τ₃ = a.τ₃

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
h₁ : (a - b).τ₁ = (a + -b).τ₁
h₂ : (a - b).τ₂ = (a + -b).τ₂
h₃ : (a - b).τ₃ = (a + -b).τ₃
⊢ a - b = a + -b

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₁ = (a + -b).τ₁

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₂ = (a + -b).τ₂

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a - b).τ₃ = (a + -b).τ₃

Tactic:
apply sub_eq_add_neg

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
h₁ : (-a + a).τ₁ = Hom.τ₁ 0
h₂ : (-a + a).τ₂ = Hom.τ₂ 0
h₃ : (-a + a).τ₃ = Hom.τ₃ 0
⊢ -a + a = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₁ = Hom.τ₁ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₂ = Hom.τ₂ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a : S₁ ⟶ S₂
⊢ (-a + a).τ₃ = Hom.τ₃ 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
h₁ : (a + b).τ₁ = (b + a).τ₁
h₂ : (a + b).τ₂ = (b + a).τ₂
h₃ : (a + b).τ₃ = (b + a).τ₃
⊢ a + b = b + a

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₁ = (b + a).τ₁

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₂ = (b + a).τ₂

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
a b : S₁ ⟶ S₂
⊢ (a + b).τ₃ = (b + a).τ₃

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ + φ').τ₁ = φ.τ₁ + φ'.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ + φ').τ₂ = φ.τ₂ + φ'.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ + φ').τ₃ = φ.τ₃ + φ'.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ - φ').τ₁ = φ.τ₁ - φ'.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ - φ').τ₂ = φ.τ₂ - φ'.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
⊢ (φ - φ').τ₃ = φ.τ₃ - φ'.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (-φ).τ₁ = -φ.τ₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (-φ).τ₂ = -φ.τ₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
⊢ (-φ).τ₃ = -φ.τ₃

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂

Tactic:
simp only [γ.leftHomologyMap'_eq, γ.neg.leftHomologyMap'_eq, LeftHomologyMapData.neg_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.neg, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq