mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
⊢ ∀ (ha : ij ∈ S), φ ij ha ∈ Sᶜ

Tactic:
hij

Goal state after:
case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
CategoryTheory.SimplicialObject.δ_comp_δ''

Goal state after:
case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (i, j).2 ≫ X.δ (i, j).1

case h.e_a.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).castSucc

Tactic:
exact Nat.le_of_lt h

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)

Tactic:
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]

Goal state after:
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ⇑(Hom.toOrderHom f)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]

Goal state after:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : ↑j = ↑j' + i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ j' ≫ X.σ₀Iter i ⋯

Tactic:
simp [σ, σ₀Iter, ← Functor.map_comp, ← op_comp,
    SimplexCategory.σ_σ₀Iter' i j j']

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + i = m
hj' : ↑j = ↑j' + i
⊢ δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'

Tactic:
induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : j = j' := by lia
    simp
  | succ i hi =>
    obtain _ | m := m
    · grind
    · obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero
        (by rintro rfl; dsimp at hj'; lia)
      rw [δ₀Iter_succ_assoc .., δ₀Iter_succ ..,
        dsimp% δ_comp_σ_of_le (i := 0) (j := j) (by simp),
        reassoc_of% hi j j' (by lia) (by grind)]

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j

Tactic:
obtain rfl : j = k.val := by grind [dsimp% Fin.lt_def.1 hk']

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
m : ℕ
k : Fin (⦋n⦌.len + 1)
hk' : k.castSucc < i
h : m + (↑k + 1) = n + 1
hi' : ↑i ≤ ↑k + 1
hk : ↑k ≤ ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter (↑k + 1) ⋯)) (i.succAbove k)) = ↑k - ↑k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
⊢ δ i = δ j → i = j

Tactic:
hij

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
⊢ σ i = σ j → i = j

Tactic:
hij

Goal state after:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i = j
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
⊢ ↑(j.predAbove k) ≤ i

Tactic:
by_cases! hk' : k ≤ j.castSucc

Goal state after:
case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
hk' : k ≤ j.castSucc
⊢ ↑(j.predAbove k) ≤ i

case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
hk' : j.castSucc < k
⊢ ↑(j.predAbove k) ≤ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Basic

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map x✝¹)) ((ConcreteCategory.hom (Y.map ((Opposite.unop x✝³).const ⦋0⦌ 0).op)) y)

Tactic:
rw [← CategoryTheory.comp_apply, ← Functor.map_comp]

Goal state after:
X Y : SSet
y : Y _⦋0⦌
x✝³ x✝² : SimplexCategoryᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : X.obj x✝³
⊢ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y =
    (ConcreteCategory.hom (Y.map (((Opposite.unop x✝³).const ⦋0⦌ 0).op ≫ x✝¹))) y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
A B : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (op ⦋n⦌)
⊢ ↑x ∈ B.obj (op ⦋n⦌)

Tactic:
exact h _ (X.dim_lt_of_nonDegenerate x d) ⟨hx, x.prop⟩

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

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map ((image.ι f).op ≫ (factorThruImage f).op))) y = x
this : (image f).len ≤ m
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
exact ⟨(image f).len, by lia, factorThruImage f, inferInstance, by aesop⟩

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

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))
⊢ x ∈ X.degenerate (n + 1)

Tactic:
simp only [Set.mem_iUnion, Set.mem_range] at hx

Goal state after:
case mpr
X : SSet
n : ℕ
x : X _⦋n + 1⦌
hx : ∃ i y, (ConcreteCategory.hom (SimplicialObject.σ X i)) y = x
⊢ x ∈ X.degenerate (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Epi f
⊢ range f = ⊤

Tactic:
range_eq_top_iff

Goal state after:
X Y : SSet
f : X ⟶ Y
inst✝ : Epi f
⊢ Epi f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h : (fun x ↦ N.mk ↑x ⋯) x = (fun x ↦ N.mk ↑x ⋯) y
⊢ x = y

Tactic:
N.ext_iff,

Goal state after:
X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h : ((fun x ↦ N.mk ↑x ⋯) x).toS = ((fun x ↦ N.mk ↑x ⋯) y).toS
⊢ x = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.subcomplex ≤ y.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Goal state after:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.simplex ∈ y.subcomplex.obj (Opposite.op ⦋x.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ y.subcomplex ≤ x.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Goal state after:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ y.simplex ∈ x.subcomplex.obj (Opposite.op ⦋y.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ (N.mk ↑y ⋯).subcomplex ≤ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ (N.mk ↑y ⋯).simplex ∈
    { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex.obj (Opposite.op ⦋(N.mk ↑y ⋯).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_2
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex ≤ (N.mk ↑y ⋯).subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]

Goal state after:
case refine_2
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (X.map f.op)) ↑y ∈ (N.mk ↑y ⋯).subcomplex.obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
⊢ ⨆ x, ofSimplex ↑x.snd = ⊤

Tactic:
rw [eq_top_iff_contains_nonDegenerate]
  intro n x hx
  simp only [Subfunctor.iSup_obj, Set.mem_iUnion, Sigma.exists,
    Subtype.exists, exists_prop]
  exact ⟨n, x, hx, mem_ofSimplex_obj x⟩

Goal state after:
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 : ℕ
i : Fin (n + 1)
⊢ ((drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)) ≫ Y.left.σ i.succ =
    Y.left.σ i ≫ (drop.mapIso e).inv.app (op ⦋n + 1⦌) ≫ ed.s (n + 1) ≫ (drop.mapIso e).hom.app (op ⦋n + 1 + 1⦌)

Tactic:
simp [← SimplicialObject.σ_naturality, s_comp_σ_assoc,
      ← SimplicialObject.σ_naturality_assoc]

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

Goal state before:
pp: case succ
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 k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0

Tactic:
rw [C.shape, comp_zero]

Goal state after:
case succ.a
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 k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel 0 (n✝ + 1 + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ ⟨(Hom.toOrderHom (objEquiv x)) i₁, ⋯⟩ ≤ ⟨(Hom.toOrderHom (objEquiv x)) i₂, ⋯⟩

Tactic:
simp only [Subtype.mk_le_mk]
            exact OrderHom.monotone _ h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ { f := fun i₂ ↦ d₁ i₁ i₁' i₂, comm' := ⋯ }.f i₂ = Hom.f 0 i₂

Tactic:
exact shape₁ i₁ i₁' h i₂

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

Goal state before:
pp: case pos
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

pp: case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
· ext i₂ i₁ h₁
    dsimp [totalFlipIsoX]
    rw [ι_totalDesc_assoc, Linear.units_smul_comp, ι_D₂, ι_D₁_assoc]
    dsimp
    by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
    · have h₃ : ComplexShape.π c₂ c₁ c (ComplexShape.next c₂ i₂, i₁) = j' := by
        rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]
      have h₄ : ComplexShape.π c₁ c₂ c (i₁, ComplexShape.next c₂ i₂) = j' := by
        rw [← h₃, ComplexShape.π_symm c₁ c₂ c]
      rw [K.d₂_eq _ _ h₂ _ h₄, K.flip.d₁_eq _ h₂ _ _ h₃, Linear.units_smul_comp,
        assoc, ι_totalDesc, Linear.comp_units_smul, smul_smul, smul_smul,
        ComplexShape.σ_ε₂ c₁ c i₁ h₂]
      rfl
    · rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

Goal state after:
case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').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
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X

Tactic:
dsimp [shiftFunctorAdd']

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
i j k : A
h : i + j = k
X : t.Category
⊢ (eqToHom ⋯).app X ≫ (shiftFunctorAdd t.Category i j).hom.app X =
    ↑(t.z i j) • (eqToHom ⋯).app X ≫ (shiftFunctorAdd C i j).hom.app X
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
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X =
    ↑(t.z i j) •
      (t.shiftIso k).hom.app X ≫
        (shiftFunctorAdd' C i j k h).hom.app X ≫
          (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)

Tactic:
by
  have : (shiftFunctorAdd' t.Category i j k h).hom.app X =
      (t.z i j).val • (shiftFunctorAdd' C i j k h).hom.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch
  rw [this]
  congr
  change _ = 𝟙 _ ≫ _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ 𝟙 _
  simp

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
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X

Tactic:
dsimp [shiftFunctorAdd']

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
i j k : A
h : i + j = k
X : t.Category
⊢ (shiftFunctorAdd t.Category i j).inv.app X ≫ (eqToHom ⋯).app X =
    ↑(t.z i j)⁻¹ • (shiftFunctorAdd C i j).inv.app X ≫ (eqToHom ⋯).app X
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 : ℤ
⊢ ((dNext (-n)) h.hom).op = (prevD n) fun p q ↦ (h.hom (-q) (-p)).op

Tactic:
rw [dNext_eq _ (i' := - (n - 1)) (by dsimp; lia)]

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 : ℤ
⊢ (K.d (-n) (-(n - 1)) ≫ h.hom (-(n - 1)) (-n)).op = (prevD n) fun p q ↦ (h.hom (-q) (-p)).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 ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n =
    ((dNext (-n)) fun p q ↦
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom (-q) (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op

Tactic:
rw [dNext_eq _ (i' := - (n - 1)) (by dsimp; lia)]

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 ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n =
    (K.d (-n) (-(n - 1)) ≫
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
          (h.hom (- -n) (- -(n - 1))).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasProduct A
inst✝¹ : HasProduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ ∏ᶜ A
b : Y ⟶ ∏ᶜ B
sq : CommSq t p (Limits.Pi.map f) b
⊢ sq.HasLift

Tactic:
have sq' (j : J) :
        CommSq (t ≫ Pi.π _ j) p (f j) (b ≫ Pi.π _ j) :=
      ⟨by rw [← Category.assoc, ← sq.w]; simp⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasProduct A
inst✝¹ : HasProduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ ∏ᶜ A
b : Y ⟶ ∏ᶜ B
sq : CommSq t p (Limits.Pi.map f) b
sq' : ∀ (j : J), CommSq (t ≫ Pi.π A j) p (f j) (b ≫ Pi.π B j)
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : i < n
hX : X.IsGE n
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
isGE_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n i : ℤ
hi : i < n
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
⊢ IsZero ((homologyFunctor C i).obj X)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝² : HasCoproduct X
inst✝¹ : HasCoproduct Y
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h : ∀ (i : J), cofibrations C (f i)
⊢ cofibrations C (Limits.Sigma.map f)

Tactic:
exact MorphismProperty.colimMap _ (fun ⟨i⟩ ↦ h i)

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : (trivialCofibrations C).MapFactorizationData (fibrations C) f
this✝ : Cofibration hf.i
this : WeakEquivalence hf.i
⊢ weakEquivalences C f

Tactic:
let φ : pushout hf.i h.i.left ⟶ Y :=
      pushout.desc (hf.p ≫ h.i.right) w (by simp)

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : WeakEquivalence w
hf : (trivialCofibrations C).MapFactorizationData (fibrations C) f
this✝ : Cofibration hf.i
this : WeakEquivalence hf.i
φ : pushout hf.i (Arrow.Hom.left h.i) ⟶ Y := pushout.desc (hf.p ≫ Arrow.Hom.right h.i) w ⋯
⊢ weakEquivalences C f