awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
a : R
inst_4 : S₁.HasLeftHomology
inst_5 : S₂.HasLeftHomology
⊢ cyclesMap (a • φ) = HSMul.hSMul (β := S₁.cycles ⟶ S₂.cycles) a (cyclesMap φ)

Tactic:
cyclesMap'_smul _ _ _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap'_smul, CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (a • φ) h₁ h₂ = a • rightHomologyMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).rightHomologyMap'_eq, RightHomologyMapData.smul_φH, γ.rightHomologyMap'_eq]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, CategoryTheory.ShortComplex.RightHomologyMapData.smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).opcyclesMap'_eq, RightHomologyMapData.smul_φQ, γ.opcyclesMap'_eq]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.smul, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
a : R
inst_4 : S₁.HasRightHomology
inst_5 : S₂.HasRightHomology
⊢ rightHomologyMap (a • φ) = HSMul.hSMul (β := S₁.rightHomology ⟶ S₂.rightHomology) a (rightHomologyMap φ)

Tactic:
rightHomologyMap'_smul _ _ _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
a : R
inst_4 : S₁.HasRightHomology
inst_5 : S₂.HasRightHomology
⊢ opcyclesMap (a • φ) = HSMul.hSMul (β := S₁.opcycles ⟶ S₂.opcycles) a (opcyclesMap φ)

Tactic:
opcyclesMap'_smul _ _ _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap'_smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
a : R
⊢ homologyMap' (a • φ) h₁ h₂ = a • homologyMap' φ h₁ h₂

Tactic:
leftHomologyMap'_smul _ _ _ _

Premises used: CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.leftHomologyMap'_smul
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ : S₁ ⟶ S₂
a : R
inst_4 : S₁.HasHomology
inst_5 : S₂.HasHomology
⊢ homologyMap (a • φ) = HSMul.hSMul (β := S₁.homology ⟶ S₂.homology) a (homologyMap φ)

Tactic:
homologyMap'_smul _ _ _

Premises used: CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap'_smul, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
dsimp : a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
⊢ (a • φ₁).τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + (a • φ₂).τ₁

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
rw : a • (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
⊢ a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁

Tactic:
rw [h.comm₁]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁

Tactic:
simp only [smul_add, Linear.comp_smul]

Premises used: CategoryTheory.Linear.comp_smul, smul_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
dsimp : a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
⊢ (a • φ₁).τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + (a • φ₂).τ₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
rw : a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
⊢ a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂

Tactic:
rw [h.comm₂]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂

Tactic:
simp only [smul_add, Linear.comp_smul, Linear.smul_comp]

Premises used: CategoryTheory.Linear.comp_smul, smul_add, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
dsimp : a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
⊢ (a • φ₁).τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + (a • φ₂).τ₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
rw : a • (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃
⊢ a • φ₁.τ₃ = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃

Tactic:
rw [h.comm₃]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Linear
Goal:
R : Type u_1
C : Type u_2
inst : Semiring R
inst_1 : Category.{v_1, u_2} C
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
S₁ S₂ : ShortComplex.{v_1, u_2} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = a • h.h₃ + (a • h.h₂) ≫ S₂.g + a • φ₂.τ₃

Tactic:
simp only [smul_add, Linear.smul_comp]

Premises used: smul_add, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
x : (↑S.X₁ : Type v)
⊢ Eq (α := (↑S.X₃ : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) S.g :
          (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 :=
                ModuleCat.carrier) S.f :
              (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
            x :
          (↑S.X₂ : Type v)) :
      (↑S.X₃ : Type v))
    (0 : (↑S.X₃ : Type v))

Tactic:
S.zero_apply x

Premises used: CategoryTheory.ShortComplex.zero_apply
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.Exact ↔
    ∀ (x₂ : (↑S.X₂ : Type v)),
      Eq (α := (↑S.X₃ : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.g :
                (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
              x₂ :
            (↑S.X₃ : Type v))
          (0 : (↑S.X₃ : Type v)) →
        ∃ (x₁ : (↑S.X₁ : Type v)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.f :
                (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
              x₁ =
            x₂

Tactic:
S.exact_iff_of_hasForget

Premises used: CategoryTheory.ShortComplex.exact_iff_of_hasForget
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
rw :
  (∀ (x₂ : (↑S.X₂ : Type v)),
      Eq (α := (↑S.X₃ : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.g :
                (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
              x₂ :
            (↑S.X₃ : Type v))
          (0 : (↑S.X₃ : Type v)) →
        ∃ (x₁ : (↑S.X₁ : Type v)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.f :
                (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
              x₁ =
            x₂) ↔
    (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range

Tactic:
rw [moduleCat_exact_iff]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ (∀ (x₂ : (↑S.X₂ : Type v)),
      Eq (α := (↑S.X₃ : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.g :
                (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))
              x₂ :
            (↑S.X₃ : Type v))
          (0 : (↑S.X₃ : Type v)) →
        ∃ (x₁ : (↑S.X₁ : Type v)),
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  ModuleCat.carrier) S.f :
                (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))
              x₁ =
            x₂) ↔
    (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
rw :
  (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range ↔
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
rw [moduleCat_exact_iff_ker_sub_range]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range ↔
    (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
hS : S.Exact
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using hS

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
hS : S.ShortExact
⊢ Function.Injective (α := (↑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 :=
          ModuleCat.carrier) S.f) :
      (a : (↑S.X₁ : Type v)) → (↑S.X₂ : Type v))

Tactic:
hS.injective_f

Premises used: CategoryTheory.ShortComplex.ShortExact.injective_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
hS : S.ShortExact
⊢ Function.Surjective (α := (↑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 :=
          ModuleCat.carrier) S.g) :
      (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))

Tactic:
hS.surjective_g

Premises used: CategoryTheory.ShortComplex.ShortExact.surjective_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
rw :
  (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.g).ker =
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          ModuleCat.carrier) S.f).range
⊢ S.Exact ↔
    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 :=
            ModuleCat.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 :=
            ModuleCat.carrier) S.g) :
        (a : (↑S.X₂ : Type v)) → (↑S.X₃ : Type v))

Tactic:
rw [moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff]

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
X₁ X₂ X₃ : ModuleCat.{v, u} R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker
⊢ f ≫ g = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
X₁ X₂ X₃ : ModuleCat.{v, u} R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
rw rw₁ : (ModuleCat.Hom.hom g).ker ≤ (ModuleCat.Hom.hom g).ker
⊢ (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker

Tactic:
rw [hfg]
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
X₁ X₂ X₃ : ModuleCat.{v, u} R
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
hfg : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker
⊢ (moduleCatMkOfKerLERange f g ⋯).Exact

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using hfg

Premises used: CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ ModuleCat.ofHom (ModuleCat.Hom.hom S.g).ker.subtype ≫ S.g = 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ ModuleCat.of R (↥(ModuleCat.Hom.hom S.g).ker ⧸ S.moduleCatToCycles.range))
    ((ModuleCat.kernelIsLimit S.g).lift (KernelFork.ofι S.f ⋯) ≫ ModuleCat.ofHom S.moduleCatToCycles.range.mkQ) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles

Tactic:
rfl

Premises used: LinearMap.codRestrict, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
M : ModuleCat.{v, u} R
φ : S.moduleCatLeftHomologyData.K ⟶ M
h : S.moduleCatLeftHomologyData.f' ≫ φ = 0
⊢ ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.descH φ h) =
    (ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f').range.liftQ (ModuleCat.Hom.hom φ) ⋯

Tactic:
rfl

Premises used: Submodule.liftQ, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
M : ModuleCat.{v, u} R
φ : M ⟶ S.X₂
h : φ ≫ S.g = 0
⊢ ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.liftK φ h) =
    LinearMap.codRestrict (ModuleCat.Hom.hom S.g).ker (ModuleCat.Hom.hom φ) ⋯

Tactic:
rfl

Premises used: LinearMap.codRestrict, rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.moduleCatCyclesIso.hom ≫ S.moduleCatLeftHomologyData.i = S.iCycles

Tactic:
S.moduleCatLeftHomologyData.cyclesIso_hom_comp_i

Premises used: CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.moduleCatCyclesIso.inv ≫ S.iCycles = S.moduleCatLeftHomologyData.i

Tactic:
S.moduleCatLeftHomologyData.cyclesIso_inv_comp_iCycles

Premises used: CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f'

Tactic:
simp [← cancel_mono S.moduleCatLeftHomologyData.i]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.pOpcycles ≫ S.moduleCatOpcyclesIso.hom = ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ

Tactic:
simp [moduleCatOpcyclesIso]

Premises used: CategoryTheory.ShortComplex.moduleCatOpcyclesIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
x y : (↑S.X₂ : Type v)
h :
  Eq (α := (↑S.opcycles : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) (Y := S.opcycles) S.pOpcycles :
          (a : (↑S.X₂ : Type v)) → (↑S.opcycles : Type v))
        x :
      (↑S.opcycles : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) (Y := S.opcycles) S.pOpcycles :
          (a : (↑S.X₂ : Type v)) → (↑S.opcycles : Type v))
        y :
      (↑S.opcycles : Type v))
⊢ Eq (α := (↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)

Tactic:
simpa using congr(S.moduleCatOpcyclesIso.hom $h)
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
x y : (↑S.X₂ : Type v)
h : Eq (α := (↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range) (Submodule.Quotient.mk x) (Submodule.Quotient.mk y)
⊢ Eq (α := (↑(ModuleCat.of R ((↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) S.moduleCatOpcyclesIso.hom :
          (a : (↑S.opcycles : Type v)) →
            (↑(ModuleCat.of R ((↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) (Y := S.opcycles) S.pOpcycles :
            (a : (↑S.X₂ : Type v)) → (↑S.opcycles : Type v))
          x) :
      (↑(ModuleCat.of R ((↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            ModuleCat.carrier) S.moduleCatOpcyclesIso.hom :
          (a : (↑S.opcycles : Type v)) →
            (↑(ModuleCat.of R ((↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) (Y := S.opcycles) S.pOpcycles :
            (a : (↑S.X₂ : Type v)) → (↑S.opcycles : Type v))
          y) :
      (↑(ModuleCat.of R ((↑S.X₂ : Type v) ⧸ (ModuleCat.Hom.hom S.f).range)) : Type v))

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
x : (↑S.X₂ : Type v)
⊢ Eq (α := (↑S.opcycles : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              ModuleCat.carrier) (Y := S.opcycles) S.pOpcycles :
            (a : (↑S.X₂ : Type v)) → (↑S.opcycles : Type v))
          x :
        (↑S.opcycles : Type v))
      (0 : (↑S.opcycles : Type v)) ↔
    x ∈ (ModuleCat.Hom.hom S.f).range

Tactic:
simpa using moduleCat_pOpcycles_eq_iff _ x 0

Premises used: CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.ShortComplex.ModuleCat
Goal:
R : Type u
inst : Ring R
S : ShortComplex (ModuleCat.{v, u} R)
⊢ S.homologyπ ≫ S.moduleCatHomologyIso.hom = S.moduleCatCyclesIso.hom ≫ S.moduleCatLeftHomologyData.π

Tactic:
S.moduleCatLeftHomologyData.homologyπ_comp_homologyIso_hom

Premises used: CategoryTheory.ShortComplex.moduleCatLeftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.homologyπ_comp_homologyIso_hom