mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ

pp: case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f = 𝟙 Y

Tactic:
swap

Goal state after:
case refine_2
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ ofHom { toFun := φ, monotone' := ?refine_1 } ≫ f = 𝟙 Y

case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f

Tactic:
f.comm,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f + P.p ≫ g.f ≫ Q.p = f.f + g.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f + P.p ≫ g.f ≫ Q.p = f.f + g.f

Tactic:
g.comm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ f.f + g.f = f.f + g.f
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_surj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ b ∈ Sᶜ, ∃ a, ∃ (ha : a ∈ S), φ a ha = b

Tactic:
rintro ⟨i', j'⟩ hij'
    simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
    refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
    · rintro rfl
      simp only [Fin.val_zero, not_lt_zero] at hij'
    · simpa [S] using! Nat.le_sub_one_of_lt hij'
    · simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = σ (j.castLT ⋯) ≫ δ (i.pred ⋯)

Tactic:
by
  rw [← δ_comp_σ_of_gt]
  · simp
  · rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
    exact H

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: 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 : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

pp: case h
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 : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)), (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑a.succ • X.δ a.succ) = 0

Tactic:
swap

Goal state after:
case h
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 : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)), (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑a.succ • X.δ a.succ) = 0

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 : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
i j : Fin (n.len + 1)
hij : i ≤ j
⊢ j.rev ≤ i.rev

Tactic:
rwa [Fin.rev_le_rev]

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

Goal state before:
pp: i n m : ℕ
h : n + i = m
⊢ σ₀Iter (i + 1) ⋯ = σ 0 ≫ σ₀Iter i h

Tactic:
induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    simp
  | succ i hi' =>
    rw [σ₀Iter_succ, hi' (by lia), σ₀Iter_succ, Category.assoc]

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ n < d

Tactic:
by_contra!
  obtain ⟨x, hx⟩ := x
  simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d n this] at hx

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
m : SimplexCategoryᵒᵖ
y : X.obj m
hy : y ∈ A.obj m
a✝ : ⟨(ConcreteCategory.hom (f.app m)) y, ⋯⟩ ∈ ⊤.obj m
⊢ ⟨(ConcreteCategory.hom (f.app m)) y, ⋯⟩ ∈ (range (A.toImage f)).obj m

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩

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:
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.NonDegenerateSimplices

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
by
    dsimp
    simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
    refine exists_congr (fun f ↦ ?_)
    dsimp at f ⊢
    rw [← NatTrans.naturality_apply e.hom f.op]
    exact (e.app _).toEquiv.apply_eq_iff_eq

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

Tactic:
rw [← degenerate_iff_of_isIso (Subcomplex.toRange f) x,
    Subcomplex.mem_degenerate_iff]

Goal state after:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔
    ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
n : SimplexCategoryᵒᵖ
x y : (nerve C).obj n
h : x.obj = y.obj
⊢ ∀ (i : Fin ((unop n).len + 1)), x.obj i = y.obj i

Tactic:
simp [h]

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

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj : j ∈ ↑(nonDegenerateEquiv' x)
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj⟩

Tactic:
nonDegenerateEquiv'_iff

Goal state after:
case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj✝ : j ∈ ↑(nonDegenerateEquiv' x)
hj : ∃ i, ↑x i = j
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((opObjEquiv ((ConcreteCategory.hom ((stdSimplex.obj n).op.map f)) g)) i.rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i

Tactic:
op_map

Goal state after:
n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((opObjEquiv (opObjEquiv.symm ((ConcreteCategory.hom ((stdSimplex.obj n).map (rev.map f.unop).op)) (opObjEquiv g))))
        i.rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
j : Fin ((unop (op ⦋n + 1⦌)).len + 1)
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove j) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) j

Tactic:
cases j using Fin.cases <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
j : Fin ((unop (op ⦋n + 1 + 1⦌)).len + 1)
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove j) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) j

Tactic:
cases j using Fin.cases <;> simp

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

Goal state before:
pp: case pos
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₁)
⊢ (c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
        (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ?pos✝) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0

pp: case pos
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₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'

Tactic:
swap

Goal state after:
case pos
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₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'

case pos
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₁)
⊢ (c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
        (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ?pos✝) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
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₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₂ c₁₂ i₁₂' i₁₂'' =
    0

pp: case pos
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₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

Tactic:
swap

Goal state after:
case pos
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₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

case pos
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₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₂ c₁₂ i₁₂' i₁₂'' =
    0
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
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₁₂'' =
    -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
          (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ?pos✝) ≫
        K.D₂ c₁₂ i₁₂' i₁₂''

pp: case pos
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₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'

Tactic:
swap

Goal state after:
case pos
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₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'

case pos
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₁₂'' =
    -(c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
          (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂' ?pos✝) ≫
        K.D₂ c₁₂ i₁₂' i₁₂''
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j =
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
by
  dsimp [mapBifunctorComp₁₂MapObjIso]
  apply CofanMapObjFun.ιMapObj_iso_inv

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
⊢ ρ₂₃.q (i₁, i₂₃) = r (i₁, i₂, i₃)

Tactic:
← h₂₃,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
inst✝² : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₂₃ : ρ₂₃.I₂₃
h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃
⊢ ρ₂₃.q (i₁, ρ₂₃.p (i₂, i₃)) = r (i₁, i₂, i₃)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
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 i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0

pp: case pos
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 i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

Tactic:
swap

Goal state after:
case pos
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 i₂ (c₂.next i₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'

case pos
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 i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
        (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂' ?pos✝) ≫
      K.D₁ c₁₂ i₁₂' i₁₂'' =
    0
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 L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [d₂_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₂
⊢ CommShift (flipApp (𝟙 G₁) x✝) M

Tactic:
simp only [flipApp, flipFunctor_obj, Functor.map_id, id_app]

Goal state after:
C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₂
⊢ CommShift (𝟙 (G₁.flip.obj x✝)) M
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q (n + x) ⋯) =
    𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x))

Tactic:
simp only [ι_totalDesc, comp_id, id_comp]

Goal state after: