mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫
      (alternatingConst A hOdd hEven hc).iCycles j ≫ φ =
    (ShortComplex.cyclesMapIso (alternatingConstScIsoEven A hOdd hEven hc hpj hnj h)).inv ≫ 0

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Even j
⊢ { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.iCycles ≫ φ = 0
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)).inv ≫
      (alternatingConst A hOdd hEven hc).iCycles j ≫ ψ =
    (ShortComplex.cyclesMapIso (alternatingConstScIsoOdd A hOdd hEven hc hpj hnj h)).inv ≫ 0

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝¹ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
inst✝ : CategoryWithHomology C
j : ℕ
hpj : c.Rel (c.prev j) j
hnj : c.Rel j (c.next j)
h : Odd j
⊢ { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.iCycles ≫ ψ = 0
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ ((point.mapIso e).inv ≫ ed.s' ≫ (drop.mapIso e).hom.app (op ⦋0⦌)) ≫ Y.hom.app (op ⦋0⦌) = 𝟙 Y.right

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ e.inv.right ≫ e.hom.right = 𝟙 Y.right
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ x✝ ∈ (face ∅).obj x✝¹ ↔ x✝ ∈ ⊥.obj x✝¹

Tactic:
simpa using

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ ¬univ = ∅
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
⊢ ((drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)) ≫ Y.left.δ 0 = 𝟙 (Y.left _⦋n⦌)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
⊢ e.inv.left.app (op ⦋n⦌) ≫ e.hom.left.app (op ⦋n⦌) = 𝟙 (Y.left _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ

Tactic:
simpa using

Goal state after:
case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : { x // x ≠ i }
x : Fin (n + 1 + 1)
hx : x ≠ i
⊢ x ∈ {i}ᶜ

Tactic:
simpa using

Goal state after:
n : ℕ
i : Fin (n + 2)
x✝ : { x // x ≠ i }
x : Fin (n + 1 + 1)
hx : x ≠ i
⊢ ¬x = i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
x✝ : ↥{i}ᶜ
x : Fin (n + 2)
hx : x ∈ {i}ᶜ
⊢ x ≠ i

Tactic:
simpa using

Goal state after:
n : ℕ
i : Fin (n + 2)
x✝ : ↥{i}ᶜ
x : Fin (n + 2)
hx : x ∈ {i}ᶜ
⊢ ¬x = i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
x : Fin (n + 1)
⊢ x ∈ Set.range ⇑(Hom.toOrderHom f₁) ↔ x ∈ Set.range ⇑(Hom.toOrderHom f₂)

Tactic:
simpa using

Goal state after:
case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁✝ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂✝ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₁ : Function.Injective ⇑(Hom.toOrderHom f₁)
h₂ : Function.Injective ⇑(Hom.toOrderHom f₂)
h₃ : Finset.image (⇑(Hom.toOrderHom f₁)) univ = Finset.image (⇑(Hom.toOrderHom f₂)) univ
x : Fin (n + 1)
⊢ (∃ y, (Hom.toOrderHom f₁) y = x) ↔ ∃ y, (Hom.toOrderHom f₂) y = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
simpa using

Goal state after:
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
⊢ #S = m + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
x✝¹ x✝ : Fin (d + 1)
h : (fun i ↦ ⟨↑x i, ⋯⟩) x✝¹ = (fun i ↦ ⟨↑x i, ⋯⟩) x✝
⊢ (Hom.toOrderHom (objEquiv ↑x)) x✝¹ = (Hom.toOrderHom (objEquiv ↑x)) x✝

Tactic:
simpa using

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
x✝¹ x✝ : Fin (d + 1)
h : (fun i ↦ ⟨↑x i, ⋯⟩) x✝¹ = (fun i ↦ ⟨↑x i, ⋯⟩) x✝
⊢ ↑x x✝¹ = ↑x x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
⊢ Mono f

Tactic:
simpa using

Goal state after:
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
⊢ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
this : Mono f
⊢ objEquiv.symm f = objEquiv.symm (𝟙 ⦋n⦌)

Tactic:
simpa using

Goal state after:
case refine_1
n : ℕ
f : unop (op ⦋n⦌) ⟶ ⦋n⦌
h : objEquiv.symm f ∈ Δ[n].nonDegenerate n
this : Mono f
⊢ f = 𝟙 ⦋n⦌
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
j₁ j₂ : Fin ⦋n + 1⦌.len
h₁ : ¬j₁.succ = 0
h₂ : j₂.succ ≠ 0
hi : j₁.succ ≤ j₂.succ
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) j₁.succ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) j₂.succ

Tactic:
simpa using

Goal state after:
case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
j₁ j₂ : Fin ⦋n + 1⦌.len
h₁ : ¬j₁.succ = 0
h₂ : j₂.succ ≠ 0
hi : j₁.succ ≤ j₂.succ
⊢ (SimplexCategory.Hom.toOrderHom f) j₁ ≤ (SimplexCategory.Hom.toOrderHom f) j₂
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₂.π c₁ c₁₂ ⁻¹' {j})
i₂ : I₂
i₁ : I₁
h : (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}
⊢ (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}

Tactic:
simpa using

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₂.π c₁ c₁₂ ⁻¹' {j})
i₂ : I₂
i₁ : I₁
h : (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}
⊢ c₁.π c₂ c₁₂ (i₁, i₂) = j
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₁.π c₂ c₁₂ ⁻¹' {j})
i₁ : I₁
i₂ : I₂
h : (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}
⊢ (i₂, i₁) ∈ c₂.π c₁ c₁₂ ⁻¹' {j}

Tactic:
simpa using

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
j : I₁₂
x✝ : ↑(c₁.π c₂ c₁₂ ⁻¹' {j})
i₁ : I₁
i₂ : I₂
h : (i₁, i₂) ∈ c₁.π c₂ c₁₂ ⁻¹' {j}
⊢ c₁.π c₂ c₁₂ (i₁, i₂) = j
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'
⊢ c₁₂.Rel i₁₂ i₁₂'

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'
⊢ c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (c₁.next i₁, i₂))
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₁ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁₂.Rel i₁₂ i₁₂'

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₁ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁₂.Rel (c₁.π c₂ c₁₂ (i₁, i₂)) (c₁.π c₂ c₁₂ (i₁, c₂.next i₂))
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case mpr
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : TotalComplexShape c₂ c₁ c
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c
⊢ K.HasTotal c → K.flip.HasTotal c

Tactic:
· intro
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a : A
⊢ t.z a 0 = 1

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a : A
⊢ t.z a 0 = 1
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
b : A
⊢ t.z 0 b = 1

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
b : A
⊢ t.z 0 b = 1
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : C
⊢ (shiftFunctor C c).map ((↑(t.z a b)).app X) = (↑(t.z a b)).app ((shiftFunctor C c).obj X)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : C
⊢ (shiftFunctor C c).map ((↑(t.z a b)).app X) = (↑(t.z a b)).app ((shiftFunctor C c).obj X)
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝¹⁹ : Category.{v_1, u_1} C₁
inst✝¹⁸ : Category.{v_2, u_2} C₂
inst✝¹⁷ : Category.{v_3, u_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0

Tactic:
dsimp [d₂]
  rw [shape _ _ _ h, Functor.map_zero, Functor.map_zero, zero_app, zero_comp, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : ¬c.Rel j (c.next j)
⊢ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j = 0

Tactic:
rw [zero₁ _ _ _ _ _ _ h₅, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j j' : J
h : ¬c.Rel j' j
⊢ hom₂ f₁ h₂ F c j j' = 0

Tactic:
simpa using

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j j' : J
h : ¬c.Rel j' j
⊢ H.hom j j' = 0
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j : J
⊢ (mapBifunctorMap f₁ f₂ F c).f j =
    (dNext j) (hom₂ f₁ h₂ F c) + (prevD j) (hom₂ f₁ h₂ F c) + (mapBifunctorMap f₁ f₂' F c).f j

Tactic:
simpa using

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j : J
⊢ (mapBifunctorMap f₁ f₂ F c).f j = (dNext j) H.hom + (prevD j) H.hom + (mapBifunctorMap f₁ f₂' F c).f j
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ ComplexShape.embeddingUpIntDownInt.f p' = ComplexShape.embeddingUpIntDownInt.f p

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ p' = p
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
⊢ inl ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inl

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
⊢ inl ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inl
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
⊢ inr ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inr

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit sq.cokernelCofork
s : PushoutCocone f g
⊢ inr ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inr
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ Cofork.π ⋯.cokernelCofork ≫ b = Cofork.π ⋯.cokernelCofork ≫ 0

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ biprod.desc inl inr ≫ b = 0