awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
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)
⊢ 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)
have 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')
Tactic: rwa [LinearEquiv.precomp_exact_iff_exact, LinearEquiv.postcomp_exact_iff_exact,
    LinearEquiv.conj_symm_exact_iff_exact]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
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
have refine_1 : Function.Injective (α := (↑(shortComplexOfConj eM eN eL f g sorry).X₁ : Type v)) (β :=
  (↑(shortComplexOfConj eM eN eL f g sorry).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 sorry).f) :
    (a : (↑(shortComplexOfConj eM eN eL f g sorry).X₁ : Type v)) → (↑(shortComplexOfConj eM eN eL f g sorry).X₂ : Type v))
Tactic: refine ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ModuleCat (goal)
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))
⊢ (shortComplexOfConj eM eN eL f g ⋯).ShortExact
have refine_2 : Function.Surjective (α := (↑(shortComplexOfConj eM eN eL f g sorry).X₂ : Type v)) (β :=
  (↑(shortComplexOfConj eM eN eL f g sorry).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 sorry).g) :
    (a : (↑(shortComplexOfConj eM eN eL f g sorry).X₂ : Type v)) → (↑(shortComplexOfConj eM eN eL f g sorry).X₃ : Type v))
Tactic: refine ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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)
have h₁ : (a + b + c).τ₁ = (a + (b + c)).τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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)).τ₁
⊢ a + b + c = a + (b + c)
have h₂ : (a + b + c).τ₂ = (a + (b + c)).τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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)).τ₂
⊢ a + b + c = a + (b + c)
have h₃ : (a + b + c).τ₃ = (a + (b + c)).τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
have h₁ : (0 + a).τ₁ = a.τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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.τ₁
⊢ 0 + a = a
have h₂ : (0 + a).τ₂ = a.τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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.τ₂
⊢ 0 + a = a
have h₃ : (0 + a).τ₃ = a.τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
have h₁ : (a + 0).τ₁ = a.τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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.τ₁
⊢ a + 0 = a
have h₂ : (a + 0).τ₂ = a.τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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.τ₂
⊢ a + 0 = a
have h₃ : (a + 0).τ₃ = a.τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
have h₁ : (a - b).τ₁ = (a + -b).τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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).τ₁
⊢ a - b = a + -b
have h₂ : (a - b).τ₂ = (a + -b).τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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).τ₂
⊢ a - b = a + -b
have h₃ : (a - b).τ₃ = (a + -b).τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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 = 0
have h₁ : (-a + a).τ₁ = Hom.τ₁ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ -a + a = 0
have h₂ : (-a + a).τ₂ = Hom.τ₂ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ -a + a = 0
have h₃ : (-a + a).τ₃ = Hom.τ₃ 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
have h₁ : (a + b).τ₁ = (b + a).τ₁
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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).τ₁
⊢ a + b = b + a
have h₂ : (a + b).τ₂ = (b + a).τ₂
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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).τ₂
⊢ a + b = b + a
have h₃ : (a + b).τ₃ = (b + a).τ₃
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), leftHomologyMap' (-φ) h₁ h₂ = -leftHomologyMap' φ h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂),
  leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₂ + leftHomologyMap' φ' h₁ h₂
have have : ∀ (γ' : LeftHomologyMapData φ' h₁ h₂),
  leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
Tactic: have γ' : LeftHomologyMapData φ' h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
have have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
Tactic: have γ : LeftHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
have have : ∀ (γ' : LeftHomologyMapData φ' h₁ h₂), cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
Tactic: have γ' : LeftHomologyMapData φ' h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂),
  rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
have have : ∀ (γ' : RightHomologyMapData φ' h₁ h₂),
  rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
Tactic: have γ' : RightHomologyMapData φ' h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
have have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
Tactic: have γ : RightHomologyMapData φ h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
have have : ∀ (γ' : RightHomologyMapData φ' h₁ h₂), opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
Tactic: have γ' : RightHomologyMapData φ' h₁ h₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + φ₁.τ₁
have rw : φ₂.τ₁ = -S₁.f ≫ h.h₁ + -h.h₀ + (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁)
Tactic: rw [h.comm₁, comp_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₂ = S₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + φ₁.τ₂
have rw : φ₂.τ₂ = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂)
Tactic: rw [h.comm₂, comp_neg, neg_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + φ₁.τ₃
have rw : φ₂.τ₃ = -h.h₃ + -h.h₂ ≫ S₂.g + (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃)
Tactic: rw [h.comm₃, neg_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (-φ₁).τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + (-φ₂).τ₁
have rw : -φ₂.τ₁ + -(S₁.f ≫ h.h₁ + h.h₀) = -S₁.f ≫ h.h₁ + -h.h₀ + -φ₂.τ₁
Tactic: rw [neg_τ₁, neg_τ₁, h.comm₁, neg_add_rev, comp_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (-φ₁).τ₂ = S₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + (-φ₂).τ₂
have rw : -φ₂.τ₂ + -(S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) = -S₁.g ≫ h.h₂ + -h.h₁ ≫ S₂.f + -φ₂.τ₂
Tactic: rw [neg_τ₂, neg_τ₂, h.comm₂, neg_add_rev, comp_neg, neg_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (-φ₁).τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃
have rw : -(h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.h₃ + -h.h₂ ≫ S₂.g + -φ₂.τ₃
Tactic: rw [neg_τ₃, neg_τ₃, h.comm₃, neg_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₁ = S₁.f ≫ (h₁₂.h₁ + h₂₃.h₁) + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
have rw : S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
Tactic: rw [h₁₂.comm₁, h₂₃.comm₁, comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₂ = S₁.g ≫ (h₁₂.h₂ + h₂₃.h₂) + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂
have rw : S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
  S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂
Tactic: rw [h₁₂.comm₂, h₂₃.comm₂, comp_add, add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₃ = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃
have rw : h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + h₂₃.h₂ ≫ S₂.g) + φ₃.τ₃
Tactic: rw [h₁₂.comm₃, h₂₃.comm₃, add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁
have rw : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
  S₁.f ≫ h.h₁ + S₁.f ≫ h'.h₁ + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
Tactic: rw [add_τ₁, add_τ₁, h.comm₁, h'.comm₁, comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₂ = S₁.g ≫ (h.h₂ + h'.h₂) + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂ + φ₄).τ₂
have rw : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
  S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + h'.h₁ ≫ S₂.f) + (φ₂.τ₂ + φ₄.τ₂)
Tactic: rw [add_τ₂, add_τ₂, h.comm₂, h'.comm₂, comp_add, add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ + φ₃).τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂ + φ₄).τ₃
have rw : h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
  h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)
Tactic: rw [add_τ₃, add_τ₃, h.comm₃, h'.comm₃, add_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂ - φ₄).τ₁
have rw : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
  S₁.f ≫ h.h₁ - S₁.f ≫ h'.h₁ + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)
Tactic: rw [sub_τ₁, sub_τ₁, h.comm₁, h'.comm₁, comp_sub]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₂ = S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂ - φ₄).τ₂
have rw : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
  S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - h'.h₁ ≫ S₂.f) + (φ₂.τ₂ - φ₄.τ₂)
Tactic: rw [sub_τ₂, sub_τ₂, h.comm₂, h'.comm₂, comp_sub, sub_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃
have rw : h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
  h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - h'.h₂ ≫ S₂.g) + (φ₂.τ₃ - φ₄.τ₃)
Tactic: rw [sub_τ₃, sub_τ₃, h.comm₃, h'.comm₃, sub_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
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
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ S₃.g ≫ ψ.τ₃ ≫ h.h₃ = 0
have rw : ψ.τ₂ ≫ S₁.g ≫ h.h₃ = 0
Tactic: rw [← ψ.comm₂₃_assoc, h.g_h₃, comp_zero]