mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ autoParam
    (∀ (X Y : J ⥤ C) (f : X ⟶ Y),
      (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
        eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro X Y f
    ext j
    simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ f.app (op ⦋n + 1⦌) ≫ Y.δ x✝¹ = X.δ x✝¹ ≫ f.app (op ⦋n⦌)

Tactic:
symm

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ X.δ x✝¹ ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ Y.δ x✝¹
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: ⊢ δ 0 = ⦋0⦌.const ⦋0 + 1⦌ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: ⊢ δ 1 = ⦋0⦌.const ⦋0 + 1⦌ 0

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: ⊢ mkOfSucc 1 = δ 0

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: ⊢ mkOfSucc 0 = δ 2

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
⊢ 0 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 1 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ ¬1 ≤ 0

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 0
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 0
⊢ ¬2 ≤ 0

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ ¬2 ≤ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ f.app ⦋n⦌ ≫ Y.δ x = X.δ x ≫ f.app ⦋n + 1⦌

Tactic:
symm

Goal state after:
case e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ X.δ x ≫ f.app ⦋n + 1⦌ = f.app ⦋n⦌ ≫ Y.δ x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Surjective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ Function.Injective (Hom.toOrderHom f).toFun

Tactic:
by rwa [Finite.injective_iff_surjective]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos.inl
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk✝ : ↑k ≤ i
hk : ↑k < i
⊢ 0 = ↑(Fin.predAbove 0 ((ConcreteCategory.hom (σ₀Iter i ⋯)) k))

Tactic:
grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_lt]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
⊢ s ≤ t ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
rw [le_def, Subcomplex.ofSimplex_le_iff, Subfunctor.ofSection_obj, Set.mem_ofPred_eq]
  tauto

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
⊢ X.Finite

Tactic:
by
  obtain ⟨d, _⟩ := Y.hasDimensionLT_of_finite
  have := hasDimensionLT_of_mono f d
  exact finite_of_hasDimensionLT _ d
    (fun _ _ ↦ Finite.of_injective _
      ((injective_of_mono (f.app _)).comp Subtype.val_injective))

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), ↑x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) →
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (A.toSSet.map f.op))

Tactic:
· obtain ⟨x, hx⟩ := x
    rintro ⟨m, hm, f, _, ⟨y, rfl⟩⟩
    refine ⟨m, hm, f, inferInstance, ⟨y, ?_⟩, rfl⟩
    have := isSplitEpi_of_epi f
    simpa [Set.mem_preimage, ← op_comp, ← comp_apply, ← Functor.map_comp] using
      A.map (section_ f).op hx

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∈ A.toSSet.nonDegenerate n ↔ ↑x ∈ X.nonDegenerate n

Tactic:
by
  rw [mem_nonDegenerate_iff_notMem_degenerate,
    mem_nonDegenerate_iff_notMem_degenerate, mem_degenerate_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: ⊢ 2 = Fin.succ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: ⊢ Fin.succ 0 < 2

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: ⊢ δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋0 + 1⦌ 0) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: ⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋0 + 1⦌ 1) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: ⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 2 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1 =
    δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 0 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ δ₂ 0 Edge._proof_1 _proof_3 ≫ δ₂ 1 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯

Tactic:
decide

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
cases j <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: ⊢ stdSimplex.δ 1 = SSet.const (obj₀Equiv.symm 0)

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: ⊢ stdSimplex.δ 0 = SSet.const (obj₀Equiv.symm 1)

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: ⊢ (faceSingletonIso 0).hom ≫ (face {0}).ι = stdSimplex.δ 1

Tactic:
decide

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: ⊢ (faceSingletonIso 1).hom ≫ (face {1}).ι = stdSimplex.δ 0

Tactic:
decide

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
cases j <;> simp

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

Goal state before:
pp: case neg
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₂.Rel (c₂.next i₂) (c₂.next (c₂.next i₂))
⊢ c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.d₂ c₁₂ i₁ (c₂.next i₂) i₁₂'' = 0

Tactic:
· rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]

Goal state after:
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₁₂'' : I₁₂
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
by_cases h₁ : c₁₂.Rel i₁₂ i₁₂'
  · by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
    · ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₂_assoc, comp_zero]
      by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
      · rw [totalAux.d₂_eq K c₁₂ i₁ h₃ i₁₂']; swap
        · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel (c₂.next i₂) (c₂.next (c₂.next i₂))
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₂_eq_zero c₁₂ _ _ _ h₃, zero_comp]
    · rw [K.D₂_shape c₁₂ _ _ h₂, comp_zero]
  · rw [K.D₂_shape c₁₂ _ _ h₁, zero_comp]

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

Goal state before:
pp: case neg
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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = -K.d₁ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂''

Tactic:
· rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_zero]
        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂']; swap
          · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, h]
          simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
          rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]

Goal state after:
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₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (y₁, y₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
subst h₁ h₂
  simp

Goal state after:
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₁₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ y₁ y₂ i₁₂ ⋯

Tactic:
subst h₁ h₂
  simp

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₂ : 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
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₂ c₂ c (i₁, i₂)) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (F.obj (L₁.X i₁)).map (L₂.d i₂ i₂') ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -((c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
        (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') ≫
          (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
            (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')

Tactic:
NatTrans.naturality_assoc,

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₂ : 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
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₂ c₂ c (i₁, i₂)) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (F.obj (L₁.X i₁)).map (L₂.d i₂ i₂') ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -((c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')
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 : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
← CatCenter.mul_app_assoc,

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 : t.Category
⊢ (↑(t.z (a + b) c) * ↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
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 : t.Category
⊢ (↑(t.z (a + b) c) * ↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
← CatCenter.mul_app_assoc,

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 : t.Category
⊢ (↑(t.z (a + b) c) * ↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c)) * ↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
x✝ : (up ℤ).Rel n n'
⊢ (K.totalShift₂XIso y n (n + y) ⋯).hom ≫ ((shiftFunctor (HomologicalComplex C (up ℤ)) y).obj (K.total (up ℤ))).d n n' =
    (((shiftFunctor₂ C y).obj K).total (up ℤ)).d n n' ≫ (K.totalShift₂XIso y n' (n' + y) ⋯).hom

Tactic:
dsimp
      simp only [total_d, Preadditive.add_comp, Preadditive.comp_add, smul_add,
        Linear.comp_units_smul, K.D₁_totalShift₂XIso_hom y n n' _ _ rfl rfl,
        K.D₂_totalShift₂XIso_hom y n n' _ _ rfl rfl]

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (h.hom (-n) (-(n + 1)) ≫ L.d (-(n + 1)) (-n)).op = (dNext n) fun p q ↦ (h.hom (-q) (-p)).op

Tactic:
symm

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ ((dNext n) fun p q ↦ (h.hom (-q) (-p)).op) = (h.hom (-n) (-(n + 1)) ≫ L.d (-(n + 1)) (-n)).op
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (K.d (-n) (-(n - 1)) ≫ h.hom (-(n - 1)) (-n)).op = (prevD n) fun p q ↦ (h.hom (-q) (-p)).op

Tactic:
symm

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ ((prevD n) fun p q ↦ (h.hom (-q) (-p)).op) = (K.d (-n) (-(n - 1)) ≫ h.hom (-(n - 1)) (-n)).op
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case h₀
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 (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
⊢ biprod.inl ≫ s.π = inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
symm

Goal state after:
case h₀
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 (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : inl ≫ m = biprod.inl ≫ s.π
⊢ inl ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inl ≫ s.π
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case h₁
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 (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ biprod.inr ≫ s.π = inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
symm

Goal state after:
case h₁
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 (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
m : sq.cokernelCofork.pt ⟶ s.pt
hm : inr ≫ m = biprod.inr ≫ s.π
⊢ inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = biprod.inr ≫ s.π